theory LLRG_Confluence imports Ground_Confluence Ord.Signature_Extension LV_to_GTT begin definition llrg :: "('f,'v) trs ⇒ bool" where "llrg R ≡ ∀s ∈ R. (linear_term (fst s) ∧ ground (snd s))" primrec inv_const :: "('f × nat) ⇒ 'v ⇒ ('f,'v) term ⇒ ('f, 'v) term" where "inv_const g y (Var x) = (Var x)" | "inv_const g y (Fun f ss) = (if (Fun f ss = Fun (fst g) []) then (Var y) else (Fun f (map (inv_const g y) ss)))" fun inv_const_ctxt :: "('f × nat) ⇒ 'v ⇒ ('f,'v) ctxt ⇒ ('f, 'v) ctxt" where "inv_const_ctxt g y Hole = Hole" | "inv_const_ctxt g y ((More f ss1 C ss2)) = (More f (map (inv_const g y) ss1) (inv_const_ctxt g y C) (map (inv_const g y) ss2))" definition subin :: "('f,'v) subst ⇒('f × nat) ⇒ 'v ⇒ ('f, 'v) subst" where "subin f (g::('f × nat)) (y::'v) = (λ (t::'v). inv_const g y (f t))" lemma inv_cons_sigma: fixes g:: "'f" defines "σ ≡ λ t. Fun g []" assumes "ground u" shows "(inv_const (g,0) y u) ⋅ σ = u" using assms proof (induction u) case (Fun f ss) {fix i assume i:"i < length ss" hence "ground (ss!i)" using Fun(3) by auto hence "inv_const (g, 0) y (ss!i) ⋅ σ = (ss!i)" using Fun(1,2) i by force} then show ?case by (smt σ_def fst_conv inv_const.simps(2) length_map map_nth_eq_conv subst_apply_term.simps(1) subst_apply_term.simps(2)) qed (simp) lemma subst_sig: assumes "funas_term u ⊆ F" shows "funas_term (u ⋅ (λ t. Fun g [])) ⊆ F ∪ {(g,0)}" using assms apply (induction u) apply simp by fastforce lemma rstep_sig_extn: assumes "(u, v) ∈ (sig_step F (rstep R))" shows "(u ⋅ (λ t. Fun g []), v ⋅ (λ t. Fun g [])) ∈ (sig_step (F ∪ {(g,0)}) (rstep R))" using subst_sig[of _ F] assms unfolding sig_step_def by auto lemma rstep_trancl_sig_extn: assumes "(u, v) ∈ (sig_step F (rstep R))^*" shows "(u ⋅ (λ t. Fun g []), v ⋅ (λ t. Fun g [])) ∈ (sig_step (F ∪ {(g,0)}) (rstep R))^*" using assms proof (induction rule:rtrancl_induct) case (step v w) have "(v ⋅ (λ t. Fun g []), w ⋅ (λ t. Fun g [])) ∈ (sig_step (F ∪ {(g,0)}) (rstep R))" using rstep_sig_extn[OF step(2)] . thus ?case using step(3) by simp qed (simp) lemma subst_filter: fixes g::"'f" and y::"'v" defines σ:"σ ≡ (λ t. Fun g [])" assumes "ground (u ⋅ ρ)" shows "(u ⋅ ρ) = (u ⋅ (subin ρ (g,0) y)) ⋅ σ" using assms proof (induction "u ⋅ ρ" arbitrary: u) case (Var x) then show ?case unfolding subin_def by force next case (Fun f ss) then show ?case proof (cases u) case (Var z) hence ic:"(u ⋅ (subin ρ (g,0) y)) = inv_const (g,0) y (Fun f ss)" unfolding subin_def Fun by auto moreover have "(inv_const (g,0) y (Fun f ss)) ⋅ σ = Fun f ss" using inv_cons_sigma[of "Fun f ss" g y] Fun(2,4) unfolding σ by argo ultimately have "u ⋅ subin ρ (g, 0) y ⋅ σ = Fun f ss" by argo then show ?thesis unfolding Fun(2)[symmetric] by argo next case (Fun h ts) hence ts_ss:"h = f" "length ss = length ts" using Fun.hyps(2) by fastforce+ { fix i assume i:"i < length ss" hence ts_i:"(ts!i) ⋅ ρ = (ss!i)" using ts_ss Fun.hyps(2) unfolding Fun by simp moreover have "ground (ss!i)" using Fun.prems i unfolding Fun.hyps(2)[symmetric] by auto ultimately have "(ts!i) ⋅ ρ = (ts!i) ⋅ subin ρ (g, 0) y ⋅ σ" using Fun.hyps(1,3) by (metis σ i nth_mem)} then show ?thesis using Fun ts_ss by (smt map_eq_conv' nth_map subst_apply_term.simps(2) term.distinct(1) term.sel(4) weak_match.elims(2) weak_match_match) qed qed lemma inv_const_filter_funas: fixes g::"'f" and y::"'v" and u::"('f,'v) term" defines σ:"σ ≡ (λ t. Fun g [])" assumes "funas_term u ⊆ F ∪ {(g,0)}" "(g,0) ∉ F" shows "funas_term (inv_const (g,0) y u) ⊆ F" using assms proof (induction u) case (Fun f ss) then show ?case proof (cases "f = g ∧ ss = []") case True hence "inv_const (g,0) y (Fun f ss) = Var y" by simp then show ?thesis by (metis empty_subsetI funas_term.simps(1)) next case False hence "(f,length ss) ≠ (g,0)" by fastforce hence f:"(f, length ss) ∈ F" using Fun(3) by auto {fix i assume i:"i < length ss" hence "funas_term (ss!i) ⊆ F ∪ {(g, 0)}" using Fun(3) funas_term.simps(2)[of f ss] by force hence "funas_term (inv_const (g,0) y (ss!i)) ⊆ F" using Fun(1-4) i by auto} hence "∀i < length ss. funas_term (inv_const (g,0) y (ss!i)) ⊆ F" by blast hence "⋃set (map funas_term (map (inv_const (g,0) y) ss)) ⊆ F" apply simp proof - assume a1: "∀i<length ss. funas_term (inv_const (g, 0) y (ss ! i)) ⊆ F" obtain nn :: "('f, 'v) Term.term list ⇒ ('f, 'v) Term.term ⇒ nat" where "∀x0 x1. (∃v2<length x0. x1 = x0 ! v2) = (nn x0 x1 < length x0 ∧ x1 = x0 ! nn x0 x1)" by moura then have f2: "∀t ts. t ∉ set ts ∨ nn ts t < length ts ∧ t = ts ! nn ts t" by (meson in_set_idx) obtain tt :: "('f, 'v) Term.term set ⇒ (('f, 'v) Term.term ⇒ ('f × nat) set) ⇒ ('f × nat) set ⇒ ('f, 'v) Term.term" where "∀x0 x1 x2. (∃v3. x2 = x1 v3 ∧ v3 ∈ x0) = (x2 = x1 (tt x0 x1 x2) ∧ tt x0 x1 x2 ∈ x0)" by moura then have f3: "∀P f T. P ∉ f ` T ∨ P = f (tt T f P) ∧ tt T f P ∈ T" by (meson imageE) obtain PP :: "('f × nat) set ⇒ ('f × nat) set set ⇒ ('f × nat) set" where "∀x0 x1. (∃v2. v2 ∈ x1 ∧ ¬ v2 ⊆ x0) = (PP x0 x1 ∈ x1 ∧ ¬ PP x0 x1 ⊆ x0)" by moura then have f4: "∀P Pa. PP Pa P ∈ P ∧ ¬ PP Pa P ⊆ Pa ∨ ⋃P ⊆ Pa" by (meson Union_least) moreover { assume "funas_term (inv_const (g, 0) y (ss ! nn ss (tt (set ss) (funas_term ∘ inv_const (g, 0) y) (PP F ((funas_term ∘ inv_const (g, 0) y) ` set ss))))) ⊆ F" then have "UNION (set ss) (funas_term ∘ inv_const (g, 0) y) ⊆ F ∨ (PP F ((funas_term ∘ inv_const (g, 0) y) ` set ss) ≠ (funas_term ∘ inv_const (g, 0) y) (tt (set ss) (funas_term ∘ inv_const (g, 0) y) (PP F ((funas_term ∘ inv_const (g, 0) y) ` set ss))) ∨ tt (set ss) (funas_term ∘ inv_const (g, 0) y) (PP F ((funas_term ∘ inv_const (g, 0) y) ` set ss)) ∉ set ss) ∨ PP F ((funas_term ∘ inv_const (g, 0) y) ` set ss) ∉ (funas_term ∘ inv_const (g, 0) y) ` set ss ∨ PP F ((funas_term ∘ inv_const (g, 0) y) ` set ss) ⊆ F" using f4 f2 by (metis (no_types) comp_def) } ultimately show "UNION (set ss) (funas_term ∘ inv_const (g, 0) y) ⊆ F" using f3 f2 a1 by meson qed then show ?thesis using f funas_term.simps(2)[of f "map (inv_const (g,0) y) ss"] by (metis (no_types, lifting) Un_insert_left empty_subsetI funas_term.elims insert_subset inv_const.simps(2) length_map sup_bot.left_neutral term.distinct(1)) qed qed (simp) lemma inv_contxt_const: "inv_const (g, 0) y C⟨s⟩ = (inv_const_ctxt (g,0) y C)⟨inv_const (g, 0) y s⟩" proof (induction C) case (More f ss1 C ss2) let ?C' = "More f ss1 C ss2" let ?ss1 = "map (inv_const (g,0) y) ss1" let ?ss2 = "map (inv_const (g,0) y) ss2" let ?C = "inv_const_ctxt (g,0) y C" have "?C'⟨s⟩ ≠ Fun g []" by simp hence 1:"inv_const (g, 0) y ?C'⟨s⟩ = (Fun f (map (inv_const (g,0) y) (ss1@C⟨s⟩#ss2)))" by force hence 2:"... = (Fun f (?ss1@(inv_const (g,0) y C⟨s⟩)#?ss2))" by simp with More have 3: "... = (Fun f (?ss1@ ?C⟨inv_const (g, 0) y s⟩ #?ss2))" by blast hence 4:"... = (More f ?ss1 ?C ?ss2)⟨inv_const (g, 0) y s⟩" by auto hence 5:"... = (inv_const_ctxt (g,0) y (More f ss1 C ss2))⟨inv_const (g, 0) y s⟩" by simp thus ?case using 1 2 3 4 by argo qed (auto) lemma inv_const_subst: assumes "funas_term s ⊆ F" "(g,0) ∉ F" shows "inv_const (g, 0) y (s ⋅ ρ) = s ⋅ (subin ρ (g,0) y)" using assms proof (induction s) case (Fun f ss) then show ?case proof (cases "f = g ∧ ss = []") case True then show ?thesis using Fun by (simp add: Fun.IH) next case False let ?ss = "map (λi. i ⋅ ρ) ss" have "(Fun f ss) ⋅ ρ = Fun f ?ss" by force hence 1:"inv_const (g, 0) y ((Fun f ss) ⋅ ρ) = Fun f (map (inv_const (g,0) y) ?ss)" using False by force {fix i assume i:"i < length ss" hence "funas_term (ss!i) ⊆ F" using Fun(2) by fastforce with i Fun(1,3) have "inv_const (g, 0) y (?ss!i) = (ss!i) ⋅ subin ρ (g, 0) y" by force} with 1 show ?thesis by (smt length_map map_eq_conv' subst_apply_term.simps(2)) qed qed (simp add: subin_def) lemma inv_const_rstep: assumes "funas_trs R ⊆ F" "(s,t) ∈ (rstep R)" "(g,0) ∉ F" shows "(inv_const (g,0) y s, inv_const (g,0) y t) ∈ (rstep R)" using assms(2,1,3) proof (induction rule: rstepE) case (rstep s t C ρ l r) let ?ρ = " (subin ρ (g,0) y)" let ?ic = "inv_const (g, 0) y" have funas: "funas_term l ⊆ F" "funas_term r ⊆ F" using rstep(3,6) unfolding funas_trs_def funas_rule_def by force+ hence 1:"?ic (l ⋅ ρ) = l ⋅ ?ρ" "?ic (r ⋅ ρ) = r ⋅ ?ρ" using rstep(7) by (simp_all add: inv_const_subst) hence "(?ic (l ⋅ ρ), ?ic (r ⋅ ρ)) ∈ rstep R" using rstep(3) by auto hence "((inv_const_ctxt (g,0) y C)⟨?ic (l ⋅ ρ )⟩, (inv_const_ctxt (g,0) y C)⟨?ic (r ⋅ ρ)⟩) ∈ rstep R" by blast then show ?case using inv_contxt_const[symmetric] by (simp add: ‹⋀y s g C. (inv_const_ctxt (g, 0) y C)⟨inv_const (g, 0) y s⟩ = inv_const (g, 0) y C⟨s⟩› rstep.hyps(1,2,4,5)) qed lemma vars_term_funas_term: assumes "x ∈ vars_term t" "(Var x) ⋅ σ = Fun f ss" shows "(f, length ss) ∈ funas_term (t ⋅ σ)" using assms proof (induction t) case (Var y) have "x = y" using Var(1) by simp then show ?case using assms(2) by auto next case (Fun g ts) obtain i where i:"i < length ts" "x ∈ vars_term (ts!i)" using Fun(2) using var_imp_var_of_arg by force hence ts_i:"(ts!i) ∈ set ts" by simp have f_len:"(f, length ss) ∈ funas_term (ts!i ⋅ σ)" using Fun(1)[OF ts_i i(2) Fun(3)] . moreover have "(ts!i ⋅ σ) ⊴ (Fun g ts ⋅ σ)" using i(1) by simp hence "funas_term (ts!i ⋅ σ) ⊆ funas_term (Fun g ts ⋅ σ)" using supteq_imp_funas_term_subset by blast then show ?case using i(1) f_len using Fun.IH Fun.prems(2) i(2) nth_mem by blast qed lemma const_ctxt: assumes "C⟨s⟩ = Fun f []" shows "C = Hole ∧ s = Fun f []" using assms by (metis ctxt.cop_nil nectxt_imp_supt_ctxt supt_const) lemma const_subst: assumes "l ⋅ ρ = Fun g []" shows "is_Var l ∨ l = Fun g []" using assms proof (cases l) case (Fun f ss) hence "f = g ∧ ss = []" using assms by force then show ?thesis using Fun by meson qed (fast) lemma Fun_ctxt_closed: assumes "(u,v) ∈ rstep R" shows "(Fun f (ss@(u#ts)), Fun f (ss@(v#ts))) ∈ rstep R" using assms by (simp add: ctxt_closed_one ctxt_closed_rstep) lemma funas_subterm: assumes "funas_term (Fun f ss) ⊆ F" shows "∀i< length ss. funas_term (ss!i) ⊆ F" using assms by fastforce lemma funas_term_take_drop: assumes "funas_term (Fun f ss) ⊆ F" "n ≤ length ss" shows "⋃(set (map funas_term (take n ss))) ⊆ F" "⋃(set (map funas_term (drop n ss))) ⊆ F" using assms set_take_subset apply fastforce by (metis (no_types, lifting) Sup_le_iff assms(1) drop_map funas_term.simps(2) in_set_dropD le_sup_iff) lemma subst_seq: assumes "u ⋅ σ = l ⋅ ρ" "funas_term u ⊆ F" "funas_term l ⊆ F" "(h, 0) ∉ F" "σ = (λ t. Fun h [])" "is_Fun u" "linear_term l" shows "∃ ρ'. u = l ⋅ ρ'" using assms proof (induction l arbitrary: u) case (Var x) have "u = Var x ⋅ (λ t. u)" by force then show ?case by blast next case (Fun g ts) have ts_subst:"Fun g ts ⋅ ρ = Fun g (map (λ t. t ⋅ ρ) ts)" by auto obtain f ss where f_ss:"u = Fun f ss" using Fun(7) by auto have lhs:"u ⋅ σ = Fun f (map (λ t. t ⋅ σ) ss)" using f_ss by force hence eq:"g = f ∧ length ss = length ts" using ts_subst Fun(2) f_ss by (metis map_eq_imp_length_eq term.inject(2)) {fix i assume i:"i < length ts" have ss_ts_i:"ss!i ⋅ σ = ts!i ⋅ ρ" using eq lhs ts_subst by (metis Fun.prems(1) i map_nth_conv term.sel(4)) hence "∃ρ⇩i. (ss!i) = (ts!i) ⋅ ρ⇩i" proof (cases "ss!i") case (Var y) hence "ss!i ⋅ σ = Fun h []" using Fun(6) by (simp add: Var) hence "ts!i ⋅ρ = Fun h []" using ss_ts_i by simp hence conj:"is_Var (ts!i) ∨ (ts!i) = Fun h []" using const_subst by fast {assume asm: "ts!i = Fun h []" hence "funas_term (ts!i) = {(h,0)}" by auto moreover have "funas_term (ts!i) ⊆ F" using i Fun(4) by fastforce ultimately have "(h,0) ∈ F" by simp hence False using Fun(5) by argo }note contr= this with conj obtain w where "ts!i = Var w" by blast then have "ss!i = (ts!i) ⋅ (λ t. Var y)" using Var by fastforce then show ?thesis by fast next case (Fun f' ss') have "funas_term (ss!i) ⊆ F" using f_ss Fun.prems(2) i eq by fastforce moreover have "funas_term (ts!i) ⊆ F" using Fun.prems(3) i by force moreover have "is_Fun (ss!i)" using Fun by simp moreover have "linear_term (ts!i)" using Fun.prems(7) i by force ultimately show ?thesis using ss_ts_i i Fun.prems(4,5) Fun.IH[of "ts!i" "ss!i"] by force qed} from this obtain r where r:"(ss!i) = (ts!i) ⋅ (r i)" if "i < length ts" for i by metis define rs where "rs= map r [0..<length ts]" then have rs:"∀i < length ts. (ss!i) = (ts!i) ⋅ (rs!i) ∧ length rs = length ts" using r by auto then obtain ρ' where " ∀i < length ts. (ts!i) ⋅ (rs!i) = (ts!i) ⋅ ρ'" using Fun(8) subst_unification_list[of ts rs] by auto hence "∀i < length ts. (ss!i) = (ts!i) ⋅ ρ'" using rs by presburger hence "Fun f ss = (Fun f ts) ⋅ ρ'" using f_ss by (simp add: ‹∀i<length ts. ss ! i = ts ! i ⋅ ρ'› ‹u = Fun f ss› eq nth_equalityI) then show ?case using f_ss eq by blast qed lemma subst_commute_rstep: fixes u v assumes "σ = (λ x. (Fun g []))" "funas_trs R ⊆ F" "(g, 0) ∉ F" "(v ⋅ σ, u) ∈ rstep R" "llrg R" "funas_term v ⊆ F" "funas_term u ⊆ F ∪ {(g,0)}" shows "∃u'. (v ,u') ∈ rstep R ∧ (u = u' ⋅ σ) ∧ funas_term u' ⊆ F" using assms(4,1,2,3,5,6,7) proof (induction v arbitrary: u) case (Var x) hence "(Fun g [], u) ∈ rstep R" by simp hence " (∃u'. ((Var x, u') ∈ rstep R) ∧ (u = u' ⋅ σ) ∧ funas_term u' ⊆ F)" using Var proof (induction rule:rstepE) case (rstep s t C ρ l r) hence C_Hole:"C = Hole" using const_ctxt by metis hence "u = r ⋅ ρ" using rstep(2,5) by auto moreover have grnd:"ground r" using rstep(3) Var(5) unfolding llrg_def by auto ultimately have u_r:"u = r" using ground_subst_apply by blast hence u_funas:"funas_term u ⊆ F" using rstep(3,8) unfolding funas_trs_def funas_rule_def snd_conv by fastforce from C_Hole have "l ⋅ ρ = Fun g []" by (simp add: rstep.hyps(1,4)) hence l:"is_Var l ∨ l = Fun g []" using const_subst by fast have "is_Var l" using l proof (cases "is_Var l") case False hence "l = Fun g []" using l by fast hence "(g,0) ∈ funas_trs R" using rstep(3) unfolding funas_trs_def funas_rule_def by fastforce then show ?thesis using rstep(8,9) by blast qed (auto) then obtain y where "l = Var y" by fast then have "(Var y, r) ∈ R" using u_r rstep(3) by simp then have "(Var y ⋅(λ y. Var x), r ⋅ (λ y. Var x)) ∈ rstep R" by fast hence "(Var x, r) ∈ rstep R" using grnd by (simp add: ground_subst_apply) moreover have "u = r ⋅ σ" using grnd u_r by(simp add:ground_subst_apply) ultimately show ?case using rstep u_funas grnd by (metis u_r) qed then show ?case by blast next case (Fun f ss) show ?case using Fun(2) proof (induction rule:rstepE) case (rstep s t C ρ l r) hence grnd:"ground r" using Fun(6) unfolding llrg_def by (metis snd_conv) define ss' where ss':"ss' = map (λi. (i ⋅σ)) ss" hence ss'_Fun:"Fun f ss ⋅ σ = Fun f ss'" by simp then show ?case proof (cases C) case Hole hence u:"u = r" using grnd rstep.hyps(2,5) by (simp add: rstep.hyps(3) ground_subst_apply) have eq:"Fun f ss ⋅ σ= l ⋅ ρ" using rstep(1,4) Hole by (metis ctxt.cop_nil) moreover have funas_l:"funas_term l ⊆ F" using Fun(4) rstep(3) unfolding funas_trs_def funas_rule_def by force ultimately obtain ρ' where ρ': "Fun f ss = l ⋅ ρ'" using subst_seq[OF eq Fun(7) funas_l Fun(5,3)] rstep(3) Fun(6) unfolding llrg_def by (metis fst_conv is_FunI) hence "(l ⋅ ρ', r ⋅ ρ') ∈ rstep R" using rstep(3) by fast hence "(Fun f ss, r) ∈ rstep R" using grnd ρ' by (simp add: ρ' ground_subst_apply) moreover have "r ⋅ σ = u" using u grnd by (simp add: u ground_subst_apply) moreover have "funas_term r ⊆ F" using rstep(3) Fun(4) unfolding funas_trs_def funas_rule_def by force ultimately show ?thesis by blast next case (More h ss1 C' ss3) hence "Fun f ss' = Fun h (ss1@(C'⟨l ⋅ ρ⟩)#ss3)" using ss'_Fun rstep by auto hence h_f:"h = f ∧ ss' = (ss1@(C'⟨l ⋅ ρ⟩)#ss3)" by simp hence "ss'!(length ss1) = (C'⟨l ⋅ ρ⟩)" by simp hence ss_i:"ss!(length ss1) ⋅ σ = (C'⟨l ⋅ ρ⟩)" using ss' by (smt ‹h = f ∧ ss' = ss1 @ C'⟨l ⋅ ρ⟩ # ss3› length_map map_eq_Cons_D map_eq_append_split nth_append_length) with h_f have u:"u = Fun f (ss1@(C'⟨r ⋅ ρ⟩)#ss3)" using More by (simp add: ‹ss ! length ss1 ⋅ σ = C'⟨l ⋅ ρ⟩› rstep.hyps(2,5)) have rstep_ind:"(ss!(length ss1) ⋅ σ, C'⟨r ⋅ ρ⟩) ∈ rstep R" using ss_i rstep(3) by blast moreover have len:"length ss1 < length ss" using h_f proof - have f1: "∀ts. ss1 @ (ss' ! length ss1 # ss3) @ ts = ss' @ ts" using h_f by auto have f2: "length ss = length ss'" using ss' by auto have "length ss1 ≠ length ss'" using f1 by (metis (full_types) append_Cons append_Cons_nth_middle ctxt_apply_eq_False) then show ?thesis using f2 f1 by (metis (no_types) append_Cons append_Cons_nth_left append_Cons_nth_middle ctxt_apply_eq_False nat_neq_iff) qed hence "length ss1 < length ss'" using ss' by simp moreover have "funas_term (ss!length ss1) ⊆ F" "funas_term (C'⟨r ⋅ ρ⟩) ⊆ F ∪ {(g,0)}" using len Fun(7) funas_subterm[of f ss] apply simp using len Fun(7,8) funas_subterm[of f "(ss1@(C'⟨r ⋅ ρ⟩)#ss3)"] by (simp add: More rstep.hyps(2,5)) ultimately obtain u' where u':"(ss!(length ss1), u') ∈ rstep R ∧( C'⟨r ⋅ ρ⟩ = u' ⋅ σ) ∧ funas_term u' ⊆ F" using rstep_ind Fun(1,3-6) using ‹length ss1 < length ss› by fastforce moreover have breakup:"(take (length ss1) ss)@((ss!(length ss1))#(drop (length ss1+1) ss)) = ss" using h_f ss' using ‹length ss1 < length ss› id_take_nth_drop by fastforce hence ss1_ss3:"map (λ i. i ⋅ σ) (take (length ss1) ss) = ss1" "map (λ i. i ⋅ σ) (drop (length ss1+1) ss) = ss3" using ss' h_f apply (simp add: h_f append_eq_conv_conj take_map) using ss' h_f id_take_nth_drop ‹length ss1 < length ss› by (metis (no_types, lifting) One_nat_def ‹length ss1 < length ss'› add.right_neutral add_Suc_right append_eq_conv_conj drop_map list.inject) let ?ss1 = "(take (length ss1) ss)" let ?ss3 = "(drop (length ss1+1) ss)" let ?u' = "?ss1@(u'#?ss3)" have "(Fun f ss, Fun f ?u') ∈ rstep R" using u' breakup Fun_ctxt_closed[of "ss ! length ss1" u' R f ?ss1 ?ss3] by presburger moreover have "(Fun f (?u')) ⋅ σ = u" using ss1_ss3 u' u by auto moreover have "funas_term (Fun f ?u') ⊆ F" using breakup Fun(7) proof - have "⋃(set (map funas_term ?u')) = (⋃ set (map funas_term ?ss1) ∪ (funas_term u') ∪ (⋃ set (map funas_term ?ss3)))" by force moreover have "⋃ set (map funas_term ?ss1) ⊆ F" using funas_term_take_drop[OF Fun(7)] len by simp moreover have "(funas_term u') ⊆ F" using u' by simp moreover have "⋃ set (map funas_term ?ss3) ⊆ F" using funas_term_take_drop[OF Fun(7)] len by simp ultimately have "⋃(set (map funas_term ?u')) ⊆ F" by blast moreover have "(f, length ss) ∈ F" using Fun(7) by simp ultimately show ?thesis by (smt Fun.prems(6) breakup funas_term.simps(2) le_sup_iff length_append list.size(4)) qed ultimately show ?thesis by blast qed qed qed lemma subst_commute_sig_step: fixes u v assumes "σ = (λ x. (Fun g []))" "funas_trs R ⊆ F" "(g, 0) ∉ F" "(v ⋅ σ, u) ∈ sig_step (F∪{(g,0)}) (rstep R)" "llrg R" "funas_term v ⊆ F" shows "∃u'. (v ,u') ∈ sig_step F (rstep R) ∧ (u = u' ⋅ σ)" using subst_commute_rstep[OF assms(1-3)] assms unfolding sig_step_def by blast lemma subst_commute_sig_step_rtrancl: fixes u v assumes "σ = (λ x. (Fun g []))" "funas_trs R ⊆ F" "(g, 0) ∉ F" "(v ⋅ σ, u) ∈ (sig_step (F∪{(g,0)}) (rstep R))^*" "llrg R" "funas_term v ⊆ F" shows "∃u'. (v ,u') ∈ (sig_step F (rstep R))^* ∧ (u = u' ⋅ σ)" using assms(4,1,2,3,5,6) proof (induction rule:rtrancl_induct) case (step y z) then obtain u⇩1 where u⇩1:"(v, u⇩1) ∈ (sig_step F (rstep R))⇧*" "y = u⇩1 ⋅ σ" by blast hence tran:"(u⇩1 ⋅ σ, z) ∈ (sig_step (F∪{(g,0)}) (rstep R))" using step.hyps(2) by blast have funas_u⇩1:"funas_term u⇩1 ⊆ F" using u⇩1(1) step(8) unfolding sig_step_def apply (induction rule:rtrancl_induct) by simp+ show ?case using subst_commute_sig_step[OF step(4,5,6) tran step(7) funas_u⇩1] proof - show ?thesis by (meson u⇩1(1) ‹∃u'. (u⇩1, u') ∈ sig_step F (rstep R) ∧ z = u' ⋅ σ› rtrancl.rtrancl_into_rtrancl) qed qed (fast) lemma varposs_subterm_extrc: assumes "p ∈ varposs (Fun f ts)" shows "∃ i q. i < length ts ∧ p = i # q ∧ q ∈ varposs(ts!i)" using assms by auto lemma var_tracing: assumes "(s,t) ∈ rstep R" "llrg R" "p ∈ varposs t" shows "t |_ p = s |_ p ∧ p ∈ varposs s" using assms proof (induction rule:rstepE) case (rstep s t C σ l r) show ?case using rstep(3-) unfolding rstep(1,2) proof (induction C arbitrary:s t p) case Hole hence "t = r ⋅ σ" by force moreover have grnd:"ground r" using rstep(3,6) Hole(1) unfolding llrg_def by fastforce ultimately have "t = r" by (simp add: ground_subst_apply) with grnd have "varposs t = {}" by (metis Hole.prems(5) empty_iff ground_vars_term_empty subt_at_imp_supteq subteq_Var_imp_in_vars_term varposs_iff) then show ?case using Hole(5) by blast next case (More f ss1 C' ss2) define ss where ss: "ss= (ss1@(C'⟨l ⋅ σ⟩)#ss2)" define ts where ts: "ts = (ss1@(C'⟨r ⋅ σ⟩)#ss2)" with More ss have s_t:"t = Fun f ts" "s = Fun f ss" by (meson ctxt_apply_term.simps(2))+ from More(6) s_t(1) obtain i q where i_q: "i < length ts ∧ p = i # q ∧ q ∈ varposs(ts!i)" using varposs_subterm_extrc[of p f ts] by blast then show ?case proof (cases "i = length (ss1)") case True hence ss_ts_i:"ss!i = (C'⟨l ⋅ σ⟩)" "ts!i = (C'⟨r ⋅ σ⟩)" using ss ts by simp+ hence "s|_ p = (C'⟨l ⋅ σ⟩)|_q" "t|_p = (C'⟨r ⋅ σ⟩)|_ q" using s_t i_q apply auto[1] by (simp add: ‹ts ! i = C'⟨r ⋅ σ⟩› i_q s_t(1)) with More(1)[of "C'⟨l ⋅ σ⟩" "C'⟨r ⋅ σ⟩" q] More(5) i_q ss_ts_i(2) show ?thesis proof - have "q ∈ varposs C'⟨r ⋅ σ⟩" using ‹ts ! i = C'⟨r ⋅ σ⟩› i_q by presburger then show ?thesis by (metis ‹⟦(l, r) ∈ R; C'⟨l ⋅ σ⟩ = C'⟨l ⋅ σ⟩; C'⟨r ⋅ σ⟩ = C'⟨r ⋅ σ⟩; llrg R; q ∈ varposs C'⟨r ⋅ σ⟩⟧ ⟹ C'⟨r ⋅ σ⟩ |_ q = C'⟨l ⋅ σ⟩ |_ q ∧ q ∈ varposs C'⟨l ⋅ σ⟩› ‹s |_ p = C'⟨l ⋅ σ⟩ |_ q› ‹t |_ p = C'⟨r ⋅ σ⟩ |_ q› i_q length_append list.size(4) poss_Cons_poss rstep.hyps(3) rstep.prems(1) s_t(2) ss ss_ts_i(1) term.sel(4) ts varposs_iff) qed next case False hence "ts!i = ss!i" using ss ts i_q by (simp add: append_Cons_nth_not_middle) moreover have "t|_ (i#q) = (ts!i)|_q" using s_t(1) i_q by simp moreover have "s|_ (i#q) = (ss!i)|_q" using s_t(2) i_q by auto ultimately have "t|_ (i#q) = s|_ (i#q)" by argo then show ?thesis using i_q by (metis ‹t |_ (i # q) = ts ! i |_ q› ‹ts ! i = ss ! i› length_append list.size(4) poss_Cons_poss s_t(2) ss term.sel(4) ts varposs_iff) qed qed qed lemma var_tracing_rtrancl: assumes "(s,t) ∈ (rstep R)^*" "llrg R" "p ∈ varposs t" shows "t |_ p = s |_ p ∧ p ∈ varposs s" using assms proof (induction rule:rtrancl_induct) case (step y z) have 1:"z |_ p = y |_ p ∧ p ∈ varposs y" using var_tracing[OF step(2,4,5)] . hence "y |_ p = s |_ p ∧ p ∈ varposs s" using step(3)[OF step(4)] by simp thus ?case using 1 by argo qed (simp) lemma var_tracing_sig_step: assumes "(s,t) ∈ sig_step F (rstep R)" "llrg R" "p ∈ varposs t" shows "t |_ p = s |_ p ∧ p ∈ varposs s" using assms var_tracing unfolding sig_step_def by blast lemma var_tracing_sig_step_rtrancl: assumes "(s,t) ∈ (sig_step F (rstep R))^*" "llrg R" "p ∈ varposs t" shows "t |_ p = s |_ p ∧ p ∈ varposs s" using var_tracing_rtrancl var_tracing_sig_step assms unfolding sig_step_def by (smt assms(1) rtranclD set_rev_mp sig_stepE trancl_into_rtrancl trancl_sig_subset) lemma in_eq_poss: assumes "s ≠ t" shows "∃p. s|_ p ≠ t |_ p ∧ p ∈ poss s ∩ poss t" using assms by (metis IntI empty_pos_in_poss subt_at.simps(1)) lemma in_eq_poss_funposs_eq: assumes "s ≠ t" "funposs s = funposs t" "∀p ∈ funposs s. s |_ p = t |_ p" shows "∃p. s|_ p ≠ t |_ p ∧ p ∈ varposs s ∩ varposs t" using in_eq_poss[OF assms(1)] assms(2) proof - obtain p where p:" s|_ p ≠ t |_ p ∧ p ∈ poss (s) ∩ poss (t)" using in_eq_poss[OF assms(1)] by blast hence or:"p ∈ funposs s ∨ p ∈ varposs s" "p ∈ funposs t ∨ p ∈ varposs t" using poss_simps apply blast by (metis Diff_Diff_Int Diff_cancel Diff_iff Int_Diff Int_empty_right Un_iff assms(2) empty_iff funposs_mctxt_mctxt_of_term p poss_simps(2) set_funposs_list) {assume asm:"p ∈ funposs s" hence False using assms(3) p by blast} hence 1:"p ∈ varposs s" using or by satx {assume asm:"p ∈ funposs t" hence False using assms(2,3) p by blast} with 1 p show ?thesis using or(2) by blast qed lemma funposs_subterm_extrc: assumes "p ∈ funposs (Fun f ts)" shows "p = [] ∨ (∃ i q. i < length ts ∧ p = i # q ∧ q ∈ funposs (ts ! i))" using assms funposs.simps(2)[of f ts] apply simp by blast lemma funposs_empty: assumes "p ∈ funposs (Fun f ts)" shows "p = [] ⟹ (Fun f ts) |_ p = Fun f ts" using assms by auto lemma funposs_subterm_extrc2: assumes "p ∈ funposs (Fun f ts)" "p ≠ []" shows "(∃ i q. i < length ts ∧ (p = i # q) ∧ q ∈ funposs(ts!i))" using assms funposs.simps(2)[of f ts] apply simp by blast lemma varposs_distinct: fixes u :: "('f, 'v) term" and g defines "σ ≡ λy. (Fun g [] :: ('f, 'v) term)" assumes "u ⋅ σ = v ⋅ σ" "funas_term u ⊆ F" "funas_term v ⊆ F" "(g, 0) ∉ F" "u ≠ v" shows "(∃p ∈ varposs u ∩ varposs v. u |_ p ≠ v |_ p)" using assms proof (induction u arbitrary: v) case (Var x) have "Var x ⋅ σ = Fun g []" by (simp add: σ_def) with Var(2) have "v ⋅ σ = Fun g []" by (force simp: σ_def) hence v:"v = Fun g [] ∨ is_Var v" by fastforce { assume asm:"v = Fun g []" hence "(g,0) ∈ funas_term v" by auto hence "(g,0) ∈ F" using Var(4) by fast hence False using Var(5) by simp } with v obtain y where y:"v = Var y" by fast hence "y ≠ x" using Var(6) by simp hence "(Var x) |_ [] ≠ (Var y) |_ []" by simp thus ?case using y by fastforce next case (Fun f ss) have Fun_eq:"(Fun f (map (λ t. t ⋅ σ) ss)) = v ⋅ σ " using Fun(3) unfolding subst_apply_term.simps(2) . then obtain ts where v:"v = Fun f ts" by (smt Collect_mem_eq Fun.hyps(2) Fun.prems(2) UnCI adapt_vars_simps assms(5) funas_term.elims funas_term.simps(2) insert_iff length_map list.map_disc_iff list.simps(8) list.size(3) subsetCE subst_apply_term.simps(1) subst_apply_term.simps(2) subst_apply_term_empty term.distinct(1) term.inject(2) term.sel(4)) have list_eq:"(map (λ t. t ⋅ σ) ss) = (map (λ t. t ⋅ σ) ts)" using Fun_eq unfolding v unfolding subst_apply_term.simps(2) by force hence len_eq:"length ss = length ts" using map_eq_conv' by blast from Fun(7) v obtain i where i:"i < length ss" "(ss!i) ≠ (ts!i)" using len_eq nth_equalityI by blast with list_eq len_eq have "(ss!i) ⋅ σ = (ts!i) ⋅ σ" by (meson map_eq_conv') moreover have "funas_term (ss!i) ⊆ F" "funas_term (ts!i) ⊆ F" using i len_eq Fun(4,5) unfolding v by force+ ultimately obtain q where q:"q ∈ varposs(ss!i) ∩ varposs(ts!i) ∧ (ss!i) |_ q ≠ (ts!i) |_ q" using Fun(1)[of "ss!i" "ts!i"] using i Fun(2,6) by fastforce hence "i#q ∈ varposs (Fun f ss)" "i#q ∈ varposs (Fun f ts)"using i len_eq by simp+ moreover have "(Fun f ss) |_ (i#q) = (ss!i) |_ q " using i(1) q by auto moreover have "(Fun f ts) |_ (i#q) = (ts!i) |_ q" using i(1) len_eq q by auto ultimately show ?case using q unfolding v by (metis IntI) qed lemma funas_extn: fixes g :: 'f and s :: "('f,'v) term" assumes "(funas_term s) ⊆ F" "(g,0) ∉ F" shows "funas_term (s ⋅ (λ y. Fun g [])) ⊆ (F ∪ {(g,0)})" using assms by (induction s) (simp, fastforce) lemma sig_step_rtrancl: assumes "(s,t) ∈ (sig_step (F) (rstep R))^*" shows "(s,t) ∈ (rstep R)^*" using assms apply (induction rule:rtrancl_induct) apply simp unfolding sig_step_def by auto lemma sig_step_rtrancl_conv: fixes g :: 'f defines σ: "σ ≡ λy. (Fun g [] :: ('f, 'v) term)" assumes "(s :: ('f,'v) term,t) ∈ (sig_step (F) (rstep R))^*" "(g, 0) ∉ F" shows "(s ⋅ σ ,t ⋅ σ) ∈ (sig_step (F ∪ {(g,0)}) (rstep R))^*" using assms(2,1,3) proof (induction rule:rtrancl_induct) case (step u v) hence 1:"(s ⋅ σ, u ⋅ σ) ∈ (sig_step (F ∪ {(g, 0)}) (rstep R))⇧*" by blast have u_v:"(u,v) ∈ rstep R" "funas_term u ⊆ F" "funas_term v ⊆ F" using step(2) unfolding sig_step_def by force+ hence "(u ⋅ σ, v ⋅ σ) ∈ (rstep R)" using rsteps_closed_subst by auto hence "(u ⋅ σ, v ⋅ σ) ∈ (sig_step (F ∪ {(g, 0)}) (rstep R))" unfolding sig_step_def using funas_extn[OF u_v(2) step(5)] funas_extn[OF u_v(3) step(5)] σ by fast with 1 show ?case by simp qed (blast) lemma funas_rtrancl: assumes "funas_term s ⊆ F" "(s, t) ∈ (sig_step F (rstep R))⇧*" shows "funas_term t ⊆ F" using assms(2,1) by (induction rule:rtrancl_induct) (auto) lemma GCR_implies_CR: fixes R :: "('f,'v) trs" assumes "(g,0) ∉ F" "CR_on (sig_step (F ∪ {(g,0)}) (rstep R)) {s. ground s ∧ funas_term s ⊆ F ∪ {(g,0)}}" "llrg R" "funas_trs R ⊆ F" shows "CR (sig_step F (rstep R))" proof - define σ where σ: "σ = (λ (y::'v) . (Fun g [] :: ('f, 'v) term))" define r where r: "r = (sig_step (F) (rstep R))" define r' where r': "r' = (sig_step (F∪{(g,0)}) (rstep R))" {fix s::"('f,'v) term" fix u::"('f,'v) term" fix v::"('f,'v) term" assume asm: "(s, u) ∈ r⇧* ∧ (s, v) ∈ r⇧*" hence neq_funas:"(s ≠ u) ∨ (s ≠ v) ⟹ (funas_term s ⊆ F) ∧ (funas_term u ⊆ F) ∧ (funas_term v ⊆ F)" unfolding r sig_step_def rtrancl_def by (metis (no_types, lifting) asm converse_rtranclE r rtrancl.simps sig_stepE) from asm have rstep_s: "(s, u) ∈ (rstep R)^*" "(s, v) ∈ (rstep R)^*" unfolding r using sig_step_rtrancl by auto have "(u,v) ∈ join r" proof (cases "(s = u) ∧ (s = v)") case False hence "(s ≠ u) ∨ (s ≠ v)" by blast hence funas_subs: "(funas_term s ⊆ F)" "(funas_term u ⊆ F)" "(funas_term v ⊆ F)" using neq_funas by auto have ground:"ground (s ⋅ σ)" "ground (u ⋅ σ)" "ground (v ⋅ σ)" unfolding σ by fastforce+ have funas_rel: "funas_term (s ⋅ σ) ⊆ F ∪ {(g,0)}" "funas_term (u ⋅ σ) ⊆ F ∪ {(g,0)}" "funas_term (v ⋅ σ) ⊆ F ∪ {(g,0)}" unfolding σ using funas_extn[OF funas_subs(1) assms(1)] funas_extn[OF funas_subs(2) assms(1)] funas_extn[OF funas_subs(3) assms(1)]. have meet_gcr:"(s ⋅ σ, u ⋅ σ) ∈ (r')⇧*" "(s ⋅ σ, v ⋅ σ) ∈ (r')⇧*" unfolding r' using asm unfolding r using assms(1) unfolding σ by (intro sig_step_rtrancl_conv; simp)+ hence "(u ⋅ σ, v ⋅ σ) ∈ join r'" using assms(2) funas_rel ground unfolding r' CR_on_def by blast then obtain t' where t':"(u ⋅ σ, t') ∈ r'^* " "(v ⋅ σ, t') ∈ r'^*" by blast then obtain t⇩1 where t1:"(u, t⇩1) ∈ (sig_step F (rstep R))⇧*" "(t' = t⇩1 ⋅ σ)" using subst_commute_sig_step_rtrancl[OF σ assms(4,1)] t'(1) assms(3) unfolding r' using funas_subs(2) by blast moreover obtain t⇩2 where t2:"(v, t⇩2) ∈ (sig_step F (rstep R))⇧*" "(t' = t⇩2 ⋅ σ)" using subst_commute_sig_step_rtrancl[OF σ assms(4,1)] t'(2) assms(3) unfolding r' using funas_subs(3) by blast ultimately have eq:"t⇩1 ⋅ σ = t⇩2 ⋅ σ" by auto have "t⇩1 = t⇩2" proof (rule ccontr) assume ineq_assm:"t⇩1 ≠ t⇩2" then obtain p where p:"p ∈ varposs(t⇩1) ∩ varposs(t⇩2)" "t⇩1 |_ p ≠ t⇩2 |_ p" using varposs_distinct[of t⇩1 g t⇩2 F] eq funas_rtrancl[OF funas_subs(2) t1(1)] funas_rtrancl[OF funas_subs(3) t2(1)] assms(1) unfolding σ by fast have t1_p:"t⇩1 |_ p = u |_ p ∧ p ∈ varposs(u)" using var_tracing_sig_step_rtrancl[OF t1(1) assms(3)] p(1) by blast moreover have u_s:"u |_p = s |_p ∧ p ∈ varposs(s)" using var_tracing_sig_step_rtrancl[of s u F R p] asm t1_p assms(3) unfolding r by blast ultimately have 1:"t⇩1 |_ p = s |_ p" by argo have t2_p:"t⇩2 |_ p = v |_ p ∧ p ∈ varposs(v)" using var_tracing_sig_step_rtrancl[OF t2(1) assms(3)] p(1) by blast moreover have u_s:"v |_p = s |_p ∧ p ∈ varposs(s)" using var_tracing_sig_step_rtrancl[of s v F R p] asm t2_p assms(3) unfolding r by blast ultimately have 2:"t⇩2 |_ p = s |_ p" by argo with p(2) 1 show False by argo qed with t1(1) t2(1) show ?thesis using r joinI by (simp add: ‹t⇩1 = t⇩2›) qed (auto)} thus ?thesis unfolding CR_defs using r by blast qed lemma sig_step_invert: fixes R :: "('f,'v) trs" and g :: 'f and y defines "σ ≡ λ y. (Fun g []::('f, 'v) term)" assumes "(g,0) ∉ F" "funas_trs R ⊆ F" "(s, t) ∈ (sig_step (F∪{(g,0)}) (rstep R))" "ground s" "ground t" shows "((inv_const (g,0) y s) ⋅ σ = s) ∧ ((inv_const (g,0) y t) ⋅ σ = t) ∧ (inv_const (g,0) y s, inv_const (g,0) y t) ∈ (sig_step F (rstep R))" proof - let ?s = "inv_const (g,0) y s" let ?t = "inv_const (g,0) y t" have s'_t'_rstep:"(s,t) ∈ rstep R" using assms(4) unfolding sig_step_def by simp hence s_t_rstep:"(?s,?t) ∈ rstep R" using inv_const_rstep[OF assms(3) "s'_t'_rstep" assms(2)] by (simp) have const_cond:"s = ?s ⋅ σ" "t = ?t ⋅ σ" using inv_cons_sigma[OF assms(5)] inv_cons_sigma[OF assms(6)] unfolding assms(1) by presburger+ have funas_cond: "funas_term s ⊆ F ∪ {(g,0)}" "funas_term t ⊆ F ∪ {(g,0)}" using assms(4) unfolding sig_step_def by simp+ hence "funas_term ?s ⊆ F" "funas_term ?t ⊆ F" using inv_const_filter_funas[of s F g] inv_const_filter_funas[of t F g] assms(2) by simp+ with const_cond s_t_rstep show ?thesis unfolding sig_step_def by (metis (no_types, lifting) case_prodI mem_Collect_eq) qed lemma rstep_ground_llrg: assumes "llrg R" "ground s" "(s,t) ∈ rstep R" shows "ground t" using assms empty_iff ground_vars_term_empty llrg_def prod.sel(2) rstep_ground subsetI by (metis) lemma rstep_ground_llrg_rtrancl: assumes "llrg R" "ground s" "(s,t) ∈ (rstep R)^*" shows "ground t" using assms(3,2,1) apply (induction rule:rtrancl_induct) apply simp using rstep_ground_llrg by fast lemma sig_step_invert_rtrancl: fixes R :: "('f,'v) trs" and g :: 'f defines "σ ≡ λ_. Fun g [] :: ('f, 'v) term" assumes "(g,0) ∉ F" "funas_trs R ⊆ F" "(s, t) ∈ (sig_step (F∪{(g,0)}) (rstep R))^*" "llrg R" "ground s ∧ ground t" shows "((inv_const (g,0) y s) ⋅ σ = s) ∧ ((inv_const (g,0) y t) ⋅ σ = t) ∧ (inv_const (g,0) y s, inv_const (g,0) y t) ∈ (sig_step F (rstep R))^*" using assms(4,1,2,3,5,6) proof (induction rule: rtrancl_induct) case base have "inv_const (g,0) y s ⋅ σ = s" "(inv_const (g,0) y s, inv_const (g,0) y s) ∈ (sig_step F (rstep R))⇧*" using base(5) by (simp_all add: base(1) ground_subst_apply inv_cons_sigma) then show ?case by fast next case (step u t) let ?ic = "inv_const (g,0) y" have "(s, u) ∈ (rstep R)^*" using step(1) unfolding sig_step_def using sig_step_rtrancl step.hyps(1) by blast hence grnd:"ground u" using rstep_ground_llrg_rtrancl step(7,8) by meson hence int:"((?ic s) ⋅ σ = s)" "((?ic u) ⋅ σ = u)" "((?ic s, ?ic u) ∈ (sig_step F (rstep R))⇧*)" using step by blast+ moreover have "((?ic t) ⋅ σ = t)" "((?ic u, ?ic t) ∈ (sig_step F (rstep R))⇧*)" using sig_step_invert[OF step(5,6,2) grnd] step(8) unfolding step(4) by fast+ ultimately show ?case by force qed lemma join_sig_extn: assumes "(u, v) ∈ join (sig_step F (rstep R))" shows "(u ⋅ (λ_. Fun g []), v ⋅ (λ_. Fun g [])) ∈ join (sig_step (F ∪ {(g,0)}) (rstep R))" proof - obtain t where "(u, t) ∈ (sig_step (F) (rstep R))^*" "(v, t) ∈ (sig_step (F) (rstep R))^*" using assms by auto hence "(u ⋅ (λ t. Fun g []), t ⋅ (λ t. Fun g [])) ∈ (sig_step (F ∪ {(g,0)}) (rstep R))^*" "(v ⋅ (λ t. Fun g []), t ⋅ (λ t. Fun g [])) ∈ (sig_step (F ∪ {(g,0)}) (rstep R))^*" using rstep_trancl_sig_extn[of _ _ F] by blast+ thus ?thesis by auto qed lemma CR_implies_GCR: fixes R :: "('f,'v) trs" assumes "(g,0) ∉ F" "CR (sig_step F (rstep R))" "llrg R" "funas_trs R ⊆ F" shows "CR_on (sig_step (F ∪ {(g,0)}) (rstep R)) {s. ground s ∧ funas_term s ⊆ F ∪ {(g,0)}}" proof - fix y let ?ic = "inv_const (g,0) y :: ('f, 'v) term ⇒ _" define S where S:"S = {(s::('f,'v) term). ground s ∧ funas_term s ⊆ (F ∪ {(g,0)})}" { fix s u v assume asm1: "(s,u) ∈ (sig_step (F∪{(g,0)}) (rstep R))^*" "(s,v) ∈ (sig_step (F∪{(g,0)}) (rstep R))^*" assume asm2: "s ∈ S" have grnd:"ground u" "ground v" using rstep_ground_llrg_rtrancl[OF assms(3)] asm1 unfolding sig_step_def asm2 unfolding S by (metis (no_types, lifting) S asm1 asm2 sig_step_rtrancl mem_Collect_eq)+ hence "(?ic s, ?ic u) ∈ (sig_step F (rstep R))^*" "(?ic u ⋅ (λy. Fun g [])) = u" "(?ic s, ?ic v) ∈ (sig_step F (rstep R))^*" "(?ic v ⋅ (λy. Fun g [])) = v" using asm1 asm2 sig_step_invert_rtrancl assms by (simp add: S sig_step_invert_rtrancl)+ hence "(?ic u, ?ic v) ∈ join (sig_step (F) (rstep R))" using assms(2) by blast hence "(?ic u ⋅ (λ t. Fun g []), ?ic v ⋅ (λ t. Fun g [])) ∈ join (sig_step (F∪{(g,0)}) (rstep R))" using join_sig_extn[of _ _ F] by blast hence "(u, v) ∈ join (sig_step (F∪{(g,0)}) (rstep R))" using grnd by (simp add: inv_cons_sigma) } thus ?thesis unfolding S by auto qed lemma CR_GCR_equiv: fixes R :: "('f,'v) trs" assumes "llrg R" "funas_trs R ⊆ F" "(g,0) ∉ F" shows "CR (sig_step F (rstep R)) = CR_on (sig_step (F ∪ {(g,0)}) (rstep R)) {s. ground s ∧ funas_term s ⊆ F ∪ {(g,0)}}" using CR_implies_GCR[of g F] GCR_implies_CR[of g F] assms by blast+ end