Theory CR.Development_Closed

(*
Author:  Christina Kirk (Kohl) <christina.kirk@uibk.ac.at> (2022-2023)
License: LGPL (see file COPYING.LESSER)
*)
theory Development_Closed
imports
  Proof_Terms_Term_Rewriting.Labels_and_Overlaps    
  First_Order_Rewriting.Critical_Pairs
  Weighted_Path_Order.Relations
  First_Order_Terms.Unification_More
  TRS.More_Abstract_Rewriting
  Auxx.Util
begin

context
  fixes ren :: "'v :: infinite renaming2" 
begin
abbreviation "rename_x ≡ map_vars_term (rename_1 ren)"
abbreviation "rename_y ≡ map_vars_term (rename_2 ren)"

lemma inj_rename[simp,intro]: "inj_on (rename_1 ren) S"  "inj_on (rename_2 ren) S" 
  using rename_12[of ren] by (metis injD inj_on_def)+

lemma linear_rename_x: "linear_term s ⟹ linear_term (rename_x s)" 
  by (auto intro!: linear_term_map_inj_on_linear_term)

lemma linear_rename_y: "linear_term s ⟹ linear_term (rename_y s)" 
  by (auto intro!: linear_term_map_inj_on_linear_term)

lemma distinct_vars:
  assumes "linear_term s" "linear_term t"
  shows "distinct (vars_term_list (rename_x s) @ vars_term_list (rename_y t))" (is "distinct (?xs @ ?ys)") 
proof-
  from assms(1) have "linear_term (rename_x s)" by (rule linear_rename_x)
  then have dist1:"distinct ?xs" 
    using linear_term_var_vars_term_list by (metis comp_eq_dest_lhs distinct_remdups distinct_rev)
  from assms(2) have "linear_term (rename_y t)" by (rule linear_rename_y)
  then have dist2:"distinct ?ys" 
    using linear_term_var_vars_term_list by (metis comp_eq_dest_lhs distinct_remdups distinct_rev)
  {fix x assume xs:"x ∈ vars_term (rename_x s)" and xt:"x ∈ vars_term (rename_y t)"
    from xs have "x ∈ range (rename_1 ren)" 
      by (metis image_mono subsetD term.set_map(2) top_greatest)
    moreover from xt have "x ∈ range (rename_2 ren)"
      by (metis image_mono subsetD term.set_map(2) top_greatest)
    ultimately have False using rename_12[of ren] by auto
  }
  then have "set ?xs ∩ set ?ys = {}" 
    unfolding set_vars_term_list by blast 
  with dist1 dist2 show ?thesis by simp
qed

lemma mk_subst_rename_x:
  assumes "length (vars_distinct t) = length xs"
  shows "t ⋅ (mk_subst Var (zip (vars_distinct t) xs)) = (rename_x t) ⋅ (mk_subst Var (zip (vars_distinct (rename_x t)) xs))" 
proof-
  {fix x assume "x ∈ vars_term t" 
    then obtain i where i:"x = (vars_distinct t)!i" "i < length (vars_distinct t)"
      by (metis in_set_conv_nth set_vars_term_list vars_term_list_vars_distinct) 
    with assms have 1:"(mk_subst Var (zip (vars_distinct t) xs)) x = xs!i" 
      using mk_subst_distinct by (metis comp_apply distinct_remdups distinct_rev) 
    have "vars_distinct (rename_x t) = map (rename_1 ren) (vars_distinct t)" 
      unfolding vars_map_vars_term[symmetric] comp_apply
      by (metis distinct_map distinct_remdups distinct_remdups_id inj_rename(1) remdups_map_remdups rev_map) 
    with assms i have 2:"(mk_subst Var (zip (vars_distinct (rename_x t)) xs)) ((rename_1 ren) x) = xs!i"
      by (metis (mono_tags, lifting) comp_apply distinct_remdups distinct_rev length_map mk_subst_same nth_map) 
    from 1 2 have "(mk_subst Var (zip (vars_distinct t) xs)) x = (mk_subst Var (zip (vars_distinct (rename_x t)) xs)) ((rename_1 ren) x)"
      by presburger
  }
  then show ?thesis
    by (simp add: apply_subst_map_vars_term term_subst_eq_conv) 
qed

(*TODO: refactor since this is copy of lemma above!*)
lemma mk_subst_rename_y:
  assumes "length (vars_distinct t) = length xs"
  shows "t ⋅ (mk_subst Var (zip (vars_distinct t) xs)) = (rename_y t) ⋅ (mk_subst Var (zip (vars_distinct (rename_y t)) xs))" 
proof-
  {fix x assume "x ∈ vars_term t" 
    then obtain i where i:"x = (vars_distinct t)!i" "i < length (vars_distinct t)"
      by (metis in_set_conv_nth set_vars_term_list vars_term_list_vars_distinct) 
    with assms have 1:"(mk_subst Var (zip (vars_distinct t) xs)) x = xs!i" 
      using mk_subst_distinct by (metis comp_apply distinct_remdups distinct_rev) 
    have "vars_distinct (rename_y t) = map (rename_2 ren) (vars_distinct t)" 
      unfolding vars_map_vars_term[symmetric] comp_apply
      by (metis distinct_map distinct_remdups distinct_remdups_id inj_rename(2) remdups_map_remdups rev_map) 
    with assms i have 2:"(mk_subst Var (zip (vars_distinct (rename_y t)) xs)) ((rename_2 ren) x) = xs!i"
      by (metis (mono_tags, lifting) comp_apply distinct_remdups distinct_rev length_map mk_subst_same nth_map) 
    from 1 2 have "(mk_subst Var (zip (vars_distinct t) xs)) x = (mk_subst Var (zip (vars_distinct (rename_y t)) xs)) ((rename_2 ren) x)"
      by presburger
  }
  then show ?thesis
    by (simp add: apply_subst_map_vars_term term_subst_eq_conv) 
qed

text‹Define critical peak as pair of two proof terms.›
(*New definition here since the other definition of critical_peaks in Decreasing_Diagrams2 is not 
sufficient (it is not defined for two different TRSs R and S). Using proof terms here to see
if it is simpler than using something like the ('f, 'v) step type in Decreasing_Diagrams2.*)
definition pterm_cpeaks :: "('f,'v) trs ⇒ ('f,'v) trs ⇒ (('f, 'v) pterm × ('f, 'v) pterm) set"
  where "pterm_cpeaks R S = {(C⟨Prule α (map (to_pterm ∘ τ) (var_rule α))⟩, Prule β (map (to_pterm ∘ σ) (var_rule β))) 
  | α β p C σ τ. to_rule α ∈ R ∧ to_rule β ∈ S ∧ p ∈ fun_poss (lhs β) ∧
  C = to_pterm_ctxt (ctxt_of_pos_term p (lhs β ⋅ σ)) ∧ 
  mgu_vd ren ((lhs β)|_p) (lhs α) = Some (σ, τ) }"

lemma pterm_cpeaksI:
  assumes "to_rule α ∈ R" and "to_rule β ∈ S"
    and "p ∈ fun_poss (lhs β)"
    and "mgu_vd ren ((lhs β)|_p) (lhs α) = Some (σ, τ)"
    and "C = to_pterm_ctxt (ctxt_of_pos_term p (lhs β ⋅ σ))"
  shows "(C⟨Prule α (map (to_pterm ∘ τ) (var_rule α))⟩, Prule β (map (to_pterm ∘ σ) (var_rule β))) ∈ pterm_cpeaks R S"
  using assms unfolding pterm_cpeaks_def by blast

lemma pterm_cpeak_rstep1:
  assumes "(A, B) ∈ pterm_cpeaks R S"
  shows "(source A, target A) ∈ rstep R"
proof-
  from assms obtain α β p C σ τ where alpha:"to_rule α ∈ R" and "to_rule β ∈ S"
    and p:"p ∈ fun_poss (lhs β)"
    and C:"C = to_pterm_ctxt (ctxt_of_pos_term p (lhs β ⋅ σ))"
    and A:"A = C⟨Prule α (map (to_pterm ∘ τ) (var_rule α))⟩" 
    unfolding pterm_cpeaks_def by blast
  show ?thesis unfolding A C source_to_pterm_ctxt target_to_pterm_ctxt source.simps target.simps map_map using alpha p
    by (smt (verit, ccfv_SIG) comp_apply map_eq_conv rstep.simps source_to_pterm target_to_pterm) 
qed

lemma pterm_cpeak_rstep2:
  assumes "(A, B) ∈ pterm_cpeaks R S"
  shows "(source B, target B) ∈ rstep S"
proof-
  from assms obtain β σ where beta:"to_rule β ∈ S"
    and B:"B = Prule β (map (to_pterm ∘ σ) (var_rule β))" 
    unfolding pterm_cpeaks_def by blast
  show ?thesis unfolding B source.simps target.simps map_map using beta
    by (smt (verit, ccfv_SIG) comp_apply map_eq_conv rstep_rule rstep_subst source_to_pterm target_to_pterm) 
qed


text‹Connection between proof term peaks and the critical pairs.›
lemma pterm_cpeak_to_critical_pair:
  (*use varcond to avoid strange cases when instantiating the right-hand sides of rules*)
  assumes varcond:"⋀l r. (l, r) ∈ R ∪ S ⟹ vars_term r ⊆ vars_term l" 
  and "(A, B) ∈ pterm_cpeaks R S" 
  shows "(is_Prule A, target A, target B) ∈ critical_pairs ren S R"
proof-
  from assms obtain α β p C σ τ where rules:"to_rule β ∈ S" "to_rule α ∈ R" and
  C:"C = to_pterm_ctxt (ctxt_of_pos_term p (lhs β ⋅ τ))" and fun_poss:"p ∈ fun_poss (lhs β)" and
  mgu:"mgu_vd ren ((lhs β)|_p) (lhs α) = Some (τ, σ)" and
  A:"A = C⟨Prule α (map (to_pterm ∘ σ) (var_rule α))⟩" and 
  B:"B = Prule β (map (to_pterm ∘ τ) (var_rule β))"
    unfolding pterm_cpeaks_def by blast
  let ?l="lhs α" and ?r="rhs α" and ?l'="lhs β" and ?r'="rhs β" and ?l''="(lhs β)|_p" 
  let ?C="ctxt_of_pos_term p ?l'"
  have C_l':"?l' = ?C⟨?l''⟩" 
    using fun_poss by (simp add: ctxt_supt_id fun_poss_imp_poss) 
  have is_Fun:"is_Fun (?l' |_ p)"
    by (simp add: fun_poss fun_poss_fun_conv is_Fun_Fun_conv)  
  have tgt_A:"target A = (?C ⋅⇩c τ)⟨?r ⋅ σ⟩" 
    unfolding A C target_to_pterm_ctxt target.simps using lhs_subst_var_rule varcond rules
    unfolding ctxt_of_pos_term_subst[OF fun_poss_imp_poss[OF fun_poss], symmetric]
    by (smt (verit, ccfv_SIG) List.map.compositionality Un_iff target_empty_apply_subst target_to_pterm to_pterm_empty to_pterm_subst)
  have tgt_B:"target B = ?r' ⋅ τ" unfolding B target.simps using lhs_subst_var_rule varcond rules
    by (smt (verit, del_insts) Un_iff list.map_comp target_empty_apply_subst target_to_pterm to_pterm_empty to_pterm_subst)
  have b:"is_Prule A = (?C = □)" proof(cases p)
    case Nil
    show ?thesis unfolding A C Nil by simp
  next
    case (Cons i p')
    from fun_poss obtain f ts where f:"lhs β = Fun f ts"
      by (metis Cons_poss_Var fun_poss_imp_poss local.Cons term.exhaust_sel)
    show ?thesis 
      unfolding A C Cons f by simp
  qed               
  show ?thesis using critical_pairsI[OF rules C_l' is_Fun mgu tgt_B tgt_A b] .
qed

text‹The set of critical peak steps of TRS S for R.›
definition CPS :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ (('f, 'v) term × ('f, 'v) term) set"
  where "CPS R S = {(s,u). ∃A B. ((A,B) ∈ pterm_cpeaks R S ∨ (B,A) ∈ pterm_cpeaks S R) ∧ 
                    source B = s ∧ target B = u }"

text‹The set of all non-closed critical peak steps of TRS S for R›
definition CPS' :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ (('f, 'v) term × ('f, 'v) term) set"
  where "CPS' R S = {(s,u). ∃A B.(((A,B) ∈ pterm_cpeaks R S ∧ (target A, target B) ∉ mstep S) ∨ 
                                 ((B,A) ∈ pterm_cpeaks S R ∧ (target B, target A) ∉ mstep R)) ∧
                                  source B = s ∧ target B = u }"

lemma CPS'_subset_CPS: "CPS' R S ⊆ CPS R S"
  unfolding CPS'_def CPS_def by auto

text‹The set of all non-closed critical peak steps of TRS S for R, using weakening for overlays›
context
  fixes R S :: "('f, 'v) trs" (*Fix R and S, since order matters here. Only one of the TRSs is allowed to have multiple steps.*)
begin

fun is_R_S_closed :: "(('f, 'v) pterm × ('f, 'v) pterm) ⇒ bool" where
  "is_R_S_closed (A, Prule β Bs) = (∃v. (target A, v) ∈ mstep S ∧ (target (Prule β Bs), v) ∈ (rstep R)⇧*)" (* all cases where root step is on the right, including overlays*)
| "is_R_S_closed (Prule α As, B) = ((target B, target (Prule α As)) ∈ mstep R)"
| "is_R_S_closed _ = False"

definition CPS_R :: "(('f, 'v) term × ('f, 'v) term) set"
  where "CPS_R = {(s,u). ∃A B.((A,B) ∈ pterm_cpeaks R S ∨ (B,A) ∈ pterm_cpeaks S R) ∧ ¬ is_R_S_closed (A,B) ∧ source A = s ∧ target A = u}"

definition CPS_S :: "(('f, 'v) term × ('f, 'v) term) set"
  where "CPS_S = {(s,u). ∃A B.((A,B) ∈ pterm_cpeaks R S ∨ (B,A) ∈ pterm_cpeaks S R) ∧ ¬ is_R_S_closed (A,B) ∧ source B = s ∧ target B = u}"

lemma CPS_stepI:
  assumes "(A, B) ∈ pterm_cpeaks R S" "¬ is_R_S_closed (A,B)"
  shows "(source A, target A) ∈ CPS_R" "(source B, target B) ∈ CPS_S" 
proof-
  from assms show "(source A, target A) ∈ CPS_R" unfolding CPS_R_def by blast
  from assms show "(source B, target B) ∈ CPS_S" unfolding CPS_S_def by blast 
qed

lemma CPS_stepI':
  assumes "(B, A) ∈ pterm_cpeaks S R" "¬ is_R_S_closed (A,B)"
  shows "(source A, target A) ∈ CPS_R" "(source B, target B) ∈ CPS_S" 
proof-
  from assms show "(source A, target A) ∈ CPS_R" unfolding CPS_R_def by blast
  from assms show "(source B, target B) ∈ CPS_S" unfolding CPS_S_def by blast 
qed

lemma CPS_R_rstep:
  assumes "(s, t) ∈ rstep CPS_R"
  shows "(s, t) ∈ rstep R"
proof-
  from rstep_imp_C_s_r[OF assms] obtain C σ l r where "(l, r) ∈ CPS_R" and s:"s = C⟨l ⋅ σ⟩" and t:"t = C⟨r ⋅ σ⟩"
    by blast
  then obtain A B where "(A,B) ∈ pterm_cpeaks R S ∨ (B,A) ∈ pterm_cpeaks S R"
    and "source A = l ∧ target A = r"
    unfolding CPS_R_def by force
  with pterm_cpeak_rstep1 pterm_cpeak_rstep2  have "(l, r) ∈ rstep R"
    by blast 
  with s t show ?thesis by auto
qed

lemma CPS_S_rstep:
  assumes "(s, t) ∈ rstep CPS_S"
  shows "(s, t) ∈ rstep S"
proof-
  from rstep_imp_C_s_r[OF assms] obtain C σ l r where "(l, r) ∈ CPS_S" and s:"s = C⟨l ⋅ σ⟩" and t:"t = C⟨r ⋅ σ⟩"
    by blast
  then obtain A B where "(A,B) ∈ pterm_cpeaks R S ∨ (B,A) ∈ pterm_cpeaks S R"
    and "source B = l ∧ target B = r"
    unfolding CPS_S_def by force
  with pterm_cpeak_rstep1 pterm_cpeak_rstep2  have "(l, r) ∈ rstep S"
    by blast 
  with s t show ?thesis by auto
qed

lemma CPS_R_subset_CPS': "CPS_R ⊆ CPS' S R"
proof
  fix s t assume "(s,t) ∈ CPS_R" 
  then obtain A B where "((A, B) ∈ pterm_cpeaks R S ∨ (B, A) ∈ pterm_cpeaks S R)" and not_closed:"¬ is_R_S_closed (A, B)"
    and src_tgt:"source A = s ∧ target A = t"
    unfolding CPS_R_def by fastforce
  then consider "(A, B) ∈ pterm_cpeaks R S" | "(B, A) ∈ pterm_cpeaks S R"
    by fastforce 
  then show "(s,t) ∈ CPS' S R" proof(cases)
    case 1
    then obtain β Bs where B:"B = Prule β Bs"  
      unfolding pterm_cpeaks_def by blast 
    with not_closed have "((target A, target B) ∉ mstep S)" 
      unfolding B using is_R_S_closed.simps by blast 
    with 1 src_tgt show ?thesis unfolding CPS'_def by blast
  next
    case 2
     then obtain α As where A:"A = Prule α As"  
      unfolding pterm_cpeaks_def by blast 
    then show ?thesis proof(cases "∃β Bs. B = Prule β Bs")
      case True
      then obtain β Bs where B:"B = Prule β Bs" by fastforce
      with 2 not_closed src_tgt show ?thesis 
        unfolding A B is_R_S_closed.simps CPS'_def using mstep_imp_rsteps by force
    next
      case False
      with not_closed have "((target B, target A) ∉ mstep R)" unfolding A
        using is_R_S_closed.simps by (smt (verit) Pair_inject is_R_S_closed.elims(3))
      with 2 src_tgt show ?thesis unfolding CPS'_def by blast
    qed
  qed
qed

lemma CPS_S_subset_CPS': "CPS_S ⊆ CPS' R S"
proof
  fix s t assume "(s,t) ∈ CPS_S" 
  then obtain A B where "((A, B) ∈ pterm_cpeaks R S ∨ (B, A) ∈ pterm_cpeaks S R)" and not_closed:"¬ is_R_S_closed (A, B)"
    and src_tgt:"source B = s ∧ target B = t"
    unfolding CPS_S_def by fastforce
  then consider "(A, B) ∈ pterm_cpeaks R S" | "(B, A) ∈ pterm_cpeaks S R"
    by fastforce 
  then show "(s,t) ∈ CPS' R S" proof(cases)
    case 1
    then obtain β Bs where B:"B = Prule β Bs"  
      unfolding pterm_cpeaks_def by blast 
    with not_closed have "((target A, target B) ∉ mstep S)" 
      unfolding B using is_R_S_closed.simps by blast 
    with 1 src_tgt show ?thesis unfolding CPS'_def by blast
  next
    case 2
     then obtain α As where A:"A = Prule α As"  
      unfolding pterm_cpeaks_def by blast 
    then show ?thesis proof(cases "∃β Bs. B = Prule β Bs")
      case True
      then obtain β Bs where B:"B = Prule β Bs" by fastforce
      with 2 not_closed src_tgt show ?thesis 
        unfolding A B is_R_S_closed.simps CPS'_def using mstep_imp_rsteps by force
    next
      case False
      with not_closed have "((target B, target A) ∉ mstep R)" unfolding A
        using is_R_S_closed.simps by (smt (verit) Pair_inject is_R_S_closed.elims(3))
      with 2 src_tgt show ?thesis unfolding CPS'_def by blast
    qed
  qed
qed

end
 
end

locale innermost_overlap =
  fixes ren :: "'v :: infinite renaming2" 
    and R S :: "('a, 'v) trs"
    and A B p q q' p⇩α q⇩β α β
  assumes R:"left_lin_wf_trs R" and S:"left_lin_wf_trs S"
    and co_init:"source A = source B" and A:"A ∈ wf_pterm R" and B:"B ∈ wf_pterm S"
    and pq:"(p, q) ∈ overlaps_pos (labeled_source A) (labeled_source B)"
    and maximal:"∀b∈ overlaps_pos (labeled_source A) (labeled_source B). (p,q) ≤⇩o b ⟶ (p,q) = b"
    and q':"Some q' = remove_prefix q p"
    and alpha:"get_label (labeled_source A |_ p) = Some (α, 0)"
    and beta:"get_label (labeled_source B |_ q) = Some (β, 0)"
    and p⇩α:"p⇩α ∈ poss A" "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p⇩α A)" "A|_p⇩α = Prule α (map (λi. A|_(p⇩α@[i])) [0..<length (var_rule α)])"
    and q⇩β:"q⇩β ∈ poss B" "ctxt_of_pos_term q (source B) = source_ctxt (ctxt_of_pos_term q⇩β B)" "B|_q⇩β = Prule β (map (λi. B|_(q⇩β@[i])) [0..<length (var_rule β)])"
begin

lemma ll_no_var_lhs_R:"left_lin_no_var_lhs R" 
  using R by (simp add: left_lin_no_var_lhs_def left_lin_wf_trs_def wf_trs.axioms(1))

lemma ll_no_var_lhs_S:"left_lin_no_var_lhs S" 
  using S by (simp add: left_lin_no_var_lhs_def left_lin_wf_trs_def wf_trs.axioms(1))

lemma wf_trs_R:"wf_trs R" 
  using R by (simp add: left_lin_wf_trs.axioms(2))

lemma wf_trs_S:"wf_trs S" 
  using S by (simp add: left_lin_wf_trs.axioms(2))

definition "s = source A"

lemma p:"p = q@q'" 
  using q' by (metis remove_prefix_Some) 

lemma le:"q ≤⇩p p"
  by (metis prefix_def q' remove_prefix_Some) 

lemma p_q_pos:"p ∈ poss s" "q ∈ poss s" using pq
  using co_init fun_poss_imp_poss s_def by (fastforce)+

abbreviation "Δ1 ≡ ll_single_redex s p α"
abbreviation "Δ2 ≡ ll_single_redex s q β"

abbreviation "As ≡ map (λi. A|_(p⇩α@[i])) [0..<length (var_rule α)]"
abbreviation "Bs ≡ map (λi. B|_(q⇩β@[i])) [0..<length (var_rule β)]"

interpretation single_Δ1:single_redex "R" "A" "Δ1" "p" "p⇩α" "α"
proof-
  from p_q_pos(1) s_def p⇩α show "single_redex R A Δ1 p p⇩α α" 
    using single_redex.intro[OF ll_no_var_lhs_R] single_redex_axioms.intro[OF A] by simp
qed

interpretation single_Δ2:single_redex "S" "B" "Δ2" "q" "q⇩β" "β"
proof-
  from p_q_pos(2) s_def co_init q⇩β show "single_redex S B Δ2 q q⇩β β" 
     using single_redex.intro[OF ll_no_var_lhs_S] single_redex_axioms.intro[OF B] by simp
qed

lemma q'_poss:"q' ∈ fun_poss (lhs β)"
proof-
  let ?n="length q'"
  from beta pq p have n:"get_label ((labeled_source B)|_p) = Some (β, ?n)" 
    by force
  have q:"q ∈ poss (labeled_source B)"
    using co_init p_q_pos(2) s_def by auto
  have "labeled_source (B|_q⇩β) = (labeled_source B)|_q"
    using single_Δ2.labeled_source_at_pq by blast 
  moreover have "is_Fun (lhs β)"
    using single_Δ2.rule_in_TRS single_Δ2.no_var_lhs by auto 
  moreover have "Prule β Bs ∈ wf_pterm S"
    by (metis B single_Δ2.aq single_Δ2.q subt_at_is_wf_pterm) 
  ultimately show ?thesis 
    using labeled_poss_in_lhs single_Δ2.a
    by (metis (no_types, lifting) co_init n p p_q_pos(1) q s_def single_Δ2.aq single_Δ2.source_at_pq subt_at_append subterm_poss_conv) 
qed

lemma source_d1: "source Δ1 = s" 
  using s_def single_Δ1.source_delta by simp

lemma source_d2: "source Δ2 = s"
  using s_def co_init single_Δ2.source_delta by simp

abbreviation "l ≡ rename_x ren (lhs β)"
abbreviation "l' ≡ rename_y ren (lhs α)" 
abbreviation "l'' ≡ l|_q'"

lemma l''_alt:"l'' = rename_x ren ((lhs β)|_q')"
  by (simp add: fun_poss_imp_poss q'_poss)

lemma linear_l:"linear_term l"
  apply (rule linear_rename_x) 
  using single_Δ2.lin_lhs by blast

lemma linear_l':"linear_term l'"
  apply (rule linear_rename_y) 
  using single_Δ1.lin_lhs by blast

lemma linear_l'':"linear_term l''"
  using q'_poss linear_l by (simp add: fun_poss_imp_poss subt_at_linear)

lemma distinct:"distinct ((vars_term_list l) @ (vars_term_list l'))"
  using distinct_vars single_Δ1.lin_lhs single_Δ2.lin_lhs by blast

lemma disjoint_vars:"vars_term l'' ∩ vars_term l' = {}"
  by (metis distinct_append distinct_vars fun_poss_imp_poss l''_alt q'_poss set_vars_term_list single_Δ1.lin_lhs single_Δ2.lin_lhs subt_at_linear)

lemma length:"length ((map ((|_) (s |_ q)) (var_poss_list l)) @ (map ((|_) (s |_ p)) (var_poss_list l'))) = length (vars_term_list l @ vars_term_list l')"
  by (simp add: length_var_poss_list)

definition "τ = (subst_of ((left_substs l'' l') @ (right_substs l'' l')))"
definition "σ = mk_subst Var ((match_substs l (s|_q)) @ (match_substs l' (s|_p)))"

lemma σ_simp:"σ = mk_subst Var (zip (vars_term_list l @ vars_term_list l') ((map ((|_) (s |_ q)) (var_poss_list l)) @ (map ((|_) (s |_ p)) (var_poss_list l'))))"
  unfolding σ_def match_substs_def by (simp add: length_var_poss_list)

lemma sigma_vars:
  shows "(∀i<length (vars_term_list l).  σ (vars_term_list l ! i) = s |_ (q @ var_poss_list l ! i)) ∧
        (∀i<length (vars_term_list l').  σ (vars_term_list l' ! i) = s |_ (p @ var_poss_list l' ! i))" (is "?ys ∧ ?xs") 
proof
  {fix j assume j:"j < length (vars_term_list l)"
    let ?y="(vars_term_list l)!j" and ?qj="(var_poss_list l)!j"
    from j have sigma_subst:"σ ?y = s|_(q@?qj)" 
      unfolding σ_simp by (smt (z3) append_eq_append_conv distinct filter_cong length length_map length_var_poss_list map_append map_nth_conv mk_subst_same p_q_pos(2) subt_at_append) 
  } then show ?ys by simp
  {fix i assume i:"i < length (vars_term_list l')"
    let ?x="(vars_term_list l')!i" and ?pi="(var_poss_list l')!i"
    from i have sigma_subst:"σ ?x = s|_(p@?pi)" 
      unfolding σ_simp by (smt (z3) append_eq_append_conv distinct filter_cong length length_map length_var_poss_list map_append map_nth_conv mk_subst_same p_q_pos(1) subt_at_append) 
  } then show ?xs by simp
qed

lemma apply_tau:
  assumes "(x, u) ∈ set (left_substs l'' l')"
  shows "τ x = u"
proof-
  from assms have "x ∈ vars_term l''"
    using map_fst_left_substs by (metis fst_conv image_eqI list.set_map subsetD) 
  then have "x ∉ vars_term l'" using distinct_vars
    by (smt (verit, best) disjoint_iff distinct_append fun_poss_imp_poss l''_alt single_Δ1.lin_lhs single_Δ2.lin_lhs q'_poss set_vars_term_list subt_at_linear) 
  moreover have "set (map fst (right_substs l'' l')) ⊆ vars_term l'" 
    unfolding right_substs_def using zip_fst by fastforce
  ultimately have "x ∉ set (map fst (right_substs l'' l'))"
    by blast 
  then have sub1:"subst_of (right_substs l'' l') x = Var x"
    by (meson not_elem_subst_of) 
  have "distinct (map fst (left_substs l'' l'))"
    by (simp add: distinct_map_fst_left_substs linear_l'') 
  then have *:"∀(y, s)∈set (left_substs l'' l'). y = x ⟶ s = u"
    using assms eq_key_imp_eq_value by fastforce 
  have "set (map fst (left_substs l'' l')) ⊆ vars_term l''"
    by (meson map_fst_left_substs) 
  moreover have "vars_term l'' ∩ vars_term u = {}"
  proof-
    from assms have "vars_term u ⊆ vars_term l'"
      by (metis left_substs_imp_props vars_term_subt_at)
    then show ?thesis 
      using disjoint_vars by blast 
  qed
  ultimately have "subst_of (left_substs l'' l') x = u"  
    using subst_of_apply[OF assms *] by blast 
  then show ?thesis 
    unfolding τ_def subst_of_append subst_compose using sub1 by simp 
qed

lemma apply_tau2:
  assumes "(y, v) ∈ set (right_substs l'' l')"
  shows "τ y = v"
proof-
  have "distinct (map fst (right_substs l'' l'))"
    by (simp add: distinct_map_fst_right_substs linear_l') 
  then have *:"∀(x, s)∈set (right_substs l'' l'). x = y ⟶ s = v"
    using assms eq_key_imp_eq_value by fastforce 
  have "set (map fst (right_substs l'' l')) ⊆ vars_term l'"
    unfolding right_substs_def using zip_fst by fastforce
  moreover have "vars_term l' ∩ vars_term v = {}"
  proof-
    from assms have "vars_term v ⊆ vars_term l''"
      by (metis fun_poss_imp_poss right_substs_imp_props vars_term_subt_at)
    then show ?thesis 
      using disjoint_vars by blast 
  qed
  ultimately have sub1:"subst_of (right_substs l'' l') y = v"  
    using subst_of_apply[OF assms *] by blast
  {fix x assume "x ∈ vars_term v"
    with assms have "x ∉ set (map fst (left_substs l'' l'))" 
      using distinct_fst_lsubsts_snd_rsubsts[OF linear_l''] by fastforce 
    then have "subst_of (left_substs l'' l') x = Var x" 
      using not_elem_subst_of by metis
  }
  then show ?thesis 
    unfolding τ_def subst_of_append subst_compose sub1 by (simp add: term_subst_eq)
qed

lemma var_in_l'_in_domain_tau:
  assumes "τ x ≠ Var x"
    and "x ∈ vars_term l'"
  shows "∃u. (x, u) ∈ set (right_substs l'' l')"
proof-
  from assms(2) have "x ∉ vars_term l''"
    by (smt (verit, best) disjoint_iff distinct distinct_append fun_poss_imp_poss poss_map_vars_term q'_poss set_vars_term_list subsetD vars_term_subt_at)
  then have "x ∉ set (map fst (left_substs l'' l'))"
    by (meson in_mono map_fst_left_substs) 
  then have "(subst_of (left_substs l'' l')) x = Var x"
    by (meson not_elem_subst_of) 
  with assms(1) have "x ∈ set (map fst (right_substs l'' l'))" 
    unfolding τ_def subst_of_append by (metis not_elem_subst_of subst_compose_def subst_monoid_mult.mult.left_neutral) 
  then show ?thesis
    by auto 
qed

lemma var_in_domain_tau:
  assumes "τ x ≠ Var x"
    and "i < length (vars_term_list l')" and "vars_term_list l'!i = x"
  shows "(var_poss_list l'!i) ∈ fun_poss l''"
proof-
  from assms obtain u where "(x, u) ∈ set (right_substs l'' l')" 
    using var_in_l'_in_domain_tau by (metis nth_mem set_vars_term_list) 
  then obtain q where q:"q ∈ fun_poss l''" "l'' |_ q = u" "q ∈ poss l'" "l' |_ q = Var x" 
    using right_substs_imp_props by force 
  with linear_l' have "q = (var_poss_list l'!i)"
    by (metis assms(2) assms(3) length_var_poss_list linear_term_unique_vars nth_mem var_poss_imp_poss var_poss_list_sound vars_term_list_var_poss_list) 
  then show ?thesis 
    using q(1) by force 
qed

lemma l_sigma_subst:"l ⋅ σ = s|_q"
proof-
  let ?xs="map source (map (to_pterm ∘ (λpi. s |_ (q @ pi))) (var_poss_list (lhs β)))"
  from source_d2 have "(lhs β) ⋅ ⟨?xs⟩⇩β  = s|_q" 
    unfolding ll_single_redex_def by (metis (no_types, lifting) p_q_pos(2) replace_at_subt_at source.simps(3) source_to_pterm_ctxt to_pterm_ctxt_at_pos)
  then have "l ⋅ (mk_subst Var (zip (vars_distinct l) ?xs)) = s|_q"
    by (metis (mono_tags, lifting) length_map length_var_poss_list linear_term_var_vars_term_list mk_subst_rename_x single_Δ2.lin_lhs) 
  with sigma_vars show ?thesis using substitution_subterm_at
    by (smt (verit, best) filter_cong p_q_pos(2) subt_at_append)
qed

lemma l'_sigma_subst:"l' ⋅ σ = s|_p"
proof-
  let ?xs="map source (map (to_pterm ∘ (λpi. s |_ (p @ pi))) (var_poss_list (lhs α)))"
  from source_d1 have "(lhs α) ⋅ ⟨?xs⟩⇩α  = s|_p" 
    unfolding ll_single_redex_def by (metis (no_types, lifting) p_q_pos(1) replace_at_subt_at source.simps(3) source_to_pterm_ctxt to_pterm_ctxt_at_pos) 
  then have "l' ⋅ (mk_subst Var (zip (vars_distinct l') ?xs)) = s|_p"
    by (metis (mono_tags, lifting) length_map length_var_poss_list linear_term_var_vars_term_list mk_subst_rename_y single_Δ1.lin_lhs)
  with sigma_vars show ?thesis using substitution_subterm_at
    by (smt (verit, best) filter_cong p_q_pos(1) subt_at_append)
qed

lemma l''_sigma_subst:"l'' ⋅ σ = s|_p"
proof-
  from q' have "p = q@q'"
    by (metis remove_prefix_Some) 
  then have "s|_p = (s|_q)|_q'" using p_q_pos
    by simp 
  then show ?thesis
    by (metis l_sigma_subst poss_map_vars_term q'_poss fun_poss_imp_poss subt_at_subst) 
qed

lemma mgu:"mgu l'' l' = Some τ"
proof-
  from l''_sigma_subst have un:"unifiers {(l'', l')} ≠ {}" 
    unfolding l'_sigma_subst[symmetric] using unifiers_def by fastforce 
  from distinct have "distinct (vars_term_list (l |_ q') @ vars_term_list l')"
    by (metis distinct_vars fun_poss_imp_poss l''_alt q'_poss single_Δ1.lin_lhs single_Δ2.lin_lhs subt_at_linear) 
  then show ?thesis 
    using mgu_distinct_vars_term_list[OF un] distinct unfolding τ_def by simp
qed

lemma ctxt_l_at_q':"ctxt_of_pos_term q' l ⋅⇩c τ = ctxt_of_pos_term q' l"
proof-
  {fix x assume x:"x ∈ vars_ctxt (ctxt_of_pos_term q' l)"
    then have "x ∉ vars_term l''" 
      using linear_term_ctxt by (metis disjoint_iff fun_poss_imp_poss linear_l poss_map_vars_term q'_poss)
    then have l:"x ∉ set (map fst (left_substs l'' l'))" 
      using map_fst_left_substs by (metis subset_code(1))
    have "x ∉ vars_term l'"
      using disjoint_iff distinct fun_poss_imp_poss q'_poss vars_ctxt_pos_term x by fastforce
    then have r:"x ∉ set (map fst (right_substs l'' l'))"
      unfolding right_substs_def using zip_fst by fastforce
    from l r have "τ x = Var x" unfolding τ_def 
      using not_elem_subst_of by (metis Un_iff map_append set_append)  
  }
  then show ?thesis
    by (simp add: ctxt_subst_eq) 
qed

abbreviation x_var :: "'v ⇒ 'v" where "x_var ≡ rename_1 ren" 
abbreviation y_var :: "'v ⇒ 'v" where "y_var ≡ rename_2 ren"

lemma x_diff_y[simp]: "x_var v ≠ y_var w" 
  using rename_12[of ren] by blast

abbreviation rename_x where "rename_x ≡ map_vars_term (rename_1 ren)"
abbreviation rename_y where "rename_y ≡ map_vars_term (rename_2 ren)"

abbreviation "a ≡ (to_pterm_ctxt (ctxt_of_pos_term q' l)) ⟨Prule α (map (to_pterm ∘ τ ∘ y_var) (var_rule α))⟩"
abbreviation "b ≡ Prule β (map (to_pterm ∘ τ ∘ x_var) (var_rule β))"

lemma critical_peak:
  shows "(a, b) ∈ pterm_cpeaks ren R S"
proof-
  from mgu have mgu':"mgu_vd ren (lhs β |_ q') (lhs α) = Some (τ ∘ x_var, τ ∘ y_var)" 
    unfolding mgu_vd_def mgu_var_disjoint_generic_def using l''_alt by simp
  have C:"to_pterm_ctxt (ctxt_of_pos_term q' (lhs β ⋅ (τ ∘ x_var))) = to_pterm_ctxt (ctxt_of_pos_term q' l)"
    by (metis apply_subst_map_vars_term ctxt_l_at_q' ctxt_of_pos_term_subst fun_poss_imp_poss poss_map_vars_term q'_poss)
  from pterm_cpeaksI[OF single_Δ1.rule_in_TRS single_Δ2.rule_in_TRS q'_poss mgu'] show ?thesis 
    unfolding C by (simp add: comp_assoc) 
qed

lemma critical_pair: 
  shows "(p=q, replace_at l q' ((rename_y (rhs α)) ⋅ τ), (rename_x (rhs β)) ⋅ τ) ∈ critical_pairs ren S R"
proof-
  have "(p=q) = is_Prule a" proof(cases "q'")
    case Nil
    with p show ?thesis by simp
  next
    case (Cons i q'')
    with p have *:"p ≠ q"
      by simp 
    from Cons q'_poss obtain f ts where l:"l = Fun f ts"
      by (metis empty_iff fun_poss.simps(1) fun_poss_map_vars_term term_to_term_lab.cases) 
    from * show ?thesis unfolding Cons l by simp 
  qed
  moreover have "target a = replace_at l q' ((rename_y (rhs α)) ⋅ τ)" 
  proof-
    {fix x assume "x ∈ vars_term (rhs α)"
      then have "x ∈ vars_term (lhs α)"
        using single_Δ1.rule_in_TRS wf_trs_R unfolding wf_trs_def var_rhs_subset_lhs_def by fastforce 
      then obtain i where "i < length (var_rule α)" and "x = (var_rule α)!i"
        by (metis in_set_idx linear_term_var_vars_term_list set_vars_term_list single_Δ1.lin_lhs) 
      then have "⟨map (target ∘ (to_pterm ∘ τ ∘ y_var)) (var_rule α)⟩⇩α x = (τ ∘ y_var) x" 
        using lhs_subst_var_i target_to_pterm by (metis (no_types, lifting) comp_apply length_map nth_map) 
      }
      then show ?thesis 
        unfolding target_to_pterm_ctxt by (simp add: apply_subst_map_vars_term term_subst_eq_conv)
    qed
  moreover have "target b = (rename_x (rhs β)) ⋅ τ" proof-
    {fix x assume "x ∈ vars_term (rhs β)"
      then have "x ∈ vars_term (lhs β)"
        using single_Δ2.rule_in_TRS wf_trs_S unfolding wf_trs_def var_rhs_subset_lhs_def by fastforce 
      then obtain i where "i < length (var_rule β)" and "x = (var_rule β)!i"
        by (metis in_set_idx linear_term_var_vars_term_list set_vars_term_list single_Δ2.lin_lhs) 
      then have "⟨map (target ∘ (to_pterm ∘ τ ∘ x_var)) (var_rule β)⟩⇩β x = (τ ∘ x_var) x" 
        using lhs_subst_var_i target_to_pterm by (metis (no_types, lifting) comp_apply length_map nth_map) 
    }
    then show ?thesis 
      unfolding target_to_pterm_ctxt by (simp add: apply_subst_map_vars_term term_subst_eq_conv)
  qed
  moreover have "(⋀l r. (l, r) ∈ R ∪ S ⟹ vars_term r ⊆ vars_term l)" 
    using wf_trs_R wf_trs_S unfolding wf_trs_def var_rhs_subset_lhs_def by blast 
  ultimately show ?thesis using pterm_cpeak_to_critical_pair critical_peak
    by (smt (verit, best)) 
qed

lemma sigma_tau_vars:
  shows "(∀i < length (vars_term_list l). (τ ∘⇩s σ) ((vars_term_list l)!i) = s|_(q@(var_poss_list l)!i)) ∧
         (∀i < length (vars_term_list l'). (τ ∘⇩s σ) ((vars_term_list l')!i) = s|_(p@(var_poss_list l')!i)) " (is "?ys ∧ ?xs")
proof
  let ?l_substs="left_substs l'' l'"
  let ?r_substs="right_substs l'' l'"
  have disj:"vars_term l ∩ vars_term l' = {}" 
    by (simp add: disjoint_iff_not_equal term.set_map(2)) 
  
  {fix j assume j:"j < length (vars_term_list l)"
    let ?y="(vars_term_list l)!j" and ?qj="(var_poss_list l)!j"
    from j have var:"l|_?qj = Var ?y"
      by (metis vars_term_list_var_poss_list) 
    have "set (map fst (?r_substs)) ⊆ vars_term l'"
      unfolding right_substs_def using zip_fst by fastforce
    then have right:"?y ∉ set (map fst (?r_substs))"
      using j disj nth_mem by fastforce
    have "(τ ∘⇩s σ) ?y = s |_ (q @ ?qj)" proof (cases "?y ∈ set (map fst ?l_substs)")
      case True
      then obtain u where u:"(?y, u) ∈ set ?l_substs"
        by fastforce  
      then obtain qj' where qj':"qj' ∈ poss l''" "l'' |_ qj' = Var ?y" "qj' ∈ poss l'" "l' |_ qj' = u" 
        using left_substs_imp_props by metis 
      with u have tau_subst:"τ ?y = l'|_qj'" 
        using apply_tau by blast
      from var qj'(2) have qj:"?qj = q'@qj'" using linear_term_unique_vars[OF linear_l] j qj'(1) q'_poss
        by (metis fun_poss_imp_poss length_var_poss_list nth_mem pos_append_poss poss_map_vars_term subt_at_append var_poss_imp_poss var_poss_list_sound)
      then have "(τ ∘⇩s σ) ?y = (l' ⋅ σ)|_qj'" 
        unfolding subst_compose tau_subst using qj'(3) subt_at_subst by metis
      then show ?thesis unfolding l'_sigma_subst qj using q' subt_at_append p_q_pos
        by (metis append.assoc remove_prefix_Some)
    next
      case False
      with right have tau_subst:"τ ?y = Var ?y" 
        unfolding τ_def using not_elem_subst_of by (metis Un_iff map_append set_append)
      from j have sigma_subst:"σ ?y = s|_(q@?qj)" 
        using sigma_vars by blast 
      then show ?thesis 
        unfolding subst_compose tau_subst eval_term.simps by blast
    qed
  } 
  then show ?ys by simp
  {fix i assume i:"i < length (vars_term_list l')"
    let ?x="(vars_term_list l')!i" and ?pi="(var_poss_list l')!i"
    from i have var:"l'|_?pi = Var ?x"
      by (metis vars_term_list_var_poss_list) 
    have "set (map fst (?l_substs)) ⊆ vars_term l''"
      unfolding left_substs_def using zip_fst by fastforce
    then have "set (map fst (?l_substs)) ⊆ vars_term l"
      by (smt (verit, best) fun_poss_imp_poss poss_map_vars_term q'_poss subsetD subsetI vars_term_subt_at)
    then have left:"?x ∉ set (map fst (?l_substs))"
      using i disj nth_mem by fastforce
    have "(τ ∘⇩s σ) ?x = s |_ (p @ ?pi)" proof (cases "?x ∈ set (map fst ?r_substs)")
      case True
      then obtain u where u:"(?x, u) ∈ set ?r_substs"
        by fastforce  
      then obtain pi' where pi':"pi' ∈ poss l'" "l' |_ pi' = Var ?x" "pi' ∈ fun_poss l''" "l'' |_ pi' = u" 
        using right_substs_imp_props by metis 
      with u have tau_subst:"τ ?x = l''|_pi'" 
        using apply_tau2 by blast
      from var pi'(2) have pi:"?pi = pi'" using linear_term_unique_vars[OF linear_l'] i pi'(1)
        by (metis length_var_poss_list nth_mem var_poss_imp_poss var_poss_list_sound) 
      then have "(τ ∘⇩s σ) ?x = (l'' ⋅ σ)|_pi'" 
        unfolding subst_compose tau_subst using pi'(3) by (simp add: fun_poss_imp_poss)
      then show ?thesis unfolding l''_sigma_subst pi 
        using subt_at_append p_q_pos by simp
    next
      case False
      with left have tau_subst:"τ ?x = Var ?x" 
        unfolding τ_def using not_elem_subst_of by (metis Un_iff map_append set_append)
      from i have sigma_subst:"σ ?x = s|_(p@?pi)" 
        using sigma_vars by blast
      then show ?thesis 
        unfolding subst_compose tau_subst eval_term.simps by blast
    qed
  } then show ?xs by simp
qed

lemma l_tau_sigma:
  shows "l ⋅ τ ⋅ σ = s|_q"
proof-
  {fix x assume "x ∈ vars_term l"
    then obtain i where "i < length (vars_term_list l)" "x = (vars_term_list l ! i)"
      by (metis in_set_idx set_vars_term_list)
    with sigma_tau_vars sigma_vars have "(τ ∘⇩s σ) x = σ x"
      by simp
  }
  then show ?thesis using l_sigma_subst
    by (metis (no_types, lifting) subst_subst term_subst_eq) 
qed

lemma l'_tau_sigma:
  shows "l' ⋅ τ ⋅ σ = s|_p"
proof-
  {fix x assume "x ∈ vars_term l'"
    then obtain i where "i < length (vars_term_list l')" "x = (vars_term_list l' ! i)"
      by (metis in_set_idx set_vars_term_list)
    with sigma_tau_vars sigma_vars have "(τ ∘⇩s σ) x = σ x"
      by simp
  }
  then show ?thesis using l'_sigma_subst
    by (metis (no_types, lifting) subst_subst term_subst_eq) 
qed

text‹Preparation for Lemma 4.1 of 'Commutation via Relative Termination'›
lemma Δ1_is_rstep:
  assumes "(source a, target a) ∈ X"
  shows "(source Δ1, target Δ1) ∈ rstep X"
proof-
  have *:"vars_term (rhs α) ⊆ vars_term (lhs α)" 
     using wf_trs_R single_Δ1.rule_in_TRS unfolding wf_trs_def var_rhs_subset_lhs_def by blast  
  from q'_poss have q':"q' ∈ poss l"
     by (simp add: fun_poss_imp_poss) 
  have src:"source a = (ctxt_of_pos_term q' l) ⟨rename_y (lhs α) ⋅ τ⟩"
    unfolding source_to_pterm_ctxt source.simps map_map lhs_subst_var_rule[OF subset_refl[of "vars_term (lhs α)"]] 
    by (simp add: apply_subst_map_vars_term term_subst_eq_conv) 
  have tgt:"target a = (ctxt_of_pos_term q' l) ⟨rename_y (rhs α) ⋅ τ⟩"
    unfolding target_to_pterm_ctxt target.simps map_map lhs_subst_var_rule[OF *] 
    by (simp add: apply_subst_map_vars_term term_subst_eq_conv)
  have "source Δ1 = (ctxt_of_pos_term q s) ⟨(source a) ⋅ σ⟩"
    unfolding src by (metis ctxt_supt_id l''_sigma_subst l'_tau_sigma l_sigma_subst p_q_pos(2) q' s_def single_Δ1.source_delta subst_apply_term_ctxt_apply_distrib)
  moreover have "target Δ1 = (ctxt_of_pos_term q s) ⟨(target a) ⋅ σ⟩"
    unfolding tgt using *
    by (smt (z3) apply_subst_map_vars_term calculation ctxt_apply_ctxt_apply ctxt_of_pos_term_subst l'_tau_sigma l_sigma_subst p p_q_pos(1) p_q_pos(2) q' replace_at_subt_at s_def single_Δ1.source_delta source_single_redex subst_apply_term_ctxt_apply_distrib subst_subst_compose target_single_redex vars_term_subset_subst_eq)
  ultimately show ?thesis using assms by blast
qed

lemma Δ2_is_rstep: 
   assumes "(source b, target b) ∈ X"
   shows "(source Δ2, target Δ2) ∈ rstep X" 
proof-
  have *:"vars_term (rhs β) ⊆ vars_term (lhs β)" 
    using single_Δ2.rule_in_TRS wf_trs_S unfolding wf_trs_def var_rhs_subset_lhs_def by blast 
  have src:"source b = rename_x (lhs β) ⋅ τ"
    unfolding source.simps map_map lhs_subst_var_rule[OF subset_refl[of "vars_term (lhs β)"]]
    by (simp add: apply_subst_map_vars_term term_subst_eq_conv) 
  have tgt:"target b = rename_x (rhs β) ⋅ τ"
    unfolding target.simps map_map lhs_subst_var_rule[OF *] by (simp add: apply_subst_map_vars_term term_subst_eq_conv)
  have "source Δ2 = (ctxt_of_pos_term q s) ⟨(source b) ⋅ σ⟩"
    unfolding src by (simp add: l_tau_sigma p_q_pos(2) replace_at_ident source_d2) 
  moreover have "target Δ2 = (ctxt_of_pos_term q s) ⟨(target b) ⋅ σ⟩"
    unfolding tgt target_single_redex[OF p_q_pos(2)]
    by (smt (verit) "*" filter_cong l_tau_sigma map_eq_conv map_vars_term_eq p_q_pos(2) replace_at_subt_at source_d2 source_single_redex subst_subst_compose vars_term_subset_subst_eq)
  ultimately show ?thesis using assms by blast
qed
 
context 
  fixes D'
  assumes d'_well:"D' ∈ wf_pterm S" 
    and src_d':"source D' = replace_at l q' (rename_y (rhs α) ⋅ τ)" 
begin

definition "D = replace_at (to_pterm s) q (D' ⋅ (to_pterm ∘ σ))"

lemma d_well:"D ∈ wf_pterm S"
proof-
  have "(D' ⋅ (to_pterm ∘ σ)) ∈ wf_pterm S" 
    using apply_subst_wf_pterm using d'_well by force 
   then show ?thesis 
     by (simp add: ctxt_wf_pterm D_def p_in_poss_to_pterm p_q_pos(2))
qed

lemma source_D:  
  "source D = target Δ1" 
proof-
  have α:"to_rule α ∈ R"
    using single_Δ1.rule_in_TRS by blast 
  {fix x assume "x ∈ vars_term (rhs α)"
    with α have x:"x ∈ vars_term (lhs α)" using wf_trs_R unfolding wf_trs_def var_rhs_subset_lhs_def by blast
    then have "(⟨map (λpi. s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α) x = ((Var ∘ y_var) x) ⋅ τ ⋅ σ"
    proof-
      from x obtain i where i:"x = var_rule α!i" and len:"i < length (var_rule α)"
        by (metis in_set_conv_nth linear_term_var_vars_term_list single_Δ1.lin_lhs set_vars_term_list)
      then have len2:"i < length (var_poss_list (lhs α))"
        by (metis length_var_poss_list linear_term_var_vars_term_list single_Δ1.lin_lhs)  
      then have left:"(⟨map (λpi. s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α) x = s |_ (p @ (var_poss_list (lhs α)!i))" 
        using lhs_subst_var_i[OF i len] by (smt (z3) length_map nth_map) 
      from i have "x = vars_term_list (lhs α) ! i"
        by (metis linear_term_var_vars_term_list single_Δ1.lin_lhs) 
      with len2 have "((y_var) x) = vars_term_list (rename_y (lhs α))!i" 
        using vars_map_vars_term by (metis length_var_poss_list nth_map)
      with len2 have right:"((Var ∘ y_var) x) ⋅ τ ⋅ σ = s |_ (p @ (var_poss_list (lhs α)!i))" 
        using sigma_tau_vars var_poss_list_map_vars_term
        by (smt (verit, best) comp_apply filter_cong length_var_poss_list eval_term.simps(1) subst_subst_compose) 
      show ?thesis unfolding left right by simp
    qed
  }
  then have "rhs α ⋅ ⟨map (λpi. s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α = (rename_y (rhs α)) ⋅ τ ⋅ σ"
    using term_subst_eq_conv[where τ="(Var ∘ y_var) ∘⇩s τ ∘⇩s σ"] 
    unfolding map_vars_term_eq by (simp add: subst_compose)
  then have target:"target (ll_single_redex s p α) = replace_at s p ((rename_y (rhs α)) ⋅ τ ⋅ σ)"
    using p_q_pos target_single_redex by fastforce
  have "source D = (ctxt_of_pos_term q s)⟨source (D' ⋅ (to_pterm ∘ σ))⟩" 
    unfolding D_def using p_q_pos source_to_pterm_ctxt to_pterm_ctxt_at_pos by metis
  also have "... = (ctxt_of_pos_term q s)⟨(replace_at l q' ((rename_y (rhs α)) ⋅ τ)) ⋅ σ⟩" 
    using d'_well source_apply_subst src_d' by (metis source_to_pterm to_pterm_subst to_pterm_wf_pterm)
  also have "... = (ctxt_of_pos_term q s)⟨replace_at (l⋅σ) q' ((rename_y (rhs α)) ⋅ τ ⋅ σ)⟩" 
    using q'_poss by (simp add: ctxt_of_pos_term_subst fun_poss_imp_poss) 
  also have "... = (ctxt_of_pos_term p s)⟨(rename_y (rhs α)) ⋅ τ ⋅ σ⟩" 
    unfolding l_sigma_subst ctxt_ctxt using p_q_pos q' ctxt_of_pos_term_append by (metis (no_types, lifting) remove_prefix_Some) 
  finally show ?thesis using target by auto 
qed

section‹Introducing ρ›

abbreviation "lhs⇩β' ≡ (lhs β)|_q'"
definition "rho_substs = match_substs (to_pterm l') ((to_pterm lhs⇩β') ⋅ ⟨Bs⟩⇩β)"
abbreviation "ρ ≡ mk_subst Var ((zip (vars_distinct l) Bs)@rho_substs)"

lemma innermost_ov_contr:
  assumes "r ∈ fun_poss l'"
  shows "r ∉ possL (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)"
proof
  assume r:"r ∈ possL (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)"
  {fix x assume "x ∈ vars_term lhs⇩β'"
    then have "(⟨Bs⟩⇩β) x ∈ wf_pterm S"
      by (metis lhs_subst_var_well_def single_Δ2.as_well) 
  }
  then obtain p1 p2 x γ where p1:"p1 ∈ poss lhs⇩β'" and x:"lhs⇩β' |_ p1 = Var x" and p1p2:"p1 @ p2 ≤⇩p r" and
    p2:"p2 ∈ possL ((⟨Bs⟩⇩β) x)" and lab0:"get_label (labeled_source ((⟨Bs⟩⇩β) x) |_ p2) = Some (γ, 0)"
    using labeled_source_to_pterm_subst[OF r] by blast 
  from p1 x have x_beta:"x ∈ set (var_rule β)"
    by (metis fun_poss_imp_poss in_mono linear_term_var_vars_term_list q'_poss set_vars_term_list single_Δ2.lin_lhs term.set_intros(3) vars_term_subt_at)
  from p2 obtain f' ts where fun_f':"(labeled_source ((⟨Bs⟩⇩β) x))|_p2 = Fun f' ts"
    using labelposs_subs_fun_poss fun_poss_fun_conv by blast
  with lab0 have f':"snd f' = Some (γ, 0)"
    by simp 
  have q'p1_pos:"(q' @ p1) ∈ poss (labeled_lhs β)" 
    using q'_poss p1 by (simp add: fun_poss_imp_poss) 
  then have "labeled_lhs β |_ (q'@p1) = Var x" using x
    by (smt (verit) DiffE fun_poss_label_term is_VarE label_term_to_term labeled_source_pos poss_is_Fun_fun_poss poss_simps(3) poss_term_lab_to_term q'_poss subt_at_append term.inject(1) term_lab_to_term.simps(1) var_poss_iff)
  then have "(labeled_source (Prule β Bs))|_(q'@p1@p2) = ((⟨map labeled_source Bs⟩⇩β) x) |_ p2" 
    unfolding labeled_source.simps using q'p1_pos subt_at_append[of "q'@p1"]
    by (smt (verit, best) poss_append_poss poss_imp_subst_poss eval_term.simps(1) subt_at_append subt_at_subst)
  with fun_f' have lab:"(labeled_source (Prule β Bs))|_(q'@p1@p2) = Fun f' ts" 
    using x_beta single_Δ2.length_as by (smt (verit) in_set_idx length_map lhs_subst_var_i nth_map) 
  moreover from p1 x p1p2 have q'p1p2:"q' @ p1 @ p2 ∈ poss (source (Prule β Bs))" 
    unfolding source.simps using q'_poss labelposs_subs_fun_poss_source[OF p2]
    by (smt (verit, best) fun_mk_subst fun_poss_imp_poss o_apply poss_append_poss poss_imp_subst_poss source_to_pterm eval_term.simps(1) subt_at_subst to_pterm.simps(1))
  then have overlap:"(p, p@p1@p2) ∈ overlaps_pos (labeled_source A) (labeled_source B)" proof-
    have "p @ p1 @ p2 ∈ fun_poss (labeled_source B)"
      using single_Δ2.labeled_source_at_pq lab q'p1p2 unfolding single_Δ2.aq p
      by (metis (no_types, lifting) append_assoc is_FunI labeled_source_to_term pos_append_poss poss_is_Fun_fun_poss poss_term_lab_to_term single_Δ2.p subt_at_append) 
    moreover have p_pos:"p ∈ fun_poss (labeled_source A)"
      using pq by force 
    moreover have "get_label ((labeled_source B) |_ (p @ p1 @ p2)) = Some (γ, 0)" 
      using single_Δ2.labeled_source_at_pq lab q'p1p2 f' unfolding single_Δ2.aq p by (simp add: single_Δ2.p) 
    moreover have "get_label ((labeled_source A) |_ p) = Some (α, 0)"
      by (simp add: alpha)
    moreover have "get_label ((labeled_source A) |_ (p @ p1 @ p2)) = Some (α, length (p1@p2))" proof-
      from assms have "r ∈ fun_poss (lhs α)"
        by (simp add: fun_poss_map_vars_term)
      then have "p1@p2 ∈ fun_poss (lhs α)" using p1p2
        by (metis fun_poss_append_poss fun_poss_imp_poss prefix_pos_diff self_append_conv)  
      moreover have "labeled_source A|_p = labeled_lhs α ⋅ ⟨map labeled_source As⟩⇩α"
        using single_Δ1.labeled_source_at_pq single_Δ1.aq by simp 
      ultimately show ?thesis 
        using label_term_increase p_pos by (metis (no_types, lifting) add_0 fun_poss_imp_poss subt_at_append)
    qed
    ultimately show ?thesis 
      using overlaps_pos_intro overlaps_pos_symmetric by blast
  qed
  have "p1 ≠ []" 
    using x q'_poss fun_poss_fun_conv by fastforce 
  moreover have "(p, q) ≤⇩o (p, p@p1@p2)"
    unfolding less_eq_overlap_def by (simp add: le)
  ultimately show False  
    using maximal using le overlap by fastforce 
qed

lemma apply_tau_rho:
  assumes j:"j < length (vars_term_list l)" and y:"y = vars_term_list l!j"
  shows "(to_pterm (τ y)) ⋅ ρ = Bs!j"
proof-
  let ?qj="var_poss_list l!j" 
  have qj:"l|_?qj = Var y"
    by (simp add: j vars_term_list_var_poss_list y) 
  have y':"y = vars_distinct l ! j" 
    using linear_l linear_term_var_vars_term_list y by force 
  have l'_rho:"to_pterm l' ⋅ ρ = ((to_pterm (lhs β)|_q') ⋅ ⟨Bs⟩⇩β)" proof-
    {fix x assume x:"x ∈ vars_term l'"
      then have "x ∉ set (vars_distinct l)" 
        using distinct by auto 
      then have "x ∉ set (map fst (zip (vars_distinct l) Bs))"
        by (smt (verit, best) length_map linear_l linear_term_var_vars_term_list map_fst_zip single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term) 
      then have "ρ x = (mk_subst Var rho_substs) x" 
        using mk_subst_concat by fastforce
    }
    moreover have "to_pterm l' ⋅ (mk_subst Var rho_substs) = (to_pterm (lhs β)|_q') ⋅ ⟨Bs⟩⇩β" proof-
      have well:"to_pterm (lhs β) |_ q' ⋅ ⟨Bs⟩⇩β ∈ wf_pterm S" 
        using lhs_subst_var_well_def[OF single_Δ2.as_well] p_in_poss_to_pterm q'_poss subt_at_is_wf_pterm
        by (smt (verit, ccfv_SIG) fun_poss_imp_poss lhs_subst_well_def single_Δ2.as_well to_pterm_wf_pterm)
      have src:"source (to_pterm (lhs β) |_ q' ⋅ ⟨Bs⟩⇩β) = l' ⋅ σ" proof-
        have "source (to_pterm (lhs β) |_ q' ⋅ ⟨Bs⟩⇩β) = (source (Prule β Bs)) |_q'"
          unfolding source.simps using subt_at_subst source_apply_subst q'_poss
          using ctxt_supt_id fun_mk_subst fun_poss_imp_poss p_in_poss_to_pterm replace_at_subt_at source.simps(1) source_to_pterm to_pterm_ctxt_apply_term to_pterm_ctxt_at_pos to_pterm_wf_pterm
          by (metis (no_types, lifting))
        then show ?thesis unfolding l'_sigma_subst
          by (metis co_init innermost_overlap.p_q_pos(2) innermost_overlap_axioms p s_def single_Δ2.aq single_Δ2.source_at_pq subt_at_append)
      qed
      have "to_pterm (lhs β) |_ q' = to_pterm lhs⇩β'"
        by (metis fun_poss_imp_poss p_in_poss_to_pterm q'_poss replace_at_ident replace_at_subt_at to_pterm_ctxt_of_pos_apply_term)
      moreover then have "∀p∈fun_poss l'. p ∉ possL (to_pterm (lhs β) |_ q' ⋅ ⟨Bs⟩⇩β)"
        using innermost_ov_contr by simp
      ultimately show ?thesis
        using linear_l' rho_substs_def single_Δ2.pterm_source_substitution src well by force
    qed
    ultimately show ?thesis
      by (smt (verit, ccfv_SIG) set_vars_term_list term_subst_eq_conv vars_to_pterm)
  qed
  have y_Bsj:"ρ y = Bs!j" proof-
    have "j < length (vars_distinct l)" 
      using j linear_l by (metis linear_term_var_vars_term_list) 
    moreover have "length (vars_distinct l) = length Bs"
      by (smt (verit, best) length_map linear_l linear_term_var_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term) 
    ultimately have *:"map_of (zip (vars_distinct l) Bs) y = Some (Bs!j)" 
      using map_of_zip_nth distinct y' by force 
    then show ?thesis unfolding mk_subst_def map_of_append map_add_def * by fastforce
  qed
  show ?thesis proof (cases "y ∈ set (map fst (left_substs l'' l'))")
    case True
    then obtain u where u:"(y, u) ∈ set (left_substs l'' l')"
      by fastforce  
    then obtain qj' where qj':"qj' ∈ poss l''" "l'' |_ qj' = Var y" "qj' ∈ poss l'" "l' |_ qj' = u" 
      using left_substs_imp_props by metis
    with u have "τ y = l'|_qj'" 
      using apply_tau by blast
    then have "(to_pterm (τ y)) ⋅ ρ = ((to_pterm (lhs β)|_q') ⋅ ⟨Bs⟩⇩β) |_qj'" 
      using l'_rho by (smt (verit, best) p_in_poss_to_pterm qj'(3) replace_at_ident replace_at_subt_at subt_at_subst to_pterm_ctxt_of_pos_apply_term)
    moreover have "((to_pterm (lhs β)|_q') ⋅ ⟨Bs⟩⇩β) |_qj' = Bs!j" proof-
      from qj'(1) have qj'_pos:"qj' ∈ poss ((lhs β)|_q')"
        by (simp add: l''_alt)  
      with qj'(2) have "(to_pterm (lhs β)|_q')|_qj' = Var ((vars_term_list (lhs β))!j)"  
        unfolding y
        by (smt (verit) fun_poss_imp_poss j length_var_poss_list linear_l linear_term_unique_vars nth_mem p_in_poss_to_pterm pos_append_poss poss_map_vars_term q'_poss subt_at_append var_poss_imp_poss var_poss_list_map_vars_term var_poss_list_sound var_poss_list_to_pterm vars_term_list_var_poss_list vars_to_pterm)  
      with qj'_pos show ?thesis
        by (smt (verit, ccfv_threshold) apply_lhs_subst_var_rule fun_poss_imp_poss j length_map linear_term_var_vars_term_list nth_map p_in_poss_to_pterm poss_append_poss q'_poss single_Δ2.length_as single_Δ2.lin_lhs eval_term.simps(1) subt_at_subst vars_map_vars_term) 
    qed
    ultimately show ?thesis by presburger 
  next
    case False
    have "set (map fst (right_substs l'' l')) ⊆ vars_term l'"
      unfolding right_substs_def using zip_fst by fastforce
    moreover have "vars_term l ∩ vars_term l' = {}" 
      by (simp add: disjoint_iff_not_equal term.set_map(2)) 
    ultimately have right:"y ∉ set (map fst (right_substs l'' l'))"
      using j nth_mem y by fastforce
    with False have "τ y = Var y" 
      unfolding τ_def using not_elem_subst_of by (metis Un_iff map_append set_append)
    then show ?thesis using y_Bsj by simp
  qed 
qed

lemma var_l_rho:
  assumes j:"j < length (vars_distinct l)"
  shows "ρ (vars_distinct l ! j) = Bs!j"
proof-
  have "length Bs = length (vars_distinct l)"
    by (smt (verit, ccfv_threshold) length_map linear_l linear_term_var_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term) 
  then have "map_of (zip (vars_distinct l) Bs) (vars_distinct l !j) = Some (Bs ! j)"
    by (metis (no_types, lifting) distinct distinct_append j(1) linear_l linear_term_var_vars_term_list map_of_zip_nth single_Δ2.length_as) 
  then show ?thesis 
    unfolding mk_subst_def map_of_append by simp
qed

lemma var_l'_rho:
  assumes i:"i < length (vars_term_list l')"
  shows "ρ (vars_term_list l' ! i) = (to_pterm lhs⇩β' ⋅ ⟨single_Δ2.As⟩⇩β)|_(var_poss_list l' !i)"
proof-
  let ?xi="vars_term_list l' !i"
  let ?pi="var_poss_list l' !i"
  from i have i':"i < length (vars_term_list (to_pterm l'))"
    by (metis vars_to_pterm)
  moreover then have "i < length (var_poss_list (to_pterm l'))"
    by (simp add: length_var_poss_list) 
  ultimately have match_subst:"(?xi, (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)|_?pi) = (match_substs (to_pterm l') (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β))!i" 
    unfolding match_substs_def var_poss_list_to_pterm vars_to_pterm by simp 
  have "?xi ∉ vars_term l"
    by (metis (no_types, lifting) i' disjoint_iff distinct distinct_append nth_mem set_vars_term_list vars_to_pterm) 
  then have "ρ ?xi = (mk_subst Var (match_substs (to_pterm l') (to_pterm lhs⇩β' ⋅ ⟨single_Δ2.As⟩⇩β))) ?xi" 
    unfolding rho_substs_def using mk_subst_concat
    by (smt (verit) length_map linear_l linear_term_var_vars_term_list map_fst_zip set_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term)
  moreover have "distinct (map fst (match_substs (to_pterm l') (to_pterm lhs⇩β' ⋅ ⟨single_Δ2.As⟩⇩β)))"
    by (smt (verit, best) distinct_rev length_map length_var_poss_list linear_l' linear_term_var_vars_term_list map_fst_zip match_substs_def o_apply remdups_id_iff_distinct rev_swap vars_to_pterm) 
  ultimately show ?thesis 
    using i' mk_subst_distinct by (smt (z3) length_map length_var_poss_list map_fst_zip match_subst match_substs_def nth_zip prod.simps(1)) 
qed

lemma source_rho: "l ⋅ (source ∘ ρ) = s|_q" 
proof-
  {fix y assume "y ∈ vars_term (lhs β)"
    then obtain j where j:"j < length (var_rule β)" "var_rule β !j = y"
      by (metis in_set_conv_nth single_Δ2.lin_lhs linear_term_var_vars_term_list set_vars_term_list) 
    then have "vars_distinct l ! j = x_var y"
      by (metis linear_l linear_term_var_vars_term_list nth_map single_Δ2.lin_lhs vars_map_vars_term) 
    then have "ρ (x_var y) = Bs!j" 
      using var_l_rho j by (smt (verit, best) length_map linear_l linear_term_var_vars_term_list single_Δ2.lin_lhs vars_map_vars_term) 
    then have "(ρ ∘ x_var) y = (⟨Bs⟩⇩β) y"
      using j by (smt (verit, ccfv_SIG) length_map lhs_subst_var_i map_map nth_map single_Δ2.length_as) 
    then have "(source ∘ ρ ∘ x_var) y = (⟨map source Bs⟩⇩β) y"
      using j by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map o_apply single_Δ2.length_as) 
  }
  then have "l ⋅ (source ∘ ρ) = source (Prule β Bs)" 
    unfolding apply_subst_map_vars_term source.simps using term_subst_eq_conv by blast 
  then show ?thesis
    using co_init s_def single_Δ2.aq single_Δ2.source_at_pq by presburger
qed

lemma source_rho_sigma:"source ∘ ρ = σ" 
proof
  fix x
  show "(source ∘ ρ) x = σ x" proof(cases "x ∈ vars_term l")
    case True
    then show ?thesis using source_rho
      by (smt (verit, best) l_sigma_subst term_subst_eq_conv) 
  next
    case False
    note false'=this
    then have rho:"ρ x = (mk_subst Var rho_substs) x"
      by (smt (verit) length_map linear_l linear_term_var_vars_term_list map_fst_zip mk_subst_concat set_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term) 
    then show ?thesis proof(cases "x ∈ vars_term l'")
      case True
      have well:"to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β ∈ wf_pterm S" 
        using single_Δ2.as_well lhs_subst_well_def to_pterm_wf_pterm by blast
      from True obtain i where i:"i < length (vars_term_list l')" "(vars_term_list l')!i = x"
        by (metis in_set_conv_nth set_vars_term_list) 
      let ?q="var_poss_list l' ! i"
      let ?u="(to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)|_?q"
      from i have rho:"ρ x = ?u"
        using var_l'_rho by blast 
      have q_facts:"?q ∈ poss (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) ∧ labeled_source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) |_ ?q = labeled_source ((to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) |_ ?q)" proof-
          have "?q ∈ poss (source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β))" proof-
          have "source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) = s|_p"
            unfolding p by (metis (no_types, lifting) co_init fun_mk_subst fun_poss_imp_poss p_q_pos(2) q'_poss s_def single_Δ2.aq single_Δ2.source_at_pq source.simps(1) source.simps(3) source_apply_subst source_to_pterm subt_at_append subt_at_subst to_pterm_wf_pterm) 
          moreover have "?q ∈ poss (s|_p)" 
            using l'_sigma_subst by (metis i(1) length_var_poss_list nth_mem poss_imp_subst_poss var_poss_imp_poss var_poss_list_sound)
          ultimately show ?thesis by presburger 
        qed
        moreover 
        {fix r assume le:"r <⇩p ?q"
          have "?q ∈ poss l'"
            by (metis i(1) length_var_poss_list nth_mem var_poss_imp_poss var_poss_list_sound) 
          with le have "r ∈ fun_poss l'"  
            using fun_poss_append_poss by (metis less_pos_def') 
          then have "r ∉ possL (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)" 
            using innermost_ov_contr by blast 
        }
        ultimately show ?thesis
          using single_Δ2.unlabeled_above_p well by blast 
      qed
      have "source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) = s|_p"
        by (metis (no_types, lifting) co_init fun_mk_subst fun_poss_imp_poss p p_q_pos(2) q'_poss s_def single_Δ2.aq single_Δ2.source_at_pq source.simps(1) source.simps(3) source_apply_subst source_to_pterm subt_at_append subt_at_subst to_pterm_wf_pterm) 
      moreover have "σ x = s|_(p@?q)"
        using i sigma_vars by blast
      moreover from q_facts have "source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) |_ ?q = source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β |_ ?q)"
        unfolding labeled_source_to_term var_poss_list_map_vars_term
        by (smt (verit, del_insts) calculation(1) i(1) l'_sigma_subst labeled_source_to_term length_var_poss_list nth_mem poss_imp_subst_poss poss_term_lab_to_term term_lab_to_term_subt_at var_poss_imp_poss var_poss_list_map_vars_term var_poss_list_sound)  
      ultimately have "source ?u = σ x"
        using labeled_source_to_term term_lab_to_term_subt_at  by (simp add: p_q_pos(1) term_lab_to_term_subt_at) 
      with rho show ?thesis
        by simp 
    next
      case False
      with false' have "x ∉ set (vars_term_list l @ vars_term_list l')" 
        unfolding set_append by simp
      then have "σ x = Var x"
        unfolding σ_simp using mk_subst_not_mem by (metis (no_types, lifting)) 
      moreover have "ρ x = Var x"
        unfolding rho rho_substs_def match_substs_def using false' False
        by (smt (verit, del_insts) length_map linear_l linear_term_var_vars_term_list map_fst_zip mk_subst_concat mk_subst_not_mem set_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term vars_to_pterm) 
      ultimately show ?thesis by simp
    qed
  qed
qed

abbreviation "A' ≡ the (A re Δ1)"
abbreviation "B' ≡ (ctxt_of_pos_term q⇩β B) ⟨D'⋅ρ⟩"

lemma source_B': "source B' = source A'"
proof-
  have "source B' = replace_at s p ((rename_y (rhs α)) ⋅ τ ⋅ σ)" 
  proof- 
    have well_ctxt:"ctxt_of_pos_term q⇩β B ∈ wf_pterm_ctxt S"
      using B ctxt_of_pos_term_well single_Δ2.q by auto 
    have src_d'_rho:"source (D' ⋅ ρ) = (ctxt_of_pos_term q' (l ⋅ (source ∘ ρ)))⟨rename_y (rhs α) ⋅ τ ⋅ σ⟩"
      unfolding source_apply_subst[OF d'_well] src_d' subst_apply_term_ctxt_apply_distrib 
      using ctxt_of_pos_term_subst source_rho_sigma 
      by (metis fun_poss_imp_poss poss_map_vars_term q'_poss)
    show ?thesis
      using single_Δ2.source_ctxt_apply_term[OF well_ctxt] single_Δ2.pq[symmetric] src_d'_rho source_rho co_init s_def
      by (metis ctxt_apply_ctxt_apply ctxt_supt_id p p_q_pos(2)) 
  qed
  moreover have "source A' = replace_at s p ((rename_y (rhs α)) ⋅ τ ⋅ σ)"
  proof-
    {fix x assume "x ∈ vars_term (rhs α)"
      with single_Δ1.rule_in_TRS have x:"x ∈ vars_term (lhs α)" 
        using wf_trs_R unfolding wf_trs_def var_rhs_subset_lhs_def by blast
      then have "(⟨map (λpi. s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α) x = ((Var ∘ y_var) x) ⋅ τ ⋅ σ"
      proof-
        from x obtain i where i:"x = var_rule α!i" and len:"i < length (var_rule α)"
          by (metis in_set_conv_nth linear_term_var_vars_term_list single_Δ1.lin_lhs set_vars_term_list)
        then have len2:"i < length (var_poss_list (lhs α))"
          by (metis length_var_poss_list linear_term_var_vars_term_list single_Δ1.lin_lhs)  
        then have left:"(⟨map (λpi. s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α) x = s |_ (p @ (var_poss_list (lhs α)!i))" 
          using lhs_subst_var_i[OF i len] by (smt (z3) length_map nth_map) 
        from i have "x = vars_term_list (lhs α) ! i"
          by (metis linear_term_var_vars_term_list single_Δ1.lin_lhs) 
        with len2 have "((y_var) x) = vars_term_list (rename_y (lhs α))!i" 
          using vars_map_vars_term by (metis length_var_poss_list nth_map)
        with len2 have right:"((Var ∘ y_var) x) ⋅ τ ⋅ σ = s |_ (p @ (var_poss_list (lhs α)!i))" 
          using sigma_tau_vars var_poss_list_map_vars_term
          by (smt (verit, best) comp_apply filter_cong length_var_poss_list eval_term.simps(1) subst_subst_compose) 
        show ?thesis unfolding left right by simp
      qed
    }
    then have "rhs α ⋅ ⟨map (λpi. s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α = (rename_y (rhs α)) ⋅ τ ⋅ σ"
      using term_subst_eq_conv[where τ="(Var ∘ y_var) ∘⇩s τ ∘⇩s σ"] 
      unfolding map_vars_term_eq by (simp add: subst_compose)
    then have "target Δ1 = replace_at s p ((rename_y (rhs α)) ⋅ τ ⋅ σ)"
      using p_q_pos target_single_redex by fastforce
    then show ?thesis
      using A residual_src_tgt single_Δ1.delta_trs_wf_pterm single_Δ1.residual by fastforce
  qed
  ultimately show ?thesis by simp
qed

lemma B'_well: "B' ∈ wf_pterm S" 
proof-
  have vars_d':"vars_term D' = vars_term (ctxt_of_pos_term q' l)⟨(rename_y (rhs α) ⋅ τ)⟩" 
    using src_d' vars_term_source by (metis d'_well)
  have vars_d:"vars_term D' ⊆ (vars_term l) ∪ (vars_term l')" proof-
    have "vars_term (rhs α) ⊆ vars_term (lhs α)" 
      using single_Δ1.rule_in_TRS wf_trs_R unfolding wf_trs_def var_rhs_subset_lhs_def by blast
    then have "vars_term (rename_y (rhs α)) ⊆ vars_term l'"
       by (simp add: image_mono term.set_map(2)) 
    moreover 
    {fix x assume x:"x ∈ vars_term l'"
      then have "vars_term (τ x) ⊆ vars_term l ∪ vars_term l'" proof(cases "x ∈ set (map fst (right_substs l'' l'))")
        case True
        then obtain u where u:"(x, u) ∈ set (right_substs l'' l')" by auto
        then have "vars_term u ⊆ vars_term l"
          by (smt (verit, best) fun_poss_imp_poss poss_map_vars_term q'_poss right_substs_imp_props subset_trans vars_term_subt_at) 
        with u show ?thesis
          using innermost_overlap.apply_tau2 innermost_overlap_axioms by blast 
      next
        case False
        moreover from x have "x ∉ set (map fst (left_substs l'' l'))"
          by (metis imageE l''_alt list.set_map map_fst_left_substs set_vars_term_list subsetD vars_map_vars_term x_diff_y)
        ultimately have "τ x = Var x" unfolding τ_def
          by (metis Un_iff map_append not_elem_subst_of set_append) 
        then show ?thesis 
          using x by simp
      qed
    }
    ultimately show ?thesis using vars_d' unfolding vars_term_ctxt_apply vars_term_subst
      by (smt (verit, del_insts) UN_extend_simps(10) UN_iff UnCI UnE ctxt_supt_id fun_poss_imp_poss poss_map_vars_term q'_poss subset_eq vars_term_ctxt_apply)
  qed         
  {fix x assume "x ∈ vars_term D'"
    then consider "x ∈ vars_term l" | "x ∈ vars_term l'" 
      using vars_d by blast
    then have "ρ x ∈ wf_pterm S" proof(cases)
      case 1
      then obtain j where j:"j < length (vars_distinct l)" "vars_distinct l ! j = x"
        by (metis in_set_idx linear_l linear_term_var_vars_term_list set_vars_term_list) 
      then show ?thesis
        using var_l_rho by (smt (verit, best) length_map linear_l linear_term_var_vars_term_list single_Δ2.as_well single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term)
    next
      case 2
      then obtain i where i:"i < length (vars_term_list (to_pterm l'))" "vars_term_list (to_pterm l')!i = x"
        by (metis in_set_conv_nth set_vars_term_list vars_to_pterm)
      then have i':"i < length (vars_term_list l')"
        by (metis vars_to_pterm)
      from i have i'':"vars_term_list l'!i = x"
        by (metis vars_to_pterm)
      have well:"to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β ∈ wf_pterm S" 
        using single_Δ2.as_well lhs_subst_well_def to_pterm_wf_pterm by blast
      let ?q="var_poss_list (to_pterm l') ! i"
      let ?u="(to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)|_?q"
      have q_facts:"?q ∈ poss (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)" proof-
          have "?q ∈ poss (source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β))" proof-
          have "source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) = s|_p"
            unfolding p by (metis (no_types, lifting) co_init fun_mk_subst fun_poss_imp_poss p_q_pos(2) q'_poss s_def single_Δ2.aq single_Δ2.source_at_pq source.simps(1) source.simps(3) source_apply_subst source_to_pterm subt_at_append subt_at_subst to_pterm_wf_pterm) 
          moreover have "?q ∈ poss (s|_p)" 
            using l'_sigma_subst by (metis i' length_var_poss_list nth_mem poss_imp_subst_poss var_poss_imp_poss var_poss_list_sound var_poss_list_to_pterm)
          ultimately show ?thesis by presburger 
        qed
        moreover 
        {fix r assume le:"r <⇩p ?q"
          have "?q ∈ poss l'" 
            using i by (metis length_var_poss_list nth_mem var_poss_imp_poss var_poss_list_sound var_poss_list_to_pterm)
          with le have "r ∈ fun_poss l'"  
            using fun_poss_append_poss by (metis less_pos_def') 
          then have "r ∉ possL (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)" 
            using innermost_ov_contr by blast 
        }
        ultimately show ?thesis 
          using single_Δ2.unlabeled_above_p well by blast 
      qed
      with well show ?thesis
        by (metis i' i'' subt_at_is_wf_pterm var_l'_rho var_poss_list_to_pterm)
    qed
  }
  then have "D' ⋅ ρ ∈ wf_pterm S"
    using d'_well by (meson apply_subst_wf_pterm) 
  then show ?thesis
    using ctxt_wf_pterm[OF B single_Δ2.q] by blast
qed

lemma measure_helper:
  assumes r1:"r ∈ possL A'" and r2:"r ∈ possL B'"
  shows "¬ p ≤⇩p r"
proof
  assume "p ≤⇩p r" 
  then obtain r' where r':"r = p@r'"
    using prefix_def by auto 
  from r1 single_Δ1.label_ctxt[OF A single_Δ1.pq single_Δ1.p single_Δ1.q] have "r' ∈ possL (to_pterm (rhs α) ⋅ ⟨As⟩⇩α)"
    unfolding single_Δ1.residual option.sel r' by force 
  then consider "r' ∈ possL (to_pterm (rhs α))" | 
     "∃ r1 r2 x. r' = r1@r2 ∧ r1 ∈ poss (labeled_source (to_pterm (rhs α))) ∧ (labeled_source (to_pterm (rhs α)))|_r1 = Var x ∧ 
                 r2 ∈ labelposs ((labeled_source ∘ ⟨As⟩⇩α) x)"
    using labelposs_subst labeled_source_apply_subst  by (metis (no_types, lifting) to_pterm_wf_pterm)
  then show False proof(cases)
    case 1
    then have False
      by (simp add: labeled_source_simple_pterm) 
    then show ?thesis by simp
  next
    case 2
    then obtain r1 r2 x where r1r2:"r' = r1@r2" and r1_pos:"r1 ∈ poss (labeled_source (to_pterm (rhs α)))"
       "(labeled_source (to_pterm (rhs α)))|_r1 = Var x" and r2_lab:"r2 ∈ labelposs ((labeled_source ∘ ⟨As⟩⇩α) x)"
      by blast
    then have "x ∈ vars_term (rhs α)"
      by (metis in_mono labeled_source_to_term poss_term_lab_to_term source_to_pterm term.set_intros(3) var_term_lab_to_term vars_term_subt_at)
    then have "x ∈ vars_term (lhs α)" 
      using single_Δ1.rule_in_TRS wf_trs_R unfolding wf_trs_def var_rhs_subset_lhs_def by blast
    then obtain i where i:"i < length (var_rule α)" "(var_rule α)!i = x"
      by (metis in_set_idx linear_term_var_vars_term_list set_vars_term_list single_Δ1.lin_lhs) 
    with r2_lab have r2_lab':"r2 ∈ possL (As!i)"
      by (metis lhs_subst_var_i o_apply single_Δ1.length_as) 
    then obtain γ n where γ:"get_label (labeled_source (As!i) |_r2) = Some (γ, n)"
      using possL_obtain_label by blast 
    let ?rγ="take (length r2 - n) r2"
    let ?pi="var_poss_list (labeled_lhs α)!i"
    from γ have n:"n ≤ length (r2)"
      using i(1) label_term_max_value labelposs_subs_poss r2_lab' single_Δ1.as_well by fastforce 
    from γ have oc5:"n ≤ length (p@?pi@r2)"
      using i(1) label_term_max_value labelposs_subs_poss r2_lab' single_Δ1.as_well by fastforce 
    have i':"i < length (vars_term_list (labeled_lhs α))"
      by (metis i(1) linear_term_var_vars_term_list single_Δ1.lin_lhs vars_term_list_labeled_lhs) 
    then have pi_pos:"?pi ∈ poss (labeled_lhs α)"
      by (metis length_var_poss_list nth_mem var_poss_imp_poss var_poss_list_sound)  
    have pi_not_empty:"?pi ≠ []" proof-
      from single_Δ1.rule_in_TRS have "is_Fun (lhs α)"
        using wf_trs_R unfolding wf_trs_def no_var_lhs_def by force 
      then have "[] ∉ var_poss (lhs α)"
        by fastforce
      moreover have "var_poss_list (labeled_lhs α) = var_poss_list (lhs α)"
        using var_poss_list_labeled_lhs by blast
      ultimately show ?thesis
        by (metis i' length_var_poss_list nth_mem var_poss_list_sound) 
    qed
    have as_i:"(⟨map labeled_source As⟩⇩α) (vars_term_list (labeled_lhs α) ! i) = labeled_source (As!i)"
      by (smt (verit, ccfv_SIG) i(1) length_map lhs_subst_var_i linear_term_var_vars_term_list nth_map single_Δ1.length_as single_Δ1.lin_lhs vars_term_list_labeled_lhs) 
    with r2_lab' i' have "?pi@r2 ∈ possL (Prule α As)" 
      unfolding labeled_source.simps set_labelposs_subst by (smt (verit, ccfv_threshold) UN_iff UnCI lessThan_iff mem_Collect_eq)
    then have oc1:"p@?pi@r2 ∈ possL A" 
      using single_Δ1.a single_Δ1.label_ctxt[OF A single_Δ1.pq single_Δ1.p single_Δ1.q]
      by (metis (no_types, lifting) get_label_imp_labelposs in_mono labeled_source_to_term labelposs_subs_poss option.discI p_q_pos(1) pos_append_poss possL_obtain_label poss_term_lab_to_term s_def single_Δ1.aq single_Δ1.labeled_source_at_pq subt_at_append)
    from γ have "get_label (labeled_source (Prule α As) |_(?pi@r2)) = Some (γ, n)" 
      unfolding labeled_source.simps using as_i subt_at_append subt_at_subst pi_pos
      by (smt (verit, best) filter_cong fun_poss_imp_poss i' labeled_source.simps(3) labeled_source_to_term labelposs_subs_fun_poss_source oc1 poss_append_poss poss_term_lab_to_term single_Δ1.aq single_Δ1.labeled_source_at_pq eval_term.simps(1) vars_term_list_var_poss_list) 
    then have oc3:"get_label (labeled_source A |_(p@?pi@r2)) = Some (γ, n)" 
      using single_Δ1.a single_Δ1.pq  single_Δ1.labeled_source_at_pq by (simp add: single_Δ1.aq single_Δ1.p)
    from r1_pos have yx:"rename_y (rhs α) |_r1 = Var (y_var x)"
      by (metis Term.term.simps(9) labeled_source_to_term map_vars_term_subt_at poss_term_lab_to_term source_to_pterm var_term_lab_to_term) 
    then have li:"y_var x = vars_term_list l' ! i"
      by (metis i linear_term_var_vars_term_list nth_map single_Δ1.lin_lhs vars_map_vars_term) 
    from r2 single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] have "q'@r' ∈ possL (D' ⋅ ρ)"
      unfolding r' p by force 
    then consider "q'@r' ∈ possL D'" | 
     "∃ r1 r2 x. q'@r' = r1@r2 ∧ r1 ∈ poss (labeled_source D') ∧ (labeled_source D')|_r1 = Var x ∧ 
                 r2 ∈ labelposs ((labeled_source ∘ ρ) x)"
    using labelposs_subst labeled_source_apply_subst d'_well by (metis (no_types, lifting))
    then show ?thesis proof(cases)
      case 1
      then have "q'@r' ∈ fun_poss (source D')"
        using labelposs_subs_fun_poss_source by auto 
      then have r'_pos:"r' ∈ fun_poss (rename_y (rhs α) ⋅ τ)" 
        unfolding src_d' using fun_poss_in_ctxt fun_poss_imp_poss hole_pos_ctxt_of_pos_term poss_map_vars_term q'_poss by blast 
      from yx have "rename_y (rhs α) ⋅ τ |_r1 = τ (y_var x)"
        using r1_pos(1) by force 
      then have r2_funp:"r2 ∈ fun_poss (τ (y_var x))"
        unfolding r1r2 by (metis fun_poss_in_ctxt fun_poss_imp_poss hole_pos_ctxt_of_pos_term poss_append_poss r'_pos r1r2 replace_at_ident)  
      then have "τ (y_var x) ≠ Var (y_var x)"
        by force  
      then have "var_poss_list l' ! i ∈ fun_poss l''" 
        using var_in_domain_tau li i' by (smt (verit, del_insts) length_map vars_map_vars_term vars_term_list_labeled_lhs) 
      then have *:"?pi ∈ fun_poss l''"
        by (metis var_poss_list_labeled_lhs var_poss_list_map_vars_term) 
      have "((y_var x), l''|_?pi) ∈ set (right_substs l'' l')" proof-
        have "?pi ∈ poss l'" 
          using pi_pos by auto 
        moreover have "l'|_?pi = Var (y_var x)"
          by (smt (verit, ccfv_SIG) Term.term.simps(9) calculation filter_cong i' i(2) label_term_to_term linear_term_var_vars_term_list map_vars_term_subt_at pi_pos poss_map_vars_term single_Δ1.lin_lhs var_term_lab_to_term vars_term_list_labeled_lhs vars_term_list_var_poss_list) 
        ultimately show ?thesis
          using props_imp_right_substs[OF *] by metis
      qed
      then have "τ (y_var x) = l''|_?pi"
        using apply_tau2 by blast 
      with r2_funp have "r2 ∈ fun_poss (l''|_?pi)"
        by simp 
      then have "q'@?pi@r2 ∈ fun_poss l"
        by (smt (verit, del_insts) Diff_iff ‹var_poss_list (labeled_lhs α) ! i ∈ fun_poss (l |_ q')› fun_poss_map_vars_term pos_append_poss poss_simps(3) q'_poss subterm_poss_conv var_poss_iff)
      then have funpos:"q'@?pi@r2 ∈ fun_poss (lhs β)"
        using fun_poss_map_vars_term by blast
      then have lab_beta:"get_label (labeled_source (Prule β Bs) |_(q'@?pi@r2)) = Some (β, length (q'@?pi@r2))" 
        using label_term_increase unfolding labeled_source.simps
        by (metis (no_types, lifting) length_0_conv length_append self_append_conv2)
      then have oc4:"get_label (labeled_source B |_(p@?pi@r2)) = Some (β, length (q'@?pi@r2))" proof-
        have "labeled_source B = (ctxt_of_pos_term q (labeled_source B))⟨labeled_source (Prule β Bs)⟩"
          using single_Δ2.a single_Δ2.label_source_ctxt[OF B single_Δ2.pq] by (metis single_Δ2.p single_Δ2.q)
        then have "labeled_source B |_(p@?pi@r2) = labeled_source (Prule β Bs) |_(q'@?pi@r2)"
          unfolding p using co_init p_q_pos(2) s_def single_Δ2.aq single_Δ2.labeled_source_at_pq by auto      
        then show ?thesis
          using lab_beta unfolding p by simp 
      qed
      then have oc2:"p @ ?pi @ r2 ∈ possL B"
        by (metis co_init fun_poss_imp_poss get_label_imp_labelposs labeled_source_to_term labelposs_subs_fun_poss_source oc1 option.discI poss_term_lab_to_term)
      have **:"take (length (p @ ?pi @ r2) - n) (p @ ?pi @ r2) = p@?pi@?rγ" 
        using n by simp
      have *:"take (length (p @ ?pi @ r2) - length (q' @ var_poss_list (labeled_lhs α) ! i @ r2)) (p @ var_poss_list (labeled_lhs α) ! i @ r2) = q"
        unfolding p by simp     
      have "(p@?pi@?rγ, q) ∈ overlaps_pos (labeled_source A) (labeled_source B)"
        using obtain_overlap[OF oc1 oc2 oc3 oc4 oc5] A B unfolding * ** using p
        by (smt (verit, ccfv_SIG) "*" append.assoc diff_is_0_eq less_eq_pos_simps(1) nat_le_linear self_append_conv2 take_eq_Nil2) 
      then show ?thesis using maximal pi_not_empty
        by (metis (no_types, lifting) append_is_Nil_conv fst_conv less_eq_overlap_def less_eq_pos_simps(1) self_append_conv snd_conv) 
    next
      case 2
      then obtain r3 r4 y where r3r4:"q' @ r' = r3 @ r4" "r3 ∈ poss (labeled_source D')" 
        "labeled_source D' |_ r3 = Var y" "r4 ∈ labelposs ((labeled_source ∘ ρ) y)" 
        by blast 
      then have r3_pos:"r3 ∈ poss (source D')" by simp
      from r3r4 have y:"source D' |_r3 = Var y"
        by (metis labeled_source_to_term var_term_lab_to_term) 
      have "q'@r1 ≤⇩p r3" proof-
        from r3r4(1) have "q'@r1@r2 = r3@r4" 
          unfolding r1r2 by simp
        then consider "q'@r1 ≤⇩p r3" | "r3 <⇩p q'@r1"
          by (metis append.assoc less_eq_pos_simps(1) pos_cases pos_less_eq_append_not_parallel) 
        then show ?thesis proof(cases)
          case 2
          have "q'@r1 ∈ poss (ctxt_of_pos_term q' l)⟨rename_y (rhs α)⟩"
            using r1_pos poss_term_lab_to_term
            by (metis fun_poss_imp_poss hole_pos_ctxt_of_pos_term hole_pos_poss labeled_source_to_term pos_append_poss poss_map_vars_term q'_poss replace_at_subt_at source_to_pterm) 
          then have "r3 ∈ fun_poss (source D')" 
            unfolding src_d' by (metis "2" ctxt_l_at_q' fun_poss_append_poss less_pos_def' poss_imp_subst_poss subst_apply_term_ctxt_apply_distrib) 
          then have False using r3r4
            by (metis fun_poss_fun_conv fun_poss_term_lab_to_term labeled_source_to_term term.distinct(1)) 
          then show ?thesis by simp
        qed simp
      qed
      then obtain r3' where r3:"r3 = q'@r1@r3'" unfolding prefix_def by auto 
      have r3'_pos:"r3' ∈ poss (τ (y_var x))" 
        using r3_pos y unfolding r3 src_d' using yx
        by (metis fun_poss_imp_poss labeled_source_to_term poss_map_vars_term poss_term_lab_to_term q'_poss r1_pos(1) replace_at_subt_at source_to_pterm eval_term.simps(1) subt_at_subst subterm_poss_conv) 
      have r3'_y:"(τ (y_var x))|_r3' = Var y" 
        using r3_pos y unfolding r3 src_d' using yx
        by (metis fun_poss_imp_poss labeled_source_to_term poss_map_vars_term poss_term_lab_to_term q'_poss r1_pos(1) replace_at_subt_at source_to_pterm eval_term.simps(1) subt_at_subst subterm_poss_conv)
      then show ?thesis proof(cases "?pi ∈ fun_poss l''")
        case True
        have "((y_var x), l''|_?pi) ∈ set (right_substs l'' l')" proof-
          have "?pi ∈ poss l'" 
            using pi_pos by auto 
          moreover have "l'|_?pi = Var (y_var x)"
            by (smt (verit, ccfv_SIG) Term.term.simps(9) calculation filter_cong i' i(2) label_term_to_term linear_term_var_vars_term_list map_vars_term_subt_at pi_pos poss_map_vars_term single_Δ1.lin_lhs var_term_lab_to_term vars_term_list_labeled_lhs vars_term_list_var_poss_list) 
          ultimately show ?thesis
            using props_imp_right_substs[OF True] by metis
        qed
        then have l''_pi:"τ (y_var x) = l''|_?pi"
          using apply_tau2 by blast 
        with r3'_pos y yx have "y ∈ vars_term l''" 
          unfolding src_d' r3
          by (smt (verit, ccfv_SIG) True fun_poss_imp_poss labeled_source_to_term pos_append_poss poss_map_vars_term poss_term_lab_to_term q'_poss r1_pos(1) r3 r3_pos replace_at_subt_at source_to_pterm src_d' eval_term.simps(1) subt_at_subst subterm_poss_conv var_poss_iff vars_term_var_poss_iff) 
        then obtain j where j:"vars_term_list l ! j = y" "j < length (vars_term_list l)"
          by (smt (verit, best) fun_poss_imp_poss in_set_conv_nth poss_map_vars_term q'_poss set_vars_term_list subsetD vars_term_subt_at) 
        then have bsj:"ρ y = Bs!j" 
          using var_l_rho linear_l by (metis (no_types, lifting) linear_term_var_vars_term_list) 

        from r3r4 obtain δ m where δ:"get_label (labeled_source (ρ y) |_r4) = Some (δ, m)"
          using possL_obtain_label by fastforce 
        then have oc6:"m ≤ length r4" 
          unfolding bsj using label_term_max_value
          by (smt (verit, best) bsj in_mono j(2) labelposs_subs_poss length_map linear_term_var_vars_term_list o_apply r3r4(4) single_Δ2.as_well single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term) 
        let ?rδ="take (length r4 - m) r4"
        have qj:"q' @ ?pi @ r3' = var_poss_list (labeled_lhs β) !j" proof-
          have "l |_ (q' @ var_poss_list (labeled_lhs α) ! i @ r3') = τ (y_var x) |_ r3'"
            using l''_pi by (simp add: True fun_poss_imp_poss q'_poss) 
          then have "l|_(q' @ ?pi @ r3') = Var y"
            using r3'_y by presburger
          with j have "q' @ ?pi @ r3' = var_poss_list l !j"
            using linear_l
            by (smt (verit, ccfv_SIG) True fun_poss_imp_poss l''_pi length_var_poss_list linear_term_unique_vars nth_mem pos_append_poss poss_map_vars_term q'_poss r3'_pos var_poss_imp_poss var_poss_list_sound vars_term_list_var_poss_list)
          then show ?thesis
            by (metis var_poss_list_labeled_lhs var_poss_list_map_vars_term)  
        qed
        have "get_label (labeled_source (Prule β Bs) |_(q'@?pi@r3'@r4)) = Some (δ, m)"
        proof-
          from qj have sub_pos:"q' @ ?pi @ r3' ∈ poss (labeled_lhs β)"
            by (metis True ‹τ (y_var x) = l |_ q' |_ ?pi› fun_poss_imp_poss label_term_to_term pos_append_poss poss_map_vars_term poss_term_lab_to_term q'_poss r3'_pos) 
          from qj have "labeled_lhs β |_(q' @ ?pi @ r3') = Var (vars_term_list (labeled_lhs β) ! j)"
            by (smt (verit) filter_cong j(2) length_map vars_map_vars_term vars_term_list_labeled_lhs vars_term_list_var_poss_list) 
          moreover have "(⟨map labeled_source Bs⟩⇩β) (vars_term_list (labeled_lhs β) ! j) = labeled_source (Bs ! j)" 
            using j by (smt (verit, del_insts) length_map lhs_subst_var_i linear_term_var_vars_term_list nth_map single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term vars_term_list_labeled_lhs) 
          then have "labeled_source (Prule β Bs) |_(q'@?pi@r3') = labeled_source (Bs ! j)" 
            unfolding labeled_source.simps subt_at_subst[OF sub_pos] using calculation by force
          then have "labeled_source (Prule β Bs) |_(q'@?pi@r3'@r4) = labeled_source (Bs ! j) |_r4" 
            using sub_pos by (smt (verit, ccfv_SIG) labeled_source.simps(3) poss_append_poss poss_imp_subst_poss subt_at_append)
          with bsj δ show ?thesis 
            by presburger
        qed
        then have oc4:"get_label (labeled_source B |_((p@?pi)@r3'@r4)) = Some (δ, m)"
          unfolding p using single_Δ2.a co_init p_q_pos(2) s_def single_Δ2.aq single_Δ2.labeled_source_at_pq by auto 
        have "((p@?pi)@r3'@r4) ∈ possL B" proof-
          have "r4 ∈ possL (Bs!j)" 
            using qj r3r4(4) δ bsj
            by (smt (verit, ccfv_SIG) δ get_label_imp_labelposs in_mono j(2) labelposs_subs_poss length_map linear_term_var_vars_term_list o_apply obtain_label_root option.discI single_Δ2.as_well single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term)
          moreover have "(⟨map labeled_source Bs⟩⇩β) (vars_term_list (labeled_lhs β) ! j) = labeled_source (Bs!j)" 
            using j(2)
            by (smt (verit, del_insts) apply_lhs_subst_var_rule length_map linear_term_var_vars_term_list nth_map single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term vars_term_list_labeled_lhs) 
          ultimately have "q' @ ?pi @ r3'@r4 ∈ possL (Prule β Bs)"
            unfolding labeled_source.simps set_labelposs_subst using qj j(2)
            by (smt (verit, ccfv_threshold) UN_iff UnCI append_assoc length_map lessThan_iff mem_Collect_eq vars_map_vars_term vars_term_list_labeled_lhs)
          then show ?thesis 
            using single_Δ2.a single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] qj unfolding p
            by (metis (no_types, lifting) append.assoc labeled_source_to_term labelposs_subt_at poss_term_lab_to_term single_Δ2.aq single_Δ2.labeled_source_at_pq single_Δ2.p) 
        qed
        moreover have r2:"r2 = r3'@r4"
          using r3 r3r4(1) r1r2 by auto 
        ultimately have oc2:"(p@?pi@r2) ∈ possL B" 
          by simp
        from r2 oc4 have oc4:"get_label (labeled_source B |_ (p @ ?pi @ r2)) = Some (δ, m)" 
          by simp
        have *:"take (length (p @ ?pi @ r2) - n) (p @ ?pi @ r2) = p@?pi@?rγ" 
          using n by simp
        have **:"take (length (p @ ?pi @ r2) - m) (p @ ?pi @ r2) = p@?pi@r3'@?rδ" 
          unfolding r2 using oc6 by simp
        from r2 consider "r3'@?rδ ≤⇩p ?rγ" | "?rγ <⇩p r3'@?rδ"
          by (metis append_take_drop_id prefix_def less_eq_pos_simps(2) pos_cases pos_less_eq_append_not_parallel) 
        then have "(p@?pi@?rγ, p@?pi@r3'@?rδ) ∈ overlaps_pos (labeled_source A) (labeled_source B)" proof(cases)
          case 1
            show ?thesis 
              using obtain_overlap[OF oc1 oc2 oc3 oc4 oc5] using r2 oc6 1 A B unfolding * **
              by (metis (no_types, lifting) "**" append_is_Nil_conv diff_is_0_eq less_eq_pos_simps(2) nat_le_linear pi_not_empty take_eq_Nil2) 
          next
            case 2 
            from oc6 r2 have oc6:"m ≤ length (p @ var_poss_list (labeled_lhs α) ! i @ r2)" 
              by simp
            have "(p@?pi@r3'@?rδ, p@?pi@?rγ) ∈ overlaps_pos (labeled_source B) (labeled_source A)"  
              using obtain_overlap[OF oc2 oc1 oc4 oc3 oc6 oc5] using r2 2 A B unfolding * **
              by (meson less_eq_pos_simps(2) prefix_order.less_le_not_le) 
            then show ?thesis 
              using overlaps_pos_symmetric by blast 
        qed
        then show ?thesis using maximal pi_not_empty
          by (smt (verit) append.assoc append_is_Nil_conv fst_conv less_eq_overlap_def less_eq_pos_simps(1) p self_append_conv snd_conv) 
      next
        case False
        moreover have "∀q ∈ poss l'. q ≠ (var_poss_list l'!i) ⟶ l'|_q ≠ Var (y_var x)" 
          using linear_l' by (metis i(1) length_var_poss_list li linear_term_unique_vars linear_term_var_vars_term_list nth_mem single_Δ1.lin_lhs var_poss_imp_poss var_poss_list_map_vars_term var_poss_list_sound vars_term_list_var_poss_list)
        ultimately have "¬ (∃q. q ∈ fun_poss l'' ∧ q ∈ poss l' ∧ l' |_ q = Var (y_var x))"
          by (metis var_poss_list_labeled_lhs var_poss_list_map_vars_term) 
        then have "(y_var x) ∉ set (map fst (right_substs l'' l'))" 
          using right_substs_imp_props by fastforce
        moreover have "(y_var x) ∉ set (map fst (left_substs l'' l'))" 
          using li by (smt (verit, ccfv_threshold) disjoint_iff distinct distinct_append fun_poss_imp_poss i(1) in_mono length_map linear_term_var_vars_term_list map_fst_left_substs nth_mem poss_map_vars_term q'_poss set_vars_term_list single_Δ1.lin_lhs vars_map_vars_term vars_term_subt_at) 
        ultimately have "τ (y_var x) = Var (y_var x)" 
          unfolding τ_def subst_of_append
          by (metis Un_iff map_append not_elem_subst_of set_append subst_of_append)  
        moreover with r3'_pos have r3':"r3' = []" 
          by simp
        ultimately have "(y_var x) = y"
          using r3'_y by simp 
        then have "y = vars_term_list l' !i"
          using li by simp
        moreover have pi_alt:"?pi = var_poss_list l' ! i"
          by (metis var_poss_list_labeled_lhs var_poss_list_map_vars_term) 
        ultimately have "ρ y = (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)|_?pi" 
          using var_l'_rho i' by (smt (verit, del_insts) i(1) length_map linear_term_var_vars_term_list single_Δ1.lin_lhs vars_map_vars_term) 
        with r3r4(4) have "r4 ∈ possL ((to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)|_?pi)"
          by simp 
        moreover have pi_pos:"?pi ∈ poss (labeled_source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β))" proof-
          have "source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) = s|_p"
            by (metis (no_types, lifting) co_init fun_mk_subst fun_poss_imp_poss p p_q_pos(2) q'_poss s_def single_Δ2.aq single_Δ2.source_at_pq source.simps(1) source.simps(3) source_apply_subst source_to_pterm subt_at_append subt_at_subst to_pterm_wf_pterm) 
          moreover have "?pi ∈ poss (s|_p)"
            by (metis l'_sigma_subst label_term_to_term pi_pos poss_imp_subst_poss poss_map_vars_term poss_term_lab_to_term) 
          ultimately show ?thesis
            by force 
        qed
        moreover have "labeled_source (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β) |_ ?pi = labeled_source ((to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)|_?pi)" proof-
          have "to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β ∈ wf_pterm S" 
            using single_Δ2.as_well by (meson lhs_subst_well_def to_pterm_wf_pterm) 
          moreover
          {fix r assume "r <⇩p ?pi"
            then have "r ∈ fun_poss l'" 
              using pi_alt
              by (metis fun_poss_append_poss i(1) length_var_poss_list less_pos_def' linear_term_var_vars_term_list nth_mem single_Δ1.lin_lhs var_poss_imp_poss var_poss_list_map_vars_term var_poss_list_sound) 
            then have "r ∉ possL (to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β)" 
              using innermost_ov_contr by simp
          }
          ultimately show ?thesis using single_Δ2.unlabeled_above_p pi_pos
            by (smt (verit, del_insts) labeled_source_to_term poss_term_lab_to_term)        
        qed
        ultimately have "?pi@r4 ∈ possL ((to_pterm lhs⇩β' ⋅ ⟨Bs⟩⇩β))"
          using labelposs_subt_at by metis 
        then have "?pi@r4 ∈ possL (to_pterm lhs⇩β') ∨ (∃p1 p2 x. ?pi@r4 = p1 @ p2 ∧ p1 ∈ poss (labeled_source (to_pterm lhs⇩β'))  ∧ (labeled_source (to_pterm lhs⇩β')) |_ p1 = Var x ∧ p2 ∈ possL ((⟨Bs⟩⇩β) x))"
          unfolding labeled_source_apply_subst[OF to_pterm_wf_pterm[of "lhs⇩β'"]] using labelposs_subst[of "?pi@r4"] by (smt (verit, best) o_apply)
        then obtain r5 r6 y' where r5r6:"?pi@r4 = r5 @ r6" "r5 ∈ poss (labeled_source (to_pterm lhs⇩β'))" "(labeled_source (to_pterm lhs⇩β')) |_ r5 = Var y'" "r6 ∈ possL ((⟨Bs⟩⇩β) y')"
          using labeled_source_simple_pterm by blast
        from r5r6(2) have "q'@r5 ∈ poss (lhs β)"
          by (simp add: fun_poss_imp_poss q'_poss) 
        moreover from r5r6(3) have "lhs β |_(q'@r5) = Var y'"
          by (metis fun_poss_imp_poss labeled_source_to_term q'_poss r5r6(2) source_to_pterm subt_at_append var_term_lab_to_term) 
        ultimately obtain j where j:"q'@r5 = var_poss_list (lhs β) ! j" "j < length (vars_term_list (lhs β))"
          by (metis in_set_idx length_var_poss_list var_poss_iff var_poss_list_sound)
        with r5r6(3) have "vars_term_list (lhs β) ! j = y'"
          by (metis ‹lhs β |_ (q' @ r5) = Var y'› term.inject(1) vars_term_list_var_poss_list)  
        with j have bsj:"(⟨Bs⟩⇩β) y' = Bs!j"
          by (metis (no_types, lifting) lhs_subst_var_i linear_term_var_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs) 
        with r5r6(4) obtain δ m where δ:"get_label (labeled_source (Bs!j)|_r6) = Some (δ, m)"
          by (metis possL_obtain_label) 
        with bsj have m:"m ≤ length r6"
          by (metis (no_types, lifting) fun_poss_imp_poss j(2) label_term_max_value labeled_source_to_term labelposs_subs_fun_poss_source linear_term_var_vars_term_list poss_term_lab_to_term r5r6(4) single_Δ2.as_well single_Δ2.length_as single_Δ2.lin_lhs) 
        let ?rδ="take (length r6 - m) r6"
        let ?qj="var_poss_list (lhs β) ! j"
        have r2:"r2 = r4"
          using r3 r3r4(1) r1r2 r3' by auto 
        have oc2:"p @ ?pi @ r2 ∈ possL B" proof-
          from bsj r5r6(4) have "r6 ∈ possL (Bs!j)"
            by presburger 
          moreover have "(⟨map labeled_source Bs⟩⇩β) (vars_term_list (labeled_lhs β) ! j) = labeled_source (Bs!j)" 
            using j(2)
            by (smt (verit, del_insts) apply_lhs_subst_var_rule length_map linear_term_var_vars_term_list nth_map single_Δ2.length_as single_Δ2.lin_lhs vars_map_vars_term vars_term_list_labeled_lhs) 
          ultimately have "?qj@r6 ∈ possL (Prule β Bs)" 
            unfolding labeled_source.simps set_labelposs_subst 
            by (smt (z3) UN_iff UnCI filter_cong j(2) lessThan_iff mem_Collect_eq var_poss_list_labeled_lhs vars_term_list_labeled_lhs)
          then show ?thesis 
            using single_Δ2.a single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] unfolding p r2 r5r6 append.assoc using j(1)
            by (metis (mono_tags, lifting) UnCI append.assoc mem_Collect_eq) 
        qed 
        have "get_label (labeled_source (Prule β Bs) |_(?qj@r6)) = Some (δ, m)" 
        proof-
          have "labeled_source (Prule β Bs) |_(?qj) = labeled_source (Bs ! j)" 
            unfolding labeled_source.simps subt_at_subst
            by (smt (verit, ccfv_SIG) apply_lhs_subst_var_rule filter_cong j(2) length_map length_var_poss_list linear_term_var_vars_term_list map_nth_conv nth_mem single_Δ2.length_as single_Δ2.lin_lhs eval_term.simps(1) subt_at_subst var_poss_iff var_poss_list_labeled_lhs var_poss_list_sound vars_term_list_labeled_lhs vars_term_list_var_poss_list) 
          then have "labeled_source (Prule β Bs) |_(?qj@r6) = labeled_source (Bs ! j) |_r6"
            by (metis (no_types, lifting) ‹q' @ r5 ∈ poss (lhs β)› j(1) labeled_source_to_term poss_imp_subst_poss poss_term_lab_to_term source.simps(3) subt_at_append) 
          with bsj δ show ?thesis 
            by presburger
        qed
        then have oc4:"get_label (labeled_source B |_(p @ ?pi @ r2)) = Some (δ, m)"
          unfolding p r2 r5r6 append.assoc using j(1)
          by (metis append.assoc co_init labeled_source_to_term p_q_pos(2) poss_term_lab_to_term s_def single_Δ2.aq single_Δ2.labeled_source_at_pq subt_at_append) 
        have oc6:"m ≤ length (p @ ?pi @ r2)" 
          unfolding p r2 r5r6 append.assoc using j(1) m by simp
        have *:"take (length (p @ ?pi @ r2) - n) (p @ ?pi @ r2) = p@?pi@?rγ"
          using n by simp
        have **:"take (length (p @ ?pi @ r2) - m) (p @ ?pi @ r2) = q@?qj@?rδ" 
          unfolding p r2 r5r6 append.assoc using j(1) m by simp
        from r5r6(1) consider "?qj@?rδ ≤⇩p q'@?pi@ ?rγ" | "q'@?pi@ ?rγ <⇩p ?qj@?rδ"
          unfolding j(1)[symmetric] r2
          by (metis append_assoc append_take_drop_id less_eq_pos_simps(1) pos_cases pos_less_eq_append_not_parallel) 
        then have "(p@?pi@?rγ, q@?qj@?rδ) ∈ overlaps_pos (labeled_source A) (labeled_source B)" proof(cases)
          case 1
          then show ?thesis using obtain_overlap[OF oc1 oc2 oc3 oc4 oc5 oc6] unfolding * ** using A B
            by (metis (no_types, lifting) append.assoc less_eq_pos_simps(2) p)
        next
          case 2
          have "(q@?qj@?rδ, p@?pi@?rγ) ∈ overlaps_pos (labeled_source B) (labeled_source A)"  
            using obtain_overlap[OF oc2 oc1 oc4 oc3 oc6 oc5] using r2 2 A B unfolding * **
            by (metis (no_types, lifting) append.assoc less_eq_pos_simps(2) prefix_order.less_le_not_le p)
          then show ?thesis 
            using overlaps_pos_symmetric by blast 
        qed
        then show ?thesis 
          using maximal pi_not_empty by (smt (verit) append.assoc append_is_Nil_conv fst_conv less_eq_overlap_def less_eq_pos_simps(1) p self_append_conv snd_conv)
      qed
    qed
  qed 
qed

lemma measure_dec: "measure_ov A' B' < measure_ov A B"
proof-
  {fix r assume "r ∈ possL A' ∩ possL B'"
    then have r1:"r ∈ possL A'" and r2:"r ∈ possL B'" by blast+
    then have r_not_below:"¬ p ≤⇩p r"
      using measure_helper by blast 
    with r1 single_Δ1.label_ctxt[OF A single_Δ1.pq single_Δ1.p single_Δ1.q] have rA:"r ∈ possL A"
      unfolding single_Δ1.residual option.sel by force 
    have rB:"r ∈ possL B" proof(cases "q ≤⇩p r")
      case True
      from True obtain r' where r':"r = q@r'"
        using less_eq_pos_remove_prefix by metis 
      with r2 single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] have "r' ∈ possL (D' ⋅ ρ)"
        unfolding r' by force 
      then have "r' ∈ labelposs (labeled_source D' ⋅ (labeled_source ∘ ρ))"
        by (metis d'_well labeled_source_apply_subst)
      then consider "r' ∈ labelposs (labeled_source D')" | 
         "∃ r1 r2 x. r' = r1@r2 ∧ r1 ∈ poss (labeled_source D') ∧ (labeled_source D')|_r1 = Var x ∧ 
                     r2 ∈ labelposs ((labeled_source ∘ ρ) x)"
        using labelposs_subst by blast
      then show ?thesis proof(cases)
        case 1
        then have r'_fun:"r' ∈ fun_poss ((ctxt_of_pos_term q' l)⟨rename_y (rhs α) ⋅ τ⟩)"
          using labelposs_subs_fun_poss_source src_d' by fastforce 
        with r_not_below have "r' ∈ fun_poss l"
          unfolding r' p using replace_at_fun_poss_not_below  q'_poss fun_poss_imp_poss by (metis less_eq_pos_simps(2) poss_map_vars_term) 
        then have "r' ∈ fun_poss (lhs β)"
          by (simp add: fun_poss_map_vars_term)
        then have "r' ∈ labelposs (labeled_lhs β)"
          by (simp add: label_poss_labeled_lhs) 
        then have "r' ∈ possL (Prule β Bs)" 
          unfolding labeled_source.simps set_labelposs_subst by simp
        then have "r ∈ possL B"                              
          using single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] r' single_Δ2.a
          by (metis (mono_tags, lifting) Un_iff mem_Collect_eq) 
        with rA show ?thesis by simp
      next
        case 2
        then obtain r1 r2 x where r12:"r' = r1@r2" and r1_pos:"r1 ∈ poss (source D')" and x:"source D' |_ r1 = Var x"
          and r2_lab:"r2 ∈ labelposs ((labeled_source ∘ ρ) x)" 
          using poss_term_lab_to_term labeled_source_to_term var_term_lab_to_term by metis
        from r_not_below consider "r <⇩p p" | "r ⊥ p"
          using parallel_pos by fastforce 
        then show ?thesis proof(cases)
          case 1
          then have le:"r1 <⇩p q'"
            unfolding p r' r12 using less_eq_pos_simps(1) less_pos_simps(2) prefix_order.dual_order.strict_trans2 by blast 
          moreover have "q' ∈ poss (source D')"
            by (simp add: fun_poss_imp_poss q'_poss replace_at_below_poss src_d') 
          ultimately have False 
            using x by (metis less_pos_def' r1_pos var_pos_maximal) 
          then show ?thesis by simp
        next
          case 2
          from r_not_below have r1_not_below:"¬ q' ≤⇩p r1"
            unfolding p r' r12 using less_eq_pos_simps(1) less_eq_pos_simps(2) prefix_order.order_trans by blast
          with r1_pos have r1_pos':"r1 ∈ poss l" 
            unfolding src_d' using fun_poss_imp_poss poss_map_vars_term q'_poss 
            by (metis prefix_order.less_le parallel_poss_replace_at pos_cases replace_at_below_poss replace_at_ident) 
          then have x':"l|_r1 = Var x" 
            using x r1_not_below unfolding src_d'
            by (metis fun_poss_imp_poss prefix_def prefix_order.dual_order.eq_iff parallel_pos parallel_replace_at_subt_at poss_map_vars_term q'_poss replace_at_below_poss var_pos_maximal) 
          with r1_pos' obtain j where j:"j < length (var_poss_list l)" "var_poss_list l ! j = r1"
            by (metis in_set_conv_nth var_poss_iff var_poss_list_sound)
          with linear_l x' have "vars_distinct l ! j = x"
            by (metis length_var_poss_list linear_term_var_vars_term_list term.inject(1) vars_term_list_var_poss_list) 
          then have "ρ x = Bs!j" 
            using var_l_rho j(1) by (metis (no_types, lifting) length_var_poss_list linear_l linear_term_var_vars_term_list) 
          with r2_lab have r2_pos:"r2 ∈ possL (Bs!j)"
            by auto  
          from j have j1:"j < length (vars_term_list (labeled_lhs β))"
            by (metis length_map length_var_poss_list vars_map_vars_term vars_term_list_labeled_lhs) 
          from j have j2:"var_poss_list (labeled_lhs β) ! j = r1"
            by (metis var_poss_list_labeled_lhs var_poss_list_map_vars_term) 
          moreover have "(⟨map labeled_source Bs⟩⇩β) (vars_term_list (labeled_lhs β)!j) = labeled_source (Bs!j)"
          using j1
          by (smt (verit, best) apply_lhs_subst_var_rule fun_mk_subst labeled_source.simps(1) linear_term_var_vars_term_list nth_map o_apply single_Δ2.length_as single_Δ2.lin_lhs vars_term_list_labeled_lhs) 
          ultimately have "r1@r2 ∈ possL (Prule β Bs)" 
            unfolding labeled_source.simps using j1 j2 r2_pos set_labelposs_subst[of "labeled_lhs β" "⟨map labeled_source Bs⟩⇩β"]
            by (smt (verit, del_insts) UN_iff UnCI lessThan_iff mem_Collect_eq)
          then show ?thesis using single_Δ2.a unfolding r' r12
            using single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] by (metis (mono_tags, lifting) UnCI mem_Collect_eq)
        qed
      qed
    next
      case False
      then show ?thesis 
        using r2 single_Δ2.label_ctxt[OF B single_Δ2.pq single_Δ2.p single_Δ2.q] by force 
    qed
    from rA rB have "r ∈ possL A ∩ possL B" by simp
  }
  moreover from pq have "p ∈ possL A ∩ possL B"
    using co_init get_label_imp_labelposs le p_q_pos(1) s_def by force
  moreover have "p ∉ possL A' ∩ possL B'" 
    using measure_helper parallel_pos by auto
  ultimately show ?thesis 
    using psubset_card_mono finite_possL by (metis finite_Int psubsetI subsetI) 
qed

lemma target_beta_Bs:
  shows "target (Prule β Bs) = target (to_pterm (rename_x (rhs β) ⋅ τ) ⋅ ρ)" 
proof-
  {fix y assume "y ∈ vars_term (rhs β)"
    then have y:"y ∈ vars_term (lhs β)"
      using single_Δ2.rule_in_TRS wf_trs_S unfolding wf_trs_def var_rhs_subset_lhs_def by blast
    then obtain j where j:"j < length (vars_term_list (lhs β))" "(vars_term_list (lhs β))!j = y"
      by (metis in_set_conv_nth set_vars_term_list) 
    let ?y="x_var y"
    from j have "vars_term_list l ! j = ?y"
      by (metis nth_map vars_map_vars_term) 
    with j(1) have "to_pterm (τ ?y) ⋅ ρ = Bs!j" 
      using apply_tau_rho  by (smt (verit, best) length_map vars_map_vars_term)
    moreover from j have "(⟨Bs⟩⇩β) y = Bs!j"
      by (metis (no_types, lifting) lhs_subst_var_i linear_term_var_vars_term_list single_Δ2.length_as single_Δ2.lin_lhs) 
    ultimately have "((to_pterm ∘ (τ ∘ x_var)) ∘⇩s ρ) y = (⟨Bs⟩⇩β) y"
      by (simp add: subst_compose_def)  
  }note args_beta=this
  have "target (to_pterm (rename_x (rhs β) ⋅ τ) ⋅ ρ) = (rhs β) ⋅ (target ∘ ((to_pterm ∘ (τ ∘ x_var)) ∘⇩s ρ))" 
    using var_rhs_subset_lhs.target_apply_subst wf_trs_S 
    unfolding apply_subst_map_vars_term to_pterm_subst subst_subst wf_trs_def
    by (metis (no_types, lifting) target_to_pterm to_pterm_wf_pterm) 
  also have "... = target (Prule β Bs)" 
    unfolding target.simps using args_beta by (smt (verit) fun_mk_subst o_apply target.simps(1) term_subst_eq)
  finally show ?thesis by simp
qed

lemma rewrite_target_B':
  assumes "(rename_x (rhs β) ⋅ τ, target D') ∈ (rstep R)⇧*"
  shows "(target B, target B') ∈ (rstep R)⇧*"
proof-
  have "target B = target (replace_at B q⇩β ((to_pterm (rename_x (rhs β) ⋅ τ) ⋅ ρ)))"
    using target_beta_Bs by (metis context_target single_Δ2.a)
  moreover have "target B' = target (replace_at B q⇩β ((to_pterm (target D') ⋅ ρ)))"
    using context_target var_rhs_subset_lhs.tgt_subst_simp wf_trs_S d'_well unfolding wf_trs_def by metis
  ultimately show ?thesis 
    using assms rewrite_tgt by metis
qed

lemma target_B':
  assumes "target D' = rename_x (rhs β) ⋅ τ"
  shows "target B' = target B"
proof-
  have "target (D'⋅ρ) = target (to_pterm (rename_x (rhs β) ⋅ τ) ⋅ ρ)" 
    using var_rhs_subset_lhs.tgt_subst_simp wf_trs_S d'_well assms unfolding wf_trs_def by metis
  then show ?thesis using target_beta_Bs by (metis context_target single_Δ2.a)
qed

end

lemma exists_A'_B'_w:
  assumes mstep:"((ctxt_of_pos_term q' l)⟨rename_y (rhs α) ⋅ τ⟩, v'') ∈ mstep S"  
      and rstep:"(rename_x (rhs β) ⋅ τ, v'') ∈ (rstep R)⇧*"
    shows "∃A' B'. A' ∈ wf_pterm R ∧ B' ∈ wf_pterm S ∧ 
  source A' = source B' ∧ target A' = target A ∧ (target B, target B') ∈ (rstep R)⇧* ∧ measure_ov A' B' < measure_ov A B ∧ source A' = target Δ1"
proof-
  from mstep obtain D' where D':"D' ∈ wf_pterm S ∧ source D' = (ctxt_of_pos_term q' l)⟨rename_y (rhs α) ⋅ τ⟩ ∧ target D' = v''"
    using var_rhs_subset_lhs.mstep_to_pterm wf_trs_S unfolding wf_trs_def by blast 
  let ?v'="replace_at s p (v'' ⋅ σ)"
  from D' obtain B'' w where "B'' ∈ wf_pterm S" and "measure_ov A' B'' < measure_ov A B" and "source B'' = source A'"
    and "target B'' = w" and "(target B, w) ∈ (rstep R)⇧*" 
    using rewrite_target_B' rstep by (metis B'_well measure_dec source_B')
  moreover have "source A' = target Δ1"
    using A residual_src_tgt single_Δ1.delta_trs_wf_pterm single_Δ1.residual by fastforce 
  ultimately show ?thesis
    by (metis single_Δ1.residual_well single_Δ1.target_residual) 
qed

lemma exists_A'_B':
  assumes "(replace_at l q' (rename_y (rhs α) ⋅ τ), rename_x (rhs β) ⋅ τ) ∈ mstep S"
  shows "∃A' B'. A' ∈ wf_pterm R ∧ B' ∈ wf_pterm S ∧ 
  source A' = source B' ∧ target A' = target A ∧ target B' = target B ∧ measure_ov A' B' < measure_ov A B ∧ source A' = target Δ1"
proof-
  from assms obtain D' where "D' ∈ wf_pterm S ∧ 
    source D' = replace_at l q' (rename_y (rhs α) ⋅ τ) ∧ 
    target D' = rename_x (rhs β) ⋅ τ"
    using var_rhs_subset_lhs.mstep_to_pterm wf_trs_S unfolding wf_trs_def by blast 
  then obtain B'' where "B'' ∈ wf_pterm S" and "measure_ov A' B'' < measure_ov A B" and "source B'' = source A'"
    and "target B'' = target B" using measure_dec source_B' target_B' B'_well by meson
  moreover have "source A' = target Δ1"
    using A residual_src_tgt single_Δ1.delta_trs_wf_pterm single_Δ1.residual by fastforce 
  ultimately show ?thesis
    by (metis single_Δ1.residual_well single_Δ1.target_residual) 
qed

end

section‹Main Proof›
lemma mstep_closed_strongly_commute:
assumes closed_1:"⋀s t b. (b, s, t) ∈ critical_pairs ren R2 R1 ⟹ ∃v. (s, v) ∈ mstep R2 ∧ (t, v) ∈ (rstep R1)⇧*"
    and closed_2:"⋀s t. (False, s, t) ∈ critical_pairs ren R1 R2 ⟹ (s, t) ∈ mstep R1"
    and R1:"left_lin_wf_trs R1" and R2:"left_lin_wf_trs R2"
  shows "strongly_commute (mstep R1) (mstep R2)"
proof (rule strongly_commuteI)
  fix s t u assume "(s, t) ∈ mstep R1" and "(s, u) ∈ mstep R2"
  from R1 ‹(s,t) ∈ mstep R1› obtain A where A:"A ∈ wf_pterm R1 ∧ source A = s" and t_a:"target A = t"
    using var_rhs_subset_lhs.mstep_to_pterm unfolding left_lin_wf_trs_def wf_trs_def by blast 
  from R2 ‹(s,u) ∈ mstep R2› obtain B where B:"B ∈ wf_pterm R2 ∧ source B = s" and t_b:"target B = u"
    using var_rhs_subset_lhs.mstep_to_pterm unfolding left_lin_wf_trs_def wf_trs_def by blast 
  from A B t_a t_b have "∃v. (t, v) ∈ mstep R2 ∧ (u, v) ∈ (rstep R1)⇧*"
  proof(induct "measure_ov A B" arbitrary: A B s u rule:less_induct)
    case less
    show ?case proof(cases "measure_ov A B")
      case 0
      from 0 less.prems have "A re B ≠ None"
        using measure_zero_imp_orthogonal R1 R2 orth_imp_residual_defined
        by (metis wf_trs_def case_prodD left_lin_no_var_lhs_def left_lin_wf_trs_def no_var_lhs.no_var_lhs) 
      with less.prems obtain D where d:"A re B = Some D ∧ target B = source D ∧ D ∈ wf_pterm R1"
        by (metis not_Some_eq residual_src_tgt residual_well_defined) 
      from 0 less.prems have "B re A ≠ None"
        using measure_zero_imp_orthogonal R1 R2 orth_imp_residual_defined
        by (metis Int_commute Proof_Terms.wf_trs_def case_prodD left_lin_no_var_lhs_def left_lin_wf_trs_def no_var_lhs.no_var_lhs)
      with less.prems obtain C where c:"B re A = Some C ∧ target A = source C ∧ C ∈ wf_pterm R2"
        by (metis not_Some_eq residual_src_tgt residual_well_defined) 
      from c d less.prems have "target C = target D" 
        using residual_tgt_tgt by blast 
      with c d less.prems(3,4) show ?thesis 
        using pterm_to_mstep by (metis mstep_imp_rsteps)
    next
      case (Suc n)
      with less(2,3) have "overlaps_pos (labeled_source A) (labeled_source B) ≠ {}"
        using empty_overlaps_imp_measure_zero [of A R1 B R2] by force
      then have "∃m∈overlaps_pos (labeled_source A) (labeled_source B).
         ∀b∈overlaps_pos (labeled_source A) (labeled_source B). m ≤⇩o b ⟶ m = b"
        by (intro order_overlaps.finite_has_maximal, auto simp: finite_fun_poss)
      then obtain p q where pq:"(p, q) ∈ overlaps_pos (labeled_source A) (labeled_source B)" and 
          innermost:"(∀b∈overlaps_pos (labeled_source A) (labeled_source B). (p,q) ≤⇩o b ⟶ (p,q) = b)"
        by (metis (no_types, lifting) prod.collapse)
      then have "p ∈ poss (labeled_source A)"
        by (simp add: fun_poss_imp_poss) 
      moreover obtain α where alpha:"get_label (labeled_source A |_ p) = Some (α, 0)" 
        using pq by auto 
      ultimately obtain p⇩α where p⇩α:"p⇩α ∈ poss A" "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p⇩α A)"
        "A|_p⇩α = Prule α (map (λi. A|_(p⇩α@[i])) [0..<length (var_rule α)])"
        using left_lin.poss_labeled_source R1 less.prems(1) unfolding wf_trs_def left_lin_wf_trs_def by fastforce
      from pq have "q ∈ poss (labeled_source B)"
        by (simp add: fun_poss_imp_poss) 
      moreover obtain β where beta:"get_label (labeled_source B |_ q) = Some (β, 0)" 
        using pq by auto 
      ultimately obtain q⇩β where q⇩β:"q⇩β ∈ poss B" "ctxt_of_pos_term q (source B) = source_ctxt (ctxt_of_pos_term q⇩β B)"
        "B|_q⇩β = Prule β (map (λi. B|_(q⇩β@[i])) [0..<length (var_rule β)])"
        using left_lin.poss_labeled_source R2 less.prems(2) unfolding wf_trs_def left_lin_wf_trs_def by fastforce
      consider "q ≤⇩p p" | "p <⇩p q"
        using pq strict_prefix_def by fastforce
      then show ?thesis proof(cases)
        case 1
        then obtain q' where q':"Some q' = remove_prefix q p"
          by (metis less_eq_pos_remove_prefix)
        then have io:"innermost_overlap R1 R2 A B p q q' p⇩α q⇩β α β" 
          unfolding innermost_overlap_def using R1 R2 less.prems pq innermost q' alpha beta p⇩α q⇩β by auto
        obtain A' B' where "A' ∈ wf_pterm R1"  "B' ∈ wf_pterm R2"
            "source A' = source B'" "target A' = target A" and tgt:"(target B, target B') ∈ (rstep R1)⇧*" and m:" measure_ov A' B' < measure_ov A B"
          using innermost_overlap.exists_A'_B'_w[OF io] innermost_overlap.critical_pair[OF io] closed_1 by meson 
        with less.hyps[OF m] obtain v where "(t, v) ∈ mstep R2 ∧ (target B', v) ∈ (rstep R1)⇧*"
            using less.prems(3) by presburger
        with tgt show ?thesis
          by (metis less.prems(4) mstep_rsteps_subset rstep_mstep_subset rtrancl_subset rtrancl_trans) 
      next
        case 2
        then have p_not_q:"p ≠ q" by simp
        from 2 obtain q' where q':"Some q' = remove_prefix p q"
          unfolding less_pos_def' by auto
        have qp:"(q, p) ∈ overlaps_pos (labeled_source B) (labeled_source A)"
          using overlaps_pos_symmetric[OF pq].
        have innermost':"(∀b∈overlaps_pos (labeled_source B) (labeled_source A). (q,p) ≤⇩o b ⟶ (q,p) = b)" proof-
          {fix b1 b2 assume assm:"(b1, b2) ∈ overlaps_pos (labeled_source B) (labeled_source A)" 
                        and le:"(q,p) ≤⇩o (b1, b2)" and ne:"(q,p) ≠ (b1, b2)"
            then have *:"(b2, b1) ∈ overlaps_pos (labeled_source A) (labeled_source B)"
              using overlaps_pos_symmetric by blast 
            from le have "(p,q) ≤⇩o (b2, b1)" unfolding less_eq_overlap_def less_overlap_def fst_conv snd_conv
              by (smt (z3) "2" assm case_prodD strict_prefix_def ne prefix_order.leD prefix_order.max_def prefix_order.min_def)
            with innermost * ne have False by fastforce 
          }then show ?thesis by fast 
        qed
        have io:"innermost_overlap R2 R1 B A q p q' q⇩β p⇩α β α" 
          unfolding innermost_overlap_def using R1 R2 less.prems qp innermost' q' beta alpha p⇩α q⇩β by auto
        obtain A' B' where "A' ∈ wf_pterm R1" and "B' ∈ wf_pterm R2"
          and "source A' = source B'" and "target A' = target A" and "target B' = target B" and m:"measure_ov A' B' < measure_ov A B"
          using innermost_overlap.exists_A'_B'[OF io] p_not_q innermost_overlap.critical_pair[OF io] closed_2 by (smt (verit) measure_ov_symm)
        with less.prems less.hyps[OF m] show ?thesis by simp
      qed
    qed 
  qed
  then show "∃v. (t, v) ∈ (mstep R2)⇧= ∧ (u, v) ∈ (mstep R1)⇧*"
    by (metis Un_iff mstep_rsteps_subset rstep_mstep_subset rtrancl_subset) 
qed

corollary mstep_closed_imp_commute:
 assumes closed_1:"⋀s t b. (b, s, t) ∈ critical_pairs ren R2 R1 ⟹ ∃v. (s, v) ∈ mstep R2 ∧ (t, v) ∈ (rstep R1)⇧*"
    and closed_2:"⋀s t. (False, s, t) ∈ critical_pairs ren R1 R2 ⟹ (s, t) ∈ mstep R1"
    and R1:"left_lin_wf_trs R1" and R2:"left_lin_wf_trs R2"
  shows "commute (rstep R1) (rstep R2)"
proof
  fix x y⇩1 y⇩2
  assume "(x, y⇩1) ∈ (rstep R1)⇧*" and "(x, y⇩2) ∈ (rstep R2)⇧*"
  then have "(x, y⇩1) ∈ (mstep R1)⇧*" and "(x, y⇩2) ∈ (mstep R2)⇧*"
    using rtrancl_mono[OF rstep_mstep_subset] by auto
  from commuteE[OF strongly_commute_imp_commute[OF mstep_closed_strongly_commute[OF assms]] this]
  obtain z where "(y⇩1, z) ∈ (mstep R2)⇧* ∧ (y⇩2, z) ∈ (mstep R1)⇧*"  by fast
  then show "∃z. (y⇩1, z) ∈ (rstep R2)⇧* ∧ (y⇩2, z) ∈ (rstep R1)⇧*"
    using rtrancl_mono[OF mstep_rsteps_subset] rtrancl_idemp by auto
qed

corollary mstep_closed_imp_CR:
  assumes "⋀s t. (False, s, t) ∈ critical_pairs ren R R ⟹ (s, t) ∈ mstep R"
    and "⋀s t. (True, s, t) ∈ critical_pairs ren R R ⟹ ∃v. (s, v) ∈ mstep R ∧ (t, v) ∈ (rstep R)⇧*"
    and "left_lin_wf_trs R"
  shows "CR (rstep R)"
proof-
  from assms(1,2) have "⋀b s t. (b, s, t) ∈ critical_pairs ren R R ⟹ ∃v. (s, v) ∈ mstep R ∧ (t, v) ∈ (rstep R)⇧*"
    by (metis rtrancl.rtrancl_refl) 
  with assms(1,3-) show ?thesis using mstep_closed_imp_commute[of ren R R]
    using CR_iff_self_commute[of "rstep R"] by blast
qed

section‹Commutation via Relative Termination›
(*Extending the proofs in "Commutation via Relative Termination"@IWC2013 to 'almost' version.*)

(*Key Lemma (generalizing Lemma 4.1. of IWC2013)*)
lemma critical_peak_step_cases:
  assumes t:"(s,t) ∈ mstep R" and u:"(s,u) ∈ mstep S"
    and R:"left_lin_wf_trs R" and S:"left_lin_wf_trs S"
  shows "(∃v. (t,v) ∈ mstep S ∧ (u,v) ∈ (rstep R)⇧*) ∨ 
         (∃s' t' u' w .(s,s') ∈ (rstep (R ∪ S))⇧* ∧ (s', t') ∈ rstep (CPS_R ren R S) ∧ (t', t) ∈ mstep R 
                           ∧ (u, w) ∈ (rstep R)⇧* ∧ (s', u') ∈ rstep (CPS_S ren R S) ∧ (u', w) ∈ mstep S)"
proof-
  from t obtain A where A:"A ∈ wf_pterm R" "source A = s" "target A = t"
    using var_rhs_subset_lhs.mstep_to_pterm R unfolding wf_trs_def left_lin_wf_trs_def by blast
  from u  obtain B where B:"B ∈ wf_pterm S" "source B = s" "target B = u"
    using var_rhs_subset_lhs.mstep_to_pterm S unfolding wf_trs_def left_lin_wf_trs_def by blast
  from A B show ?thesis
  proof(induct "measure_ov A B" arbitrary: A B s u rule:less_induct)
    case less
    show ?case proof(cases "measure_ov A B")
      case 0
      from 0 less.prems have "A re B ≠ None"
        using measure_zero_imp_orthogonal orth_imp_residual_defined R S unfolding left_lin_wf_trs_def
        by (metis case_prodD left_lin_no_var_lhs.intro no_var_lhs.no_var_lhs wf_trs.axioms(1)) 
      with less.prems obtain D where d:"A re B = Some D ∧ target B = source D ∧ D ∈ wf_pterm R"
        using residual_well_defined[OF less.prems(1,4)] not_Some_eq residual_src_tgt by metis
      from 0 less.prems have "B re A ≠ None"
        using measure_zero_imp_orthogonal orth_imp_residual_defined R S unfolding left_lin_wf_trs_def
        by (metis Int_commute case_prodD left_lin_no_var_lhs.intro no_var_lhs.no_var_lhs wf_trs.axioms(1)) 
      with less.prems obtain C where c:"B re A = Some C ∧ target A = source C ∧ C ∈ wf_pterm S"
        using residual_well_defined[OF less.prems(4,1)] not_Some_eq residual_src_tgt by metis
      from c d less.prems have "target C = target D" 
        using residual_tgt_tgt by blast 
      with c d less.prems(3,6) show ?thesis
        by (metis mstep_imp_rsteps pterm_to_mstep) 
    next
      case (Suc n)
      with less(2,5) have "overlaps_pos (labeled_source A) (labeled_source B) ≠ {}"
        using empty_overlaps_imp_measure_zero[of A _ B] by fastforce 
      then have "∃m∈overlaps_pos (labeled_source A) (labeled_source B).
         ∀b∈overlaps_pos (labeled_source A) (labeled_source B). m ≤⇩o b ⟶ m = b"
        by (intro order_overlaps.finite_has_maximal, auto simp: finite_fun_poss)
      then obtain p q where pq:"(p, q) ∈ overlaps_pos (labeled_source A) (labeled_source B)" and 
          innermost:"(∀b∈overlaps_pos (labeled_source A) (labeled_source B). (p,q) ≤⇩o b ⟶ (p,q) = b)"
        by (metis (no_types, lifting) prod.collapse)
      then have p:"p ∈ poss (labeled_source A)"
        by (simp add: fun_poss_imp_poss)  
      moreover obtain α where alpha:"get_label (labeled_source A |_ p) = Some (α, 0)" 
        using pq by auto 
      ultimately obtain p⇩α where p⇩α:"p⇩α ∈ poss A" "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p⇩α A)"
        "A|_p⇩α = Prule α (map (λi. A|_(p⇩α@[i])) [0..<length (var_rule α)])"
        using left_lin.poss_labeled_source less.prems(1) R unfolding wf_trs_def left_lin_wf_trs_def by fastforce
      from alpha less.prems(1) have α:"to_rule α ∈ R"
        using labeled_wf_pterm_rule_in_TRS p by blast  
      from pq have q:"q ∈ poss (labeled_source B)"
        by (simp add: fun_poss_imp_poss) 
      moreover obtain β where beta:"get_label (labeled_source B |_ q) = Some (β, 0)" 
        using pq by auto 
      ultimately obtain q⇩β where q⇩β:"q⇩β ∈ poss B" "ctxt_of_pos_term q (source B) = source_ctxt (ctxt_of_pos_term q⇩β B)"
        "B|_q⇩β = Prule β (map (λi. B|_(q⇩β@[i])) [0..<length (var_rule β)])"
        using left_lin.poss_labeled_source less.prems(4) S unfolding wf_trs_def left_lin_wf_trs_def by fastforce
      from beta less.prems(4) have β:"to_rule β ∈ S"
        using labeled_wf_pterm_rule_in_TRS q by blast  
      consider "q ≤⇩p p" | "p <⇩p q"
        using pq strict_prefix_def by fastforce
      then show ?thesis proof(cases)
        case 1
        then obtain q' where q':"Some q' = remove_prefix q p"
          by (metis less_eq_pos_remove_prefix)
        then have io:"innermost_overlap R S A B p q q' p⇩α q⇩β α β" 
          unfolding innermost_overlap_def using R S less.prems pq innermost q' alpha beta p⇩α q⇩β by auto
        let ?a="(to_pterm_ctxt (ctxt_of_pos_term q' (rename_x ren (lhs β))))⟨Prule α (map (to_pterm ∘ innermost_overlap.τ ren q' α β ∘ rename_2 ren) (var_rule α))⟩"
        let ?b="Prule β (map (to_pterm ∘ innermost_overlap.τ ren q' α β ∘ rename_1 ren) (var_rule β))"
        let ?Δ1="ll_single_redex s p α"
        let ?Δ2="ll_single_redex s q β"
        have *:"vars_term (rhs α) ⊆ vars_term (lhs α)" 
          using α R var_rhs_subset_lhs.varcond unfolding wf_trs_def left_lin_wf_trs_def by fastforce 
        have tgt_a:"target ?a = (ctxt_of_pos_term q' (rename_x ren (lhs β)))⟨rename_y ren (rhs α) ⋅ innermost_overlap.τ ren q' α β⟩"
          unfolding target_to_pterm_ctxt target.simps map_map lhs_subst_var_rule[OF *]
          by (smt (verit) apply_subst_map_vars_term comp_assoc target_empty_apply_subst target_to_pterm to_pterm_empty to_pterm_subst) 
        have **:"vars_term (rhs β) ⊆ vars_term (lhs β)" 
          using β S var_rhs_subset_lhs.varcond unfolding wf_trs_def left_lin_wf_trs_def by fastforce 
        have tgt_b:"target ?b = rename_x ren (rhs β) ⋅ innermost_overlap.τ ren q' α β"
          unfolding target.simps map_map lhs_subst_var_rule[OF **]
          by (smt (verit) apply_subst_map_vars_term comp_assoc target_empty_apply_subst target_to_pterm to_pterm_empty to_pterm_subst)
        from innermost_overlap.critical_peak[OF io] have cp:"(?a, ?b) ∈ pterm_cpeaks ren R S".
        show ?thesis proof(cases "is_R_S_closed R S (?a, ?b)")
          case True
          then obtain v'' where v'':"(target ?a,v'') ∈ mstep S" "(target ?b,v'') ∈ (rstep R)⇧*" 
            unfolding is_R_S_closed.simps by blast 
          obtain A' B' where A':"A' ∈ wf_pterm R" and B':"B' ∈ wf_pterm S" and src_A':"source A' = target ?Δ1"
            and "source A' = source B'" and "target A' = target A" and tgt:"(target B, target B') ∈ (rstep R)⇧*" and m:"measure_ov A' B' < measure_ov A B"
            using innermost_overlap.exists_A'_B'_w[OF io v''[unfolded tgt_a tgt_b]] by (metis innermost_overlap.s_def io less.prems(2))
          with less.hyps[OF m A'] consider "∃v. (t, v) ∈ mstep S ∧ (target B', v) ∈ (rstep R)⇧*" |
            "(∃s' t' u' w .(source A',s') ∈ (rstep (R ∪ S))⇧* ∧ (s', t') ∈ rstep (CPS_R ren R S) ∧ (t', t) ∈ mstep R 
            ∧ (target B', w) ∈ (rstep R)⇧* ∧ (s', u') ∈ rstep (CPS_S ren R S) ∧ (u', w) ∈ mstep S)"
            using less.prems(3) less.prems(6) by fastforce
          then show ?thesis proof(cases)
            case 1
            then show ?thesis using tgt less(7) by auto
          next
            case 2
            then obtain s' t' u' w where steps:"(source A', s') ∈ (rstep (R ∪ S))⇧*" "(s', t') ∈ rstep (CPS_R ren R S)" "(t', t) ∈ mstep R" 
                "(target B', w) ∈ (rstep R)⇧*" "(s', u') ∈ rstep (CPS_S ren R S)" "(u', w) ∈ mstep S"
              by blast
            have "(s, source A') ∈ rstep R"
              by (metis α innermost_overlap.s_def innermost_overlap.source_d1 io labeled_source_to_term less.prems(2) p poss_term_lab_to_term single_redex_rstep src_A')
            with steps(1) have s':"(s, s') ∈ (rstep (R ∪ S))⇧*"
              by (metis UnCI converse_rtrancl_into_rtrancl rstep_union) 
            from steps(4) tgt less.prems(6) have "(u, w) ∈ (rstep R)⇧*"
              by auto 
            with steps show ?thesis
              using s' by blast  
          qed
        next
          case False
          then have "(source ?a, target ?a) ∈ CPS_R ren R S" 
            unfolding CPS_R_def using cp by blast 
          with innermost_overlap.Δ1_is_rstep[OF io] 
          have cps_R:"(source ?Δ1, target ?Δ1) ∈ rstep (CPS_R ren R S)"
            by (metis innermost_overlap.s_def io less.prems(2)) 
          from False have "(source ?b, target ?b) ∈ CPS_S ren R S" 
            unfolding CPS_S_def using cp by blast 
          with innermost_overlap.Δ2_is_rstep[OF io] 
          have cps_S:"(source ?Δ2, target ?Δ2) ∈ rstep (CPS_S ren R S)"
            by (metis innermost_overlap.s_def io less.prems(2))
          from p⇩α have d1:"single_redex R A ?Δ1 p p⇩α α"
            using single_redex.intro R single_redex_axioms.intro[OF less.prems(1)]
            by (metis innermost_overlap.ll_no_var_lhs_R io labeled_source_to_term less.prems(2) p poss_term_lab_to_term)
          then have A':"the (A re ?Δ1) ∈ wf_pterm R" 
            by (simp add: single_redex.residual_well)
          from q⇩β have d2:"single_redex S B ?Δ2 q q⇩β β"
            using single_redex.intro S single_redex_axioms.intro[OF less.prems(4)]
            by (metis innermost_overlap.ll_no_var_lhs_S io labeled_source_to_term less.prems(5) poss_term_lab_to_term q) 
          then have B':"the (B re ?Δ2) ∈ wf_pterm S"
            by (simp add: single_redex.residual_well) 
          have "(∃t' u'. (s, t') ∈ rstep (CPS_R ren R S) ∧ (t', t) ∈ mstep R 
                       ∧ (s, u') ∈ rstep (CPS_S ren R S) ∧ (u', u) ∈ mstep S)" 
            using cps_R cps_S pterm_to_mstep[OF A'] pterm_to_mstep[OF B'] less.prems
            by (smt (verit) d1 d2 innermost_overlap.s_def innermost_overlap.source_d1 innermost_overlap.source_d2 io option.sel residual_src_tgt single_redex.delta_trs_wf_pterm single_redex.residual single_redex.target_residual)
          then show ?thesis by blast
        qed
      next
        case 2
        then have p_not_q:"p ≠ q" by simp
        from 2 obtain q' where q':"Some q' = remove_prefix p q"
          unfolding less_pos_def' by auto
        have qp:"(q, p) ∈ overlaps_pos (labeled_source B) (labeled_source A)"
          using overlaps_pos_symmetric[OF pq].
        have innermost':"(∀b∈overlaps_pos (labeled_source B) (labeled_source A). (q,p) ≤⇩o b ⟶ (q,p) = b)" proof-
          {fix b1 b2 assume assm:"(b1, b2) ∈ overlaps_pos (labeled_source B) (labeled_source A)" 
                        and le:"(q,p) ≤⇩o (b1, b2)" and ne:"(q,p) ≠ (b1, b2)"
            then have *:"(b2, b1) ∈ overlaps_pos (labeled_source A) (labeled_source B)"
              using overlaps_pos_symmetric by blast 
            from le have "(p,q) ≤⇩o (b2, b1)" unfolding less_eq_overlap_def less_overlap_def fst_conv snd_conv
              by (smt (z3) "2" assm case_prodD strict_prefix_def ne prefix_order.leD prefix_order.max_def prefix_order.min_def)
            with innermost * ne have False by fastforce 
          }then show ?thesis by fast 
        qed
        have io:"innermost_overlap S R B A q p q' q⇩β p⇩α β α" 
          unfolding innermost_overlap_def using R S less.prems qp innermost' q' beta alpha p⇩α q⇩β by auto
        let ?τ="innermost_overlap.τ ren q' β α"
        let ?b="(to_pterm_ctxt (ctxt_of_pos_term q' (rename_x ren (lhs α))))⟨Prule β (map (to_pterm ∘ ?τ ∘ rename_2 ren) (var_rule β))⟩"
        let ?a="Prule α (map (to_pterm ∘ ?τ ∘ rename_1 ren) (var_rule α))"
        let ?Δ1="ll_single_redex s p α"
        let ?Δ2="ll_single_redex s q β"  
        have *:"vars_term (rhs α) ⊆ vars_term (lhs α)" 
          using α R var_rhs_subset_lhs.varcond unfolding left_lin_wf_trs_def wf_trs_def by fastforce 
        have **:"vars_term (rhs β) ⊆ vars_term (lhs β)" 
          using β S var_rhs_subset_lhs.varcond unfolding left_lin_wf_trs_def wf_trs_def by fastforce  
        from α obtain f ts where lhsa:"lhs α = Fun f ts"
          using no_var_lhs.no_var_lhs R unfolding left_lin_wf_trs_def wf_trs_def by fastforce 
         have "q' ≠ []"
           by (metis append.right_neutral p_not_q q' remove_prefix_Some) 
         moreover have "q' ∈ poss (lhs α)"
           using fun_poss_imp_poss innermost_overlap.q'_poss io by blast 
         ultimately obtain i q'' where iq:"q' = i#q''" and "i < length ts" and "q'' ∈ poss (ts!i)"
           using lhsa by auto
         then obtain ts' where b_fun:"?b = Pfun f ts'" 
           unfolding lhsa iq by force
        have tgt_a:"target ?b = (ctxt_of_pos_term q' (rename_x ren (lhs α)))⟨rename_y ren (rhs β) ⋅ ?τ⟩"
          unfolding target_to_pterm_ctxt target.simps map_map lhs_subst_var_rule[OF **]
          by (smt (verit) apply_subst_map_vars_term comp_assoc target_empty_apply_subst target_to_pterm to_pterm_empty to_pterm_subst)  
        have tgt_b:"target ?a = rename_x ren (rhs α) ⋅ ?τ"
          unfolding target.simps map_map lhs_subst_var_rule[OF *]
          by (smt (verit) apply_subst_map_vars_term comp_assoc target_empty_apply_subst target_to_pterm to_pterm_empty to_pterm_subst)
        from innermost_overlap.critical_peak[OF io] have cp:"(?b, ?a) ∈ pterm_cpeaks ren S R".
        show ?thesis proof(cases "is_R_S_closed R S (?a, ?b)")
          case True
          then have "(target ?b, target ?a) ∈ mstep R" unfolding b_fun is_R_S_closed.simps .
          then obtain A' B' where A':"A' ∈ wf_pterm R" and B':"B' ∈ wf_pterm S" and src_A':"source B' = target ?Δ2"
            and "source A' = source B'" and tgt:"target A' = target A" "target B' = target B" and m:"measure_ov A' B' < measure_ov A B"
            using innermost_overlap.exists_A'_B'[OF io] unfolding tgt_a tgt_b
            by (metis innermost_overlap.s_def io less.prems(5) measure_ov_symm) 
          with less.hyps[OF m A'] consider "∃v. (t, v) ∈ mstep S ∧ (target B', v) ∈ (rstep R)⇧*" |
            "(∃s' t' u' w .(source B',s') ∈ (rstep (R ∪ S))⇧* ∧ (s', t') ∈ rstep (CPS_R ren R S) ∧ (t', t) ∈ mstep R 
            ∧ (target B', w) ∈ (rstep R)⇧* ∧ (s', u') ∈ rstep (CPS_S ren R S) ∧ (u', w) ∈ mstep S)"
            using less.prems(3) less.prems(6) by fastforce
          then show ?thesis proof(cases)
            case 1
            then show ?thesis using tgt less(7) by auto
          next
            case 2
            then obtain s' t' u' w where steps:"(source B', s') ∈ (rstep (R ∪ S))⇧*" "(s', t') ∈ rstep (CPS_R ren R S)" "(t', t) ∈ mstep R" 
                "(target B', w) ∈ (rstep R)⇧*" "(s', u') ∈ rstep (CPS_S ren R S)" "(u', w) ∈ mstep S"
              by blast
            have "(s, source B') ∈ rstep S"
              by (metis β innermost_overlap.s_def innermost_overlap.source_d1 io labeled_source_to_term less.prems(5) poss_term_lab_to_term q single_redex_rstep src_A') 
            with steps(1) have s':"(s, s') ∈ (rstep (R ∪ S))⇧*"
              by (metis UnCI converse_rtrancl_into_rtrancl rstep_union) 
            from steps(4) tgt less.prems(6) have "(u, w) ∈ (rstep R)⇧*"
              by auto 
            with steps show ?thesis
              using s' by blast  
          qed
        next
          case False
          then have "(source ?a, target ?a) ∈ CPS_R ren R S" 
            unfolding CPS_R_def using cp by blast 
          with innermost_overlap.Δ2_is_rstep[OF io] 
          have cps_R:"(source ?Δ1, target ?Δ1) ∈ rstep (CPS_R ren R S)"
            by (metis innermost_overlap.s_def io less.prems(5)) 
          from False have "(source ?b, target ?b) ∈ CPS_S ren R S" 
            unfolding CPS_S_def using cp by blast 
          with innermost_overlap.Δ1_is_rstep[OF io] False
          have cps_S:"(source ?Δ2, target ?Δ2) ∈ rstep (CPS_S ren R S)"
            by (metis innermost_overlap.s_def io less.prems(5))
          from p⇩α have d1:"single_redex R A ?Δ1 p p⇩α α"
            using single_redex.intro R single_redex_axioms.intro[OF less.prems(1)]
            by (metis innermost_overlap.ll_no_var_lhs_S io labeled_source_to_term less.prems(2) p poss_term_lab_to_term)
          then have A':"the (A re ?Δ1) ∈ wf_pterm R" 
            by (simp add: single_redex.residual_well)
          from q⇩β have d2:"single_redex S B ?Δ2 q q⇩β β"
            using single_redex.intro S single_redex_axioms.intro[OF less.prems(4)] less.prems(5) q
            by (metis innermost_overlap.ll_no_var_lhs_R io labeled_source_to_term poss_term_lab_to_term) 
          then have B':"the (B re ?Δ2) ∈ wf_pterm S"
            by (simp add: single_redex.residual_well)
          have "(∃t' u'. (s, t') ∈ rstep (CPS_R ren R S) ∧ (t', t) ∈ mstep R 
                       ∧ (s, u') ∈ rstep (CPS_S ren R S) ∧ (u', u) ∈ mstep S)" 
            using cps_R cps_S pterm_to_mstep[OF A'] pterm_to_mstep[OF B'] less.prems
            by (smt (verit) d1 d2 innermost_overlap.s_def innermost_overlap.source_d1 innermost_overlap.source_d2 io option.sel residual_src_tgt single_redex.delta_trs_wf_pterm single_redex.residual single_redex.target_residual)
          then show ?thesis by blast
        qed
      qed
    qed 
  qed
qed

lemma CPS''_SN_rel_imp_comm:
  assumes SN_rel:"SN_rel (rstep (CPS_R ren R S) ∪ rstep (CPS_S ren R S)) (rstep (R ∪ S))"
  and lc:"locally_commute (rstep R) (rstep S)"
  and R_wf:"left_lin_wf_trs R" and S_wf:"left_lin_wf_trs S"
shows "commute (rstep R) (rstep S)"
proof-
  let ?R = "λ(n, s). {(t,u) |t u. (t,u) ∈ mstep R ∧ (s,t) ∈ (rstep (R ∪ S))⇧* ∧ n = 0}"
  let ?S = "λ(n, s). {(t,u) |t u. (t,u) ∈ mstep S ∧ (s,t) ∈ (rstep (R ∪ S))⇧* ∧ n = 1}"
 (*s > t if s rewrites to t using the rules of R and S and the rewrite sequence contains at least one CPS step*)
  let ?r' = "((relto (rstep (CPS_R ren R S) ∪ rstep (CPS_S ren R S)) (rstep (R ∪ S)))¯)⇧+" 
  let ?r = "lex_prod less_than ?r'"
  have R: "(⋃i. ?R i) = mstep R" and S: "(⋃i. ?S i) = mstep S" by auto
  have "commute (mstep R) (mstep S)" proof (induct rule:dd_commute[of ?r ?R ?S, unfolded R S])
    case 1
    from SN_rel show ?case
      using SN_iff_wf SN_rel_imp_SN_relto wf_trancl by blast
  next
    case 2
    then show ?case by simp
  next
    case (3 a b s t u)
    from 3(1) obtain s1 where s1_s:"(s1, s) ∈ (rstep (R ∪ S))⇧*" and a:"a = (0, s1)" 
      by blast 
    from 3(2) obtain s2 where s2_s:"(s2, s) ∈ (rstep (R ∪ S))⇧*" and b:"b = (1, s2)"
      by blast 
    (*apply Key Lemma*)
    from 3(1) have m1:"(s, t) ∈ mstep R"
      by force 
    from 3(2) have m2:"(s, u) ∈ mstep S"
      by force
    let ?conv="conversion'' ?R ?S (under ?r a ∪ under ?r b)"
    (*helper lemma for sequences of steps over R*)
    {fix x y assume ms:"(x,y) ∈ (mstep R)⇧*" and "(s2, x) ∈ (rstep (R ∪ S))⇧*"
      from rtrancl_imp_seq[OF ms] obtain f n where "f 0 = x" "f n = y" "(∀i<n. (f i, f (Suc i)) ∈ mstep R)" by blast
      then have "(y,x) ∈ ((⋃i ∈ (under ?r b). ?R i)¯)⇧*" proof(induct n arbitrary: y)
        case 0
        then show ?case by fastforce
      next
        case (Suc n)
        obtain y' where y':"f n = y'"
          by simp 
        from Suc(1)[OF Suc(2) y'] Suc(4) have IH:"(y', x) ∈ ((⋃i ∈ (under ?r b). ?R i)¯)⇧*"
          using less_Suc_eq by presburger
        have "(x, y') ∈ (mstep R)⇧*"
          using Suc.prems(1) Suc.prems(3) less_SucI rtrancl_fun_conv y' by metis
        then have "(x, y') ∈ (rstep (R ∪ S))⇧*"
          by (metis in_rtrancl_UnI mstep_rsteps_subset rstep_mstep_subset rstep_union rtrancl_subset)
        with y' Suc(3,4) have "(y', y) ∈ ?R (0,x)"
          by blast
        moreover have "(0, x) ∈ under ?r b" unfolding b under_def by simp
        ultimately have "(y', y) ∈ (⋃i ∈ (under ?r b). ?R i)"
          by blast 
        with IH show ?case
          by (meson converse_iff converse_rtrancl_into_rtrancl)
      qed
      then have "(y, x) ∈ ?conv"  
        by (metis (no_types, lifting) UN_Un in_rtrancl_UnI rtrancl_converseD rtrancl_converseI) 
    }note seq_steps_R=this
   (*analogous helper lemma for sequences of steps over S*)
    {fix x y assume ms:"(x,y) ∈ (mstep S)⇧*" and under:"(x, s2) ∈ ?r'"
      from rtrancl_imp_seq[OF ms] obtain f n where "f 0 = x" and "f n = y" and "(∀i<n. (f i, f (Suc i)) ∈ mstep S)"
          by blast        
        then have "(x, y) ∈ (⋃i ∈ (under ?r b). ?S i)⇧*" proof(induct n arbitrary: y) 
          case 0
          then show ?case
            by fastforce
        next
          case (Suc n)
          obtain y' where v':"f n = y'"
            by simp 
          from Suc(1)[OF Suc(2) v'] Suc(4) have IH:"(x, y') ∈ (⋃i ∈ (under ?r b). ?S i)⇧*"
            using less_Suc_eq by presburger
          have "(x, y') ∈ (mstep S)⇧*"
            by (metis (no_types, opaque_lifting) Suc.prems(1) Suc.prems(3) less_SucI rtrancl_fun_conv v')
          then have "(x, y') ∈ (rstep (R ∪ S))⇧*"
            by (metis in_rtrancl_UnI mstep_rsteps_subset rstep_mstep_subset rstep_union rtrancl_subset)
          with v' Suc(3,4) have "(y', y) ∈ ?S (1, x)"
            by blast
          moreover from under have "(1, x) ∈ under ?r b"
            unfolding b under_def by simp
          ultimately have "(y', y) ∈ (⋃i ∈ (under ?r b). ?S i)"
            by blast
          with IH show ?case
            by (meson rtrancl.rtrancl_into_rtrancl)
        qed
    }note seq_steps_S=this
    consider "∃v. (t, v) ∈ mstep S ∧ (u, v) ∈ (rstep R)⇧*" | 
        "∃s' t' u' w. (s, s') ∈ (rstep (R ∪ S))⇧* ∧ (s', t') ∈ rstep (CPS_R ren R S) ∧ (t', t) ∈ mstep R ∧ (u, w) ∈ (rstep R)⇧* ∧ (s', u') ∈ rstep (CPS_S ren R S) ∧ (u', w) ∈ mstep S"
      using critical_peak_step_cases[OF m1 m2] R_wf S_wf by blast
    then show ?case proof(cases)
      case 1 (*corresponds to Figure 1(a)*)
      then obtain v where m3:"(t, v) ∈ mstep S" and m4:"(u, v) ∈ (rstep R)⇧*"
        by auto
      from s2_s m1 have "(s2, t) ∈ (rstep (R ∪ S))⇧*"
        by (metis in_rtrancl_UnI mstep_imp_rsteps rstep_union rtrancl_trans)
      with m3 have "(t,v) ∈ {(t, u) |t u. (t, u) ∈ mstep S ∧ (s2, t) ∈ (rstep (R ∪ S))⇧*}⇧="
        by blast 
      then have *:"(t, v) ∈ (?S b)⇧="
        unfolding b by blast
      from m4 have "(u,v) ∈ (mstep R)⇧*"
        by (meson rstep_mstep_subset rtrancl_mono subsetD) 
      moreover from s2_s m2 have "(s2, u) ∈ (rstep (R ∪ S))⇧*"
        by (metis in_rtrancl_UnI mstep_imp_rsteps rstep_union rtrancl_trans)
      ultimately have "(v, u) ∈ ?conv" 
        using seq_steps_R by simp
      with * show ?thesis by blast
    next
      case 2 (*corresponds to diagram in proof of Theorem 4.3*)
      then obtain s' t' u' w where s':"(s, s') ∈ (rstep (R ∪ S))⇧*" 
                             and cps1:"(s', t') ∈ rstep (CPS_R ren R S)" and mstep1:"(t', t) ∈ mstep R" 
                             and w:"(u, w) ∈ (rstep R)⇧*" and cps2:"(s', u') ∈ rstep (CPS_S ren R S)" and mstep2:"(u', w) ∈ mstep S"
        by blast 
      from cps1 CPS_R_rstep have "(s', t') ∈ rstep R" 
        by blast 
      moreover from cps2 CPS_S_rstep have s'u':"(s',u') ∈ rstep S" 
        by blast
      ultimately obtain v where "(t', v) ∈ (rstep S)⇧*" and "(u', v) ∈ (rstep R)⇧*" 
        using locally_commute_E11[OF lc] by meson 
      then have msteps:"(t', v) ∈ (mstep S)⇧*" "(u', v) ∈ (mstep R)⇧*" 
        by (metis mstep_rsteps_subset rstep_mstep_subset rtrancl_subset)+ 
      have c1:"(t, t') ∈ ?conv" proof-
        from cps1 have "(t', s1) ∈ ?r'"
          using rtrancl_trans[OF s1_s s'] by blast
        then have "(0, t') ∈ under ?r a"
          unfolding a by (simp add: under_def)
        with mstep1 have "(t, t') ∈ (⋃i ∈ (under ?r a). ?R i)¯"
          by blast
        then show ?thesis using UN_Un by blast 
      qed
      have c2:"(u', w) ∈ ?conv" proof-
        from cps2 have "(u', s2) ∈ ?r'" 
          using rtrancl_trans[OF s2_s s'] by blast
        then have "(1, u') ∈ under ?r b"
          unfolding b by (simp add: under_def)
        with mstep2 have "(u', w) ∈ (⋃i ∈ (under ?r b). ?S i)"
          by blast
        then show ?thesis using UN_Un by blast 
      qed
      have c3:"(t', v) ∈ ?conv" proof-
        from cps1 have "(t', s2) ∈ ?r'"
          using rtrancl_trans[OF s2_s s'] by blast
        from seq_steps_S[OF msteps(1) this] have "(t', v) ∈ (⋃i ∈ (under ?r b). ?S i)⇧*"
          by blast 
        then show ?thesis by (simp add: in_rtrancl_UnI)
      qed
      have c4:"(v, u') ∈ ?conv" proof-
        have "(s2, u') ∈ (rstep (R ∪ S))⇧*" using s2_s s'u' s'
          by (metis (no_types, lifting) UnCI rstep_union rtrancl.simps rtrancl_trans) 
        then show ?thesis using seq_steps_R[OF msteps(2)] by simp
      qed
      have c5:"(w, u) ∈ ?conv" proof-
        from w have w:"(u,w) ∈ (mstep R)⇧*"
          by (metis mstep_rsteps_subset rstep_mstep_subset rtrancl_subset)
        have "(s2, u) ∈ (rstep (R ∪ S))⇧*"
          by (metis in_rtrancl_UnI m2 mstep_imp_rsteps rstep_union rtrancl_trans s2_s)   
        then show ?thesis using seq_steps_R[OF w] by simp
      qed
      from c1 c2 c3 c4 c5 have "(t, u) ∈ ?conv"
        by (simp add: relcomp.relcompI)
      then show ?thesis by blast
    qed
  qed
  then show ?thesis
    by (meson commute_between_imp_commute mstep_rsteps_subset rstep_mstep_subset) 
qed

corollary CPS'_SN_rel_imp_comm:
  assumes SN_rel:"SN_rel (rstep (CPS' ren R S) ∪ rstep (CPS' ren S R)) (rstep (R ∪ S))"
  and lc:"locally_commute (rstep R) (rstep S)"
  and R_wf:"left_lin_wf_trs R" and S_wf:"left_lin_wf_trs S"
shows "commute (rstep R) (rstep S)"
proof-
  have "rstep (CPS_R ren R S) ∪ rstep (CPS_S ren R S) ⊆ rstep (CPS' ren R S) ∪ rstep (CPS' ren S R)"
    by (simp add: CPS_R_subset_CPS' CPS_S_subset_CPS' le_supI1 le_supI2 rstep_mono)
  with SN_rel have "SN_rel (rstep (CPS_R ren R S) ∪ rstep (CPS_S ren R S)) (rstep (R ∪ S))"
    by (meson SN_rel_on_mono subset_refl)
  with assms show ?thesis using CPS''_SN_rel_imp_comm by blast
qed

corollary CPS_SN_rel_imp_comm:
  assumes SN_rel:"SN_rel (rstep (CPS ren R S) ∪ rstep (CPS ren S R)) (rstep (R ∪ S))"
  and lc:"locally_commute (rstep R) (rstep S)"
  and R_wf:"left_lin_wf_trs R" and S_wf:"left_lin_wf_trs S"
shows "commute (rstep R) (rstep S)"
proof-
  have "rstep (CPS' ren R S) ∪ rstep (CPS' ren S R) ⊆ rstep (CPS ren R S) ∪ rstep (CPS ren S R)"
    by (meson CPS'_subset_CPS rstep_mono sup.mono)
  with SN_rel have "SN_rel (rstep (CPS' ren R S) ∪ rstep (CPS' ren S R)) (rstep (R ∪ S))"
    by (meson SN_rel_on_mono subset_refl)
  with assms show ?thesis using CPS'_SN_rel_imp_comm by blast
qed

end