Theory GTT_TRS

text ‹GTT for accepting parallel steps of a (left-linear, right-ground) TRS›

theory GTT_TRS
  imports GTT TA_moves GTT_Transitive_Closure
begin

(*Another experiment at correct setup*)
(*In this setup we use option types, The option Some x, plays the same role as e_x 
in the text of the paper*)


type_synonym ('f,'q) term_state = "('f, 'q) term option"

definition cmn_ta_rules::"('f, 'v) term set ⇒ (('f, 'v) term option, 'f) ta_rule set"
  where
"cmn_ta_rules T ≡ {(f (map Some ts) → Some (Fun f ts))|f ts t. Fun f ts ⊴ t ∧ t ∈ T}
                     "
(*Fun f ts ⊴ t ∧ t ∈ T*)
assumes"Fun f [] ⊴ t""t ∈ T"">lemma assumes "Fun f [] ⊴ t" "t ∈ T"
  shows "(f [] → Some (Fun f [])) ∈ cmn_ta_rules T"
  using assms unfolding cmn_ta_rules_def by blast



definition TRS_fst::"('f, 'v) trs ⇒ ('f, 'v) term set"
  where
"TRS_fst Ts ≡ {fst R|R. R ∈ Ts} "

definition TRS_snd::"('f, 'v) trs ⇒ ('f, 'v) term set"
  where
"TRS_snd Ts ≡ {snd R|R. R ∈ Ts}"

definition TRS_terms::"('f, 'v) trs ⇒ ('f, 'v) term set"
  where
"TRS_terms Ts ≡ (TRS_fst Ts) ∪ (TRS_snd Ts)"

definition trs_to_ta_A::"('f, 'v) trs ⇒ (('f, 'v) term option, 'f) ta"
  where
"trs_to_ta_A Ts ≡ ta.make {}
  (cmn_ta_rules (TRS_terms Ts))
  {(Some l, Some r)| l r. (l,r) ∈ Ts}"


definition trs_to_ta_B::"('f, 'v) trs ⇒ (('f, 'v) term option, 'f) ta"
  where
"trs_to_ta_B Ts ≡ ta.make {}
  (cmn_ta_rules (TRS_terms Ts))
  {(Some r, Some l)| l r. (l,r) ∈ Ts}"


abbreviation abs::"('f, 'v) term ⇒  ('f, ('f, 'v) term option) term "
  where
"abs x ≡ adapt_vars x"

abbreviation rep::" ('f, ('f, 'v) term option) term ⇒ ('f, 'v) term"
  where
"rep x ≡ adapt_vars x"

assumes"ground x"shows"abs (rep x) = x" ">lemma assumes "ground x" shows "abs (rep x) = x" 
  using assms by fastforce


abbreviation abs_R::"(('f, 'v) term × ('f, 'v) term) set 
                          
        ⇒  (('f, ('f, 'v) term option) term × ('f, ('f, 'v) term option) term) set"
  where
"abs_R R ≡ (λt. (abs (fst t), abs (snd t))) ` R"

lemma symmetry_in_G_D: " ta_rules (trs_to_ta_B R) = ta_rules (trs_to_ta_A R)" 
    "ta_eps (trs_to_ta_B R) = ((λt. (snd t, fst t)) ` ta_eps (trs_to_ta_A R))" 
    unfolding trs_to_ta_B_def trs_to_ta_A_def by force+ 

(*Finiteness Theorems*)
lemma finite_embedding:
  assumes "finite R"
  shows "finite {(Some l, Some r)| l r. (l,r) ∈ R}"
proof -
  have "{(Some l, Some r)| l r. (l,r) ∈ R} = (λ(l, r). (Some l, Some r)) ` R"
    by auto
  then show ?thesis using assms by auto
qed


lemma finite_collect:
  assumes "finite S"
  shows "finite {t| t w. t ⊴ w ∧ w ∈ S}"
proof-
 have "∀w ∈ S. finite {t|t. t ⊴ w}" using finite_subterms assms by auto
  hence "finite (⋃ ((λw.  {t|t. t ⊴ w}) ` S))" using assms by blast
  moreover have "{t| t w. t ⊴ w ∧ w ∈ S} = ⋃ ((λw.  {t|t. t ⊴ w}) ` S)"
    by blast
  ultimately show ?thesis by argo
qed

 
lemma finite_ta_states:
  assumes "finite R"
  shows "finite (ta_states (trs_to_ta_A R))" "finite (ta_states (trs_to_ta_B R))"
proof-
  have eps:"finite (ta_eps (trs_to_ta_A R))" using assms  finite_embedding[OF assms] 
    unfolding trs_to_ta_A_def ta.make_def by auto
  moreover have rules:"finite (ta_rules (trs_to_ta_A R))" 
  proof-
    have fin:"finite (TRS_terms R)" using assms unfolding TRS_terms_def TRS_fst_def TRS_snd_def
    proof -
      have "∀f. finite {t. ∃p. (t::('a, 'b) Term.term) = f p ∧ p ∈ R}"
        by (metis (no_types) Collect_mem_eq assms finite_image_set)
      then show "finite ({fst p |p. p ∈ R} ∪ {snd p |p. p ∈ R})"
        by blast
    qed
    let ?fts = "{Fun f ts|f ts t .  (∃t⊵Fun f ts. t ∈ TRS_terms R)}"
    term "{Fun f ts| f ts t . (∃t⊵Fun f ts. t ∈ TRS_terms R)}"
    have fin_fun:"finite {Fun f ts| f ts t . ∃t⊵Fun f ts. t ∈ TRS_terms R}" 
    proof-
      have "{uu. ∃f ts t. uu = Fun f ts ∧ (∃t⊵Fun f ts. t ∈ TRS_terms R)} 
        ⊆ {uu. ∃t w. uu = t ∧ w ⊵ t ∧ w ∈ TRS_terms R}" by blast
      thus ?thesis 
        using finite_collect[OF fin] 
          finite_subset[of A "{uu. ∃t w. uu = t ∧ w ⊵ t ∧ w ∈ TRS_terms R}" for A]
        by presburger
    qed
    then have "finite {f map Some ts → Some (Fun f ts)|f ts. ∃t⊵Fun f ts. t ∈ TRS_terms R}"  
    proof-
      have "{f (map Some ts) → Some (Fun f ts)|f ts. ∃t⊵Fun f ts. t ∈ TRS_terms R}
            =
          (λ u. case u of Fun f ts ⇒ (f (map Some ts) → Some (Fun f ts))) ` {Fun f ts| f ts t . (∃t⊵Fun f ts. t ∈ TRS_terms R)}"
        by (smt Collect_cong Term.term.simps(6) setcompr_eq_image)
      then show ?thesis using fin_fun by simp
    qed
    then show ?thesis unfolding trs_to_ta_A_def ta.make_def cmn_ta_rules_def by auto
  qed
  ultimately show "finite (ta_states (trs_to_ta_A R))" 
    unfolding trs_to_ta_A_def ta_states_def ta.make_def
    by (simp add: r_states_def)    
  show  "finite (ta_states (trs_to_ta_B R))"
    using finite_imageI[of "(ta_eps (trs_to_ta_A R))""λt. (snd t, fst t)"] eps
          symmetry_in_G_D[of R] rules  unfolding ta_states_def trs_to_ta_B_def ta.make_def
      by (simp add: r_states_def)    
qed



assumes"(s,t) ∈ (rstep R)"">lemma assumes "(s,t) ∈ (rstep R)"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (rstep R)"
  using assms by blast


assumes"(s,t) ∈ R^*" ">lemma  assumes "(s,t) ∈ R⇧*" 
  shows "(Some t) ∈ ta_res (trs_to_ta_A R) (Var (Some s))"
  using assms 
proof(cases "s = t")
case True
then show ?thesis by fastforce
next
case False
  then show ?thesis
  proof -
have f1: "∀r f ra t ta. ((∃t ta. (t::('a, 'b) Term.term, ta) ∈ r ∧ (f t::('a, 'b) Term.term option, f ta) ∉ ra) ∨ (t, ta) ∉ r⇧*) ∨ (f t, f ta) ∈ ra⇧*"
by (meson rtrancl_map)
obtain tt :: "(('a, 'b) Term.term option × ('a, 'b) Term.term option) set ⇒ (('a, 'b) Term.term ⇒ ('a, 'b) Term.term option) ⇒ (('a, 'b) Term.term × ('a, 'b) Term.term) set ⇒ ('a, 'b) Term.term" and tta :: "(('a, 'b) Term.term option × ('a, 'b) Term.term option) set ⇒ (('a, 'b) Term.term ⇒ ('a, 'b) Term.term option) ⇒ (('a, 'b) Term.term × ('a, 'b) Term.term) set ⇒ ('a, 'b) Term.term" where
f2: "∀x2 x3 x4. (∃v5 v6. (v5, v6) ∈ x4 ∧ (x3 v5, x3 v6) ∉ x2) = ((tt x2 x3 x4, tta x2 x3 x4) ∈ x4 ∧ (x3 (tt x2 x3 x4), x3 (tta x2 x3 x4)) ∉ x2)"
  by moura
  have "(tt {(Some t, Some ta) |t ta. (t, ta) ∈ R} Some R, tta {(Some t, Some ta) |t ta. (t, ta) ∈ R} Some R) ∉ R ∨ (Some (tt {(Some t, Some ta) |t ta. (t, ta) ∈ R} Some R), Some (tta {(Some t, Some ta) |t ta. (t, ta) ∈ R} Some R)) ∈ {(Some t, Some ta) |t ta. (t, ta) ∈ R}"
by blast
then have "(Some s, Some t) ∈ {(Some t, Some ta) |t ta. (t, ta) ∈ R}⇧*"
  using f2 f1 by (meson assms)
  then show ?thesis
    by (simp add: trs_to_ta_A_def)
qed  
qed


lemma conv_adpvars_G:
  assumes "ground s"
             "s  ⊴ t ∧ t ∈ TRS_terms R"
 shows "(Some s) ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
  using assms 
proof(induction s)
  case (Fun f  ss)
  have 0:"∀i < length ss. (map (ta_res (trs_to_ta_A R)) (map adapt_vars ss))!i 
                                = (ta_res (trs_to_ta_A R) (adapt_vars (ss!i)))"
    by simp
    hence 1:"adapt_vars (Fun f ss) = Fun f (map adapt_vars ss)" by force
  {fix i
    assume i: "i < length ss"
    hence "ground (ss!i)" using Fun(2) by simp
    moreover have "(ss!i) ⊴ t ∧ t ∈ TRS_terms R" using Fun(3)
      by (meson ‹i < length ss› nth_mem supteq.refl supteq.subt supteq_trans) 
    moreover have "adapt_vars (ss!i) = (ss!i)" 
      by (simp add: adapt_vars_id calculation(1))
    ultimately have "Some (ss!i) ∈ ta_res (trs_to_ta_A R) (adapt_vars (ss!i))"
      using Fun(1) i by fastforce} note ref = this
  have "f (map Some ss) →  Some (Fun f ss) ∈ ta_rules (trs_to_ta_A R)"
    unfolding trs_to_ta_A_def cmn_ta_rules_def  TRS_terms_def
    by (metis (mono_tags, lifting) CollectI Fun.prems(2) TRS_terms_def ta_make_simps(1)) 
   
  thus ?case
  proof-
    have "(∀ i < length ss. (map Some ss) ! i ∈ (map (ta_res (trs_to_ta_A R)) (map adapt_vars ss))!i)"
      using ref by simp
    moreover have "f (map Some ss) →  Some (Fun f ss) ∈ ta_rules (trs_to_ta_A R)"
      by (simp add: ‹f map Some ss → Some (Fun f ss) ∈ ta_rules (trs_to_ta_A R)›)
    ultimately show ?thesis using 1 by force
  qed
qed (fastforce)



lemma conv_adpvars_D:
  assumes "ground s"
             "s  ⊴ t ∧ t ∈ TRS_terms R"
 shows "(Some s) ∈ ta_res (trs_to_ta_B R) (adapt_vars s)"
  using assms 
proof(induction s)
  case (Fun f  ss)
  have 0:"∀i < length ss. (map (ta_res (trs_to_ta_B R)) (map adapt_vars ss))!i 
                                = (ta_res (trs_to_ta_B R) (adapt_vars (ss!i)))"
    by simp
    hence 1:"adapt_vars (Fun f ss) = Fun f (map adapt_vars ss)" by force
  {fix i
    assume i: "i < length ss"
    hence "ground (ss!i)" using Fun(2) by simp
    moreover have "(ss!i) ⊴ t ∧ t ∈ TRS_terms R" using Fun(3)
      by (meson ‹i < length ss› nth_mem supteq.refl supteq.subt supteq_trans) 
    moreover have "adapt_vars (ss!i) = (ss!i)" 
      by (simp add: adapt_vars_id calculation(1))
    ultimately have "Some (ss!i) ∈ ta_res (trs_to_ta_B R) (adapt_vars (ss!i))"
      using Fun(1) i by fastforce} note ref = this
  have "f (map Some ss) →  Some (Fun f ss) ∈ ta_rules (trs_to_ta_B R)"
    unfolding trs_to_ta_A_def cmn_ta_rules_def  TRS_terms_def
    by (metis (mono_tags, lifting) CollectI Fun.prems(2) cmn_ta_rules_def ta_make_simps(1) trs_to_ta_B_def)
    thus ?case
  proof-
    have "(∀ i < length ss. (map Some ss) ! i ∈ (map (ta_res (trs_to_ta_B R)) (map adapt_vars ss))!i)"
      using ref by simp
    moreover have "f (map Some ss) →  Some (Fun f ss) ∈ ta_rules (trs_to_ta_B R)"
      
      by (simp add: ‹f map Some ss → Some (Fun f ss) ∈ ta_rules (trs_to_ta_B R)›)
    ultimately show ?thesis using 1 by force
  qed
qed (fastforce)


assumes"ground u" ">lemma assumes "ground u" 
  shows "adapt_vars u = u"
  using assms
  by (simp add: adapt_vars_id) 
lemma ground_ctxt:
  assumes "ground  C⟨s⟩"
  shows "ground s"
  using assms by simp

assumes"q ∈ ta_res TA t"">lemma assumes "q ∈ ta_res TA t"
  shows "Var q ∈ ta_res' TA t"
  using assms 
  by (simp add: ta_res_res'_inclusion)

(*The following theorem gives a map from rstep acceptance to gtt_acceptance*)

lemma rstep_to_gtt_accept:
  assumes "ground_trs R" "ground u" "ground v" "(u, v) ∈ (rstep R)"
  shows "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (abs u) (abs v)"
  using assms(4,3,2,1)
 proof(induction rule:rstepE)
   case (rstep C σ s t)
   let ?𝒢 = "(trs_to_ta_A R, trs_to_ta_B R)"
   let ?C = "adapt_vars_ctxt C"
   let ?s = "adapt_vars s"
   let ?t = "adapt_vars t"
   have grnd_s_t:"ground s" "ground t" using rstep(1,6) unfolding ground_trs_def by fastforce+
  hence 1:"(Some t) ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
   proof-
     from rstep have "(Some s, Some t) ∈ ta_eps (trs_to_ta_A R)" unfolding trs_to_ta_A_def 
       by (metis (mono_tags, lifting) mem_Collect_eq ta_make_simps(2))  
     hence s_res:"(Some t) ∈ ta_res (trs_to_ta_A R) (Var (Some s))" by auto
     have "Some s ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
       using grnd_s_t(1) rstep(1) conv_adpvars_G[of s s R] 
       unfolding TRS_terms_def TRS_fst_def by auto
     hence loc:"Var (Some s) ∈ ta_res' (trs_to_ta_A R) (adapt_vars s)"
       using ta_res_res'_inclusion[of "Some s" "(trs_to_ta_A R)" "adapt_vars s"] by blast
     thus ?thesis using ta_res'_ta_res[OF "loc" "s_res"] by argo
   qed   
   hence 2:"(Some t) ∈ ta_res (trs_to_ta_B R) (adapt_vars t)"
   proof-
     have t_res:"(Some t) ∈ ta_res (trs_to_ta_B R) (Var (Some t))"
       unfolding trs_to_ta_B_def trs_to_ta_B_def using rule by simp  
     have "Some t ∈ ta_res (trs_to_ta_B R) (adapt_vars t)"
       using grnd_s_t(2) rstep(1) conv_adpvars_D[of t t R] 
       unfolding TRS_terms_def TRS_snd_def by auto
     hence loc:"Var (Some t) ∈ ta_res' (trs_to_ta_B R) (adapt_vars t)"
       using ta_res_res'_inclusion[of "Some t" "(trs_to_ta_B R)" "adapt_vars t"] by blast
     thus ?thesis using ta_res'_ta_res[OF "loc" "t_res"]  by argo
   qed
   with 1 have IH:"gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (adapt_vars s) (adapt_vars t)"
     by force
   moreover have u_v:"u = C⟨s⟩" "v = C⟨t⟩"  using grnd_s_t ground_subst_apply rstep(2,3) by metis+
   ultimately have "gtt_accept' ?𝒢 (adapt_vars u) (adapt_vars v)"
      proof-
     have loc:"(?C)⟨?s⟩  = adapt_vars u"
          "(?C)⟨?t⟩  = adapt_vars v"
       using u_v by simp+
     moreover have "fill_holes (mctxt_of_ctxt ?C) [?s] = ?C⟨?s⟩"
                   "fill_holes (mctxt_of_ctxt ?C) [?t] = ?C⟨?t⟩"
                          using fill_holes_mctxt_of_ctxt by blast+
     ultimately show ?thesis 
       using accept'_closed_ctxt[of "[adapt_vars s]" "[adapt_vars t]" "?𝒢" 
            "mctxt_of_ctxt (adapt_vars_ctxt C)"] 
             IH
       by (simp add:loc gtt_accept_equiv) 
   qed
   thus ?thesis using gtt_accept_equiv by blast
 qed



lemma ground_rstep_domain:
  assumes "ground_trs R" "(a,b) ∈ (rstep R)" "ground b"
  shows "ground a"
  using assms(2,1,3) 
proof(induction rule:rstepE)
  case (rstep C σ l r)
  have grnd:"ground l" "ground r" using rstep(1,4) unfolding ground_trs_def by fast+
  have "a = C⟨l⟩" " b = C⟨r⟩"
    using rstep(2) ground_subst_apply[OF grnd(1)] apply presburger
    using rstep(3) ground_subst_apply[OF grnd(2)] by presburger
  then show ?case using rstep(5) grnd
    using ground_ctxt_apply by blast 
qed


lemma rstep_trancl_to_gtt_trancl: assumes "ground_trs R" "finite R"
  shows  "(Restr (abs_R ((rstep R)⇧*)) {t. ground t}) 
              ⊆ gtt_lang (𝒢⇩N (trs_to_ta_A R) (trs_to_ta_B R))"
proof-
  {fix s t
   assume asm:"(s,t) ∈ (Restr (abs_R ((rstep R)⇧*)) {t. ground t})"
   hence grnd:"ground s" "ground t" by blast+
   define u v where u_v:"u = rep s" "v = rep t"
   moreover then have rep:"(u, v) ∈((rstep R)⇧*)"
     by (smt IntE Pair_inject adapt_vars_reverse asm grnd(1) grnd(2) imageE prod.collapse) 
   hence grnd':"ground u" "ground v" using grnd unfolding u_v by force+
    have "(abs u, abs v) ∈ ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)"
     using rep grnd' assms(1)
   proof(induction u v rule:rtrancl.induct)
     case (rtrancl_refl a)
     then show ?case by blast
   next
     case (rtrancl_into_rtrancl a b c)
     hence  grnd:"ground b" using ground_rstep_domain[of R b c] by fast
     hence  "(GTT_TRS.abs a, GTT_TRS.abs b) ∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*"
       using rtrancl_into_rtrancl(3,4,6) by blast
     moreover have " (GTT_TRS.abs b, GTT_TRS.abs c) 
                          ∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))"
       using grnd rtrancl_into_rtrancl(2,5,6) rstep_to_gtt_accept[of R b c]
       by auto
     ultimately show ?case 
       by (meson rtrancl.rtrancl_into_rtrancl)
   qed
   hence "(s, t) ∈ ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)"
     using u_v 
     by (simp add: u_v(1) u_v(2) grnd(1) grnd(2))
   moreover have "(s, t) ∈  {t. ground t} ×  {t. ground t}"
     using grnd by blast
   ultimately have "
(s, t) ∈ Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)  {t. ground t}"
     by blast
 }
  then have "(Restr (abs_R ((rstep R)⇧*)) {t. ground t}) 
              ⊆ Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)  {t. ground t}"
    by blast
  then show ?thesis using  finite_ta_states[OF assms(2)] 𝒢⇩N_lang[of "trs_to_ta_A R" "trs_to_ta_B R"] 
    by presburger               
qed
(* The following set of theorem are useful in showing that gtt acceptance 
implies an rstep relation. We prove a set of theorem for the ground tree tranducer G, 
and replicate it for D*)

lemma Some_ta_res: assumes "q ∈ ta_res (trs_to_ta_A R) s" "ground_trs R" "ground s"
      shows "∃p. q =  Some p" 
using assms 
proof(induction s arbitrary: q)
  case (Var x)
  then show ?case by simp
next
  case (Fun f ss)
  then obtain q' qs where q'_qs:"(f qs → q') ∈ ta_rules (trs_to_ta_A R)"
    "(q',q) ∈ ((ta_eps (trs_to_ta_A R))^*)" 
    "length qs = length ss" 
    "(∀ i < length ss. qs ! i ∈ (map (ta_res (trs_to_ta_A R)) ss) ! i)"
    by auto 
  then have "∃p'. q' = Some p'" unfolding trs_to_ta_A_def 
    by (smt CollectD cmn_ta_rules_def ta_make_simps(1) ta_rule.inject)
  then show ?case using q'_qs(2) unfolding trs_to_ta_A_def
    by (smt CollectD Pair_inject rtranclE ta_make_simps(2))  
qed


lemma Some_ta_res_D: assumes "q ∈ ta_res (trs_to_ta_B R) s" "ground_trs R" "ground s"
      shows "∃p. q =  Some p" 
using assms 
proof(induction s arbitrary: q)
  case (Var x)
  then show ?case by simp
next
  case (Fun f ss)
  then obtain q' qs where q'_qs:"(f qs → q') ∈ ta_rules (trs_to_ta_B R)"
    "(q',q) ∈ ((ta_eps (trs_to_ta_B R))^*)" 
    "length qs = length ss" 
    "(∀ i < length ss. qs ! i ∈ (map (ta_res (trs_to_ta_B R)) ss) ! i)"
    by auto 
  then have "∃p'. q' = Some p'" unfolding trs_to_ta_B_def 
    by (smt CollectD cmn_ta_rules_def ta_make_simps(1) ta_rule.inject)
  then show ?case using q'_qs(2) unfolding trs_to_ta_B_def
    by (smt CollectD Pair_inject rtranclE ta_make_simps(2))  
qed

lemma ta_eps_tranclp_G:
  assumes "(a , b) ∈ (ta_eps (trs_to_ta_A R))^+" 
  shows  "∃l r. (a = Some l ∧ b = Some r) ∧ (l, r) ∈ R⇧+ " using assms  
proof(induction rule: trancl_induct)
  case base
  then show ?case   unfolding trs_to_ta_A_def ta.make_def 
    by auto  
next
  case (step c b)
  then obtain  l r' where l:"(a = Some l ∧ c = Some r')""(l, r') ∈ R⇧+" by blast
  then obtain r where "(b = Some r) ∧ (r', r) ∈ R " using step(2) 
    unfolding trs_to_ta_A_def make_def by auto
  then show ?case using l by auto  
qed 

lemma ta_eps_rtraclp_G:
  assumes  "(Some l , Some r) ∈ (ta_eps (trs_to_ta_A R))^*"
  shows "(l, r) ∈ R⇧*" using assms
proof (cases "Some l = Some r")
  case False 
  hence "(Some l , Some r) ∈ (ta_eps (trs_to_ta_A R))^+" using assms
    by (meson rtranclD)
  hence "(l, r) ∈ R⇧+" using ta_eps_tranclp_G by blast 
  then show ?thesis by fast 
qed (blast)   
  

lemma ta_res_G_rstep:
  assumes "ground_trs R" "ground s"
    "Some q ∈ ta_res (trs_to_ta_A R) s"
  shows "(adapt_vars s, q) ∈ (rstep R)⇧*" 
  using assms(3,2,1)
proof(induction s arbitrary: q)
  case (Var x)
  then show ?case by simp 
next
  case (Fun f ss)
  then obtain qs q' where q'_qs:" (f qs → q') ∈ ta_rules (trs_to_ta_A R)" 
    "(q', Some q) ∈ ((ta_eps (trs_to_ta_A R))^*)" 
    "length qs = length ss" 
    "∀ i < length ss. qs ! i ∈ (ta_res (trs_to_ta_A R) (ss!i))" by auto
  have grnd:"∀i< length ss. ground (ss!i)" using Fun(3) by auto
  hence "∀i<length qs. ∃x. Some x = qs ! i"
    using  Some_ta_res q'_qs(3,4) assms(1) 
    by metis 
  then obtain ps where ps:"(qs = map Some ps)" 
    using construct_exI'[of "length qs" "λ x i. Some x = (qs!i)"]
    by (metis map_nth_eq_conv)      
  {fix i
    assume i:"i < length ss"
    hence "(adapt_vars (ss!i), (ps!i)) ∈ (rstep R)⇧*"
      using Fun(1) ps q'_qs(3,4) grnd assms(1) by auto}
  hence "(Fun f (map adapt_vars ss), Fun f ps) ∈ (rstep R)⇧*"
    by (metis (mono_tags, lifting) args_rsteps_imp_rsteps length_map nth_map ps q'_qs(3))
  hence 1:"(adapt_vars (Fun f ss), Fun f ps) ∈ (rstep R)⇧*"
    using Fun(3) by simp
  have "(f (map Some ps)  →  q') ∈ ta_rules (trs_to_ta_A R)"
    using q'_qs(1) ps by blast
  hence "q' = Some (Fun f ps)" unfolding trs_to_ta_A_def ta.make_def cmn_ta_rules_def
    by fastforce
  then have "(Some (Fun f ps), Some q) ∈ (ta_eps (trs_to_ta_A R))^*" using q'_qs(2) by argo
  then have "(Fun f ps, q) ∈ R⇧*" using ta_eps_rtraclp_G by blast
  with 1 show ?case
    by (smt rtranclD rtrancl_trancl_trancl subset_rstep trancl_into_rtrancl trancl_mono)
qed


(*Replicating above theorems for the case D*)

lemma ta_eps_tranclp_D:
  assumes "(a , b) ∈ (ta_eps (trs_to_ta_B R))^+" 
  shows  "∃l r. (a = Some r ∧ b = Some l) ∧ (l, r) ∈ R⇧+ " using assms  
proof(induction rule: trancl_induct)
  case base
  then show ?case unfolding trs_to_ta_B_def ta.make_def 
    by auto  
next
  case (step c b)
  then obtain  r l' where l:"(a = Some r ∧ c = Some l')""(l', r) ∈ R⇧+" by blast
  then obtain l where "(b = Some l) ∧ (l, l') ∈ R " using step(2) 
    unfolding trs_to_ta_B_def make_def by auto
  then show ?case using l by auto  
qed 

lemma ta_eps_rtraclp_D:
  assumes  "(Some l, Some r) ∈ (ta_eps (trs_to_ta_B R))^*"
  shows "(r, l) ∈ R⇧*" using assms
proof (cases "Some l = Some r")
  case False 
  hence "(Some l , Some r) ∈ (ta_eps (trs_to_ta_B R))^+" using assms
    by (meson rtranclD)
  hence "(r, l) ∈ R⇧+" using ta_eps_tranclp_D by blast   
  then show ?thesis by fast 
qed (blast)   
  

lemma ta_res_D_rstep:
  assumes "ground_trs R" "ground t"
    "Some q ∈ ta_res (trs_to_ta_B R) t"
  shows "(q, adapt_vars t) ∈ (rstep R)⇧*" 
  using assms(3,2,1)
proof(induction t arbitrary: q)
  case (Var x)
  then show ?case by simp 
next
  case (Fun f ts)
  then obtain qs q' where q'_qs:" (f qs → q') ∈ ta_rules (trs_to_ta_B R)" 
    "(q', Some q) ∈ ((ta_eps (trs_to_ta_B R))^*)" 
    "length qs = length ts" 
    "∀ i < length ts. qs ! i ∈ (ta_res (trs_to_ta_B R) (ts!i))" by auto
  have grnd:"∀i< length ts. ground (ts!i)" using Fun(3) by auto
  hence "∀i<length qs. ∃x. Some x = qs ! i"
    using  Some_ta_res_D[of "qs ! i" R "ts ! i" for i] q'_qs(3,4) assms(1)
    by metis  
  then obtain ps where ps:"(qs = map Some ps)" 
    using construct_exI'[of "length qs" "λ x i. Some x = (qs!i)"]
    by (metis map_nth_eq_conv)      
  {fix i
    assume i:"i < length ts"
    hence "(ps!i, adapt_vars (ts!i)) ∈ (rstep R)⇧*"
      using Fun(1) ps q'_qs(3,4) grnd assms(1) by auto}
  hence "(Fun f ps, Fun f (map adapt_vars ts)) ∈ (rstep R)⇧*"
    by (metis (mono_tags, lifting) args_rsteps_imp_rsteps length_map nth_map ps q'_qs(3))
  hence 1:"(Fun f ps, adapt_vars (Fun f ts)) ∈ (rstep R)⇧*"
    using Fun(3) by simp
  have "(f (map Some ps)  →  q') ∈ ta_rules (trs_to_ta_B R)"
    using q'_qs(1) ps by blast
  hence "q' = Some (Fun f ps)" unfolding trs_to_ta_B_def ta.make_def cmn_ta_rules_def
    by fastforce
  then have "(Some (Fun f ps), Some q) ∈ (ta_eps (trs_to_ta_B R))^*" using q'_qs(2) by argo
  then have "(q, Fun f ps) ∈ R⇧*" using ta_eps_rtraclp_D  by blast
  with 1 show ?case
    by (smt rtranclD rtrancl_trancl_trancl subset_rstep trancl_into_rtrancl trancl_mono)
qed

lemma gtt_accept_to_rstep_rtrancl:
  assumes "ground_trs R" "ground u" "ground v"  
          "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) u  v"
  shows "(rep u, rep v) ∈ (rstep R)⇧*"
  using assms(4,3,2,1)
 proof(induction rule:gtt_accept.induct)
  case (refl t)
  then show ?case by force
next
  case (join q s t)
  obtain p where p:"Some p =  q" 
    using Some_ta_res[of q R s] join(1,4,5) unfolding fst_conv by blast 
  then have "(adapt_vars s, p) ∈ (rstep R)⇧*" 
    using ta_res_G_rstep[of R s p] join(1,4,5) 
    unfolding fst_conv by blast
  moreover have "(p, adapt_vars t) ∈ (rstep R)⇧*" 
    using ta_res_D_rstep[of R t p] join(2,3,5) p 
    unfolding snd_conv by blast
  ultimately show ?case by fastforce  
next
  case (ctxt ss ts f)
  have ad_Fun:"adapt_vars (Fun f ss) = Fun f  (map adapt_vars ss)" 
              "adapt_vars (Fun f ss) = Fun f  (map adapt_vars ss)"
    using ctxt(4,5) by simp+
  {fix i
   assume i:"i < length ss"
   with ctxt have "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (ss ! i) (ts ! i)"
    by (auto elim:gtt_accept.cases)
  moreover have "ground (ss!i) ∧ ground (ts!i)" using i ctxt(1,3,4) by force
  ultimately have "(adapt_vars (ss ! i), adapt_vars (ts ! i)) ∈ (rstep R)⇧*"
    using ctxt(2,5) i by blast}
  with ad_Fun show ?case 
    using args_rsteps_imp_rsteps[of "map adapt_vars ss" "map adapt_vars ts" R f]
    by (simp add: ctxt.hyps)
qed
(*Might want to shorten the proof lemma before*)
lemma abs_R_rtrancl:
  assumes "ground a" "ground b" "ground c" "(a, b) ∈ abs_R (R⇧*)" "(b, c) ∈ abs_R (R⇧*)" 
  shows "(a, c)  ∈ abs_R (R⇧*)" 
proof-
  obtain a' b' c' where obt:"a = abs a'" "b = abs b'" "c = abs c'"
    using assms by blast
  then have "(a',b') ∈ R⇧*" using assms(1,2,4)
    by (smt adapt_vars_reverse fst_conv image_iff relcompE rtrancl_idemp_self_comp snd_conv)  
  moreover have "(b',c') ∈ R⇧*" using assms(2,3,5) obt(2,3)
    by (smt adapt_vars_reverse fst_conv image_iff relcompE rtrancl_idemp_self_comp snd_conv) 
  ultimately have "(a',c') ∈ R⇧*" by fastforce
  then show ?thesis using obt(1,3)  
    by (metis (mono_tags, lifting) fst_conv obt(1) obt(3) rev_image_eqI snd_conv)
qed

lemma gtt_lang_to_rstep_rtrancl:
  assumes "ground_trs R" "finite R"
  shows  "gtt_lang (𝒢⇩N (trs_to_ta_A R) (trs_to_ta_B R)) ⊆ (Restr (abs_R ((rstep R)⇧*)) {t. ground t})"
proof-
  have "Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)  {t. ground t}
    ⊆   (Restr (abs_R ((rstep R)⇧*)) {t. ground t})"
  proof-
    {fix u v
      assume asm:"(u,v) ∈  Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)  {t. ground t}"
      then have grnd:"ground u" "ground v" by blast+
      moreover have u_v:"(u,v) ∈ ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*)"
        using asm by fast
      have "(u,v) ∈ (abs_R ((rstep R)⇧*))"
        using u_v grnd assms
      proof(induction u v rule: rtrancl.induct)
        case (rtrancl_refl a)
        hence "abs (rep a) = a" by auto
        moreover have "(rep a, rep a) ∈ (rstep R)⇧*" by blast
        ultimately show ?case
          by (metis (mono_tags, lifting) fst_conv rev_image_eqI snd_conv)  
      next
        case (rtrancl_into_rtrancl a b c)
        then have grnd_b:"ground b" by force
        hence 1:"(a, b) ∈ abs_R ((rstep R)⇧*)"
          using rtrancl_into_rtrancl(3,4,6,7) by fast
        have "(rep b, rep c) ∈ ((rstep R)⇧*)"
          using  grnd_b rtrancl_into_rtrancl(2,5,6) gtt_accept_to_rstep_rtrancl by blast
        hence "(b, c) ∈ abs_R ((rstep R)⇧*)"
          using grnd_b rtrancl_into_rtrancl(5)
          by (smt adapt_vars_adapt_vars fst_conv rev_image_eqI snd_conv) 
        with 1 show ?case using abs_R_rtrancl rtrancl_into_rtrancl(4,5) grnd_b by blast
      qed
      hence "(u,v) ∈  (Restr (abs_R ((rstep R)⇧*)) {t. ground t})"
        using grnd by blast}
    thus ?thesis by blast
  qed
  thus ?thesis using  finite_ta_states[OF assms(2)] 𝒢⇩N_lang[of "trs_to_ta_A R" "trs_to_ta_B R"] 
    by presburger
qed

(*Main Theorem*)
lemma reachability_gtt_equiv:
  assumes "ground_trs R" "finite R"
  shows  "gtt_lang (𝒢⇩N (trs_to_ta_A R) (trs_to_ta_B R)) 
                    = (Restr (abs_R ((rstep R)⇧*)) {t. ground t})"
  using gtt_lang_to_rstep_rtrancl[OF assms] rstep_trancl_to_gtt_trancl[OF assms]
  by auto




end