Theory CR.Okui_Criterion

(*
original author:                Christina Kirk  (2023-2024)
generalization to commutation:  Rene Thiemann   (2026)
*)
theory Okui_Criterion
imports
  Proof_Terms_Term_Rewriting.Redex_Patterns   
  TRS.Mgu_generic
  TRS.More_Abstract_Rewriting
  Mgu_List
begin

(*Avoid confusion with supremum of Lattices. '⊔' is only used for join on proof terms in this file.*)
no_notation sup (infixl "⊔" 65) 

text‹Only take redexes from A which have overlap with proof term B.› 
definition get_overlapping_part :: "('f, 'v) pterm ⇒ ('f, 'v) pterm ⇒ ('f, 'v) pterm option"
  where "get_overlapping_part A B ≡ 
    let As = filter (λ A'. measure_ov A' B ≠ 0) (single_steps A) in ⨆ As" 

locale ren =
  fixes ren :: "'v :: infinite renamingN" 
    and R :: "('f, 'v) trs"
    and S :: "('f, 'v) trs" 
begin

definition "rename_list ss = 
    map (λ (i, s). (map_vars_term (rename_many' ren i) s)) (zip [0 ..< length ss] ss)" 

definition "rename_redex_patterns redexes =
    map (λ (i, (α, p)). ((map_vars_term (rename_many' ren i) (lhs α)), p)) (zip [0 ..< length redexes] redexes)"

text‹Define simultaneous critical peak (A,B) as pair of proof terms. Requirements:
▪ first proof term (A) represents multistep 
▪ second proof term (B) represents single step
▪ all redex patterns of A overlap with the redex pattern in B
▪ either the redex in B or one of the redexes in A are at the root
▪ there exists an mgu between all of the (renamed) lhss in A and the (renamed) lhs in B 
▪ the proof terms A and B are obtained from combining the mgu with the corresponding rule symbols 
›
definition sim_cp where
  "sim_cp = { (A, B) | τ rdp_A l β q A B As renamed_lhs_αs. 
    A ∈ wf_pterm R ∧ B ∈ wf_pterm S ∧ 
    redex_patterns A = rdp_A ∧ redex_patterns B = [(β, q)] ∧ 
    renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A) ∧
    get_overlapping_part A B = Some A ∧ 
    (q = [] ∨ snd (hd rdp_A) = []) ∧     
    l = replace_at (hd renamed_lhs_αs) q (map_vars_term (ren_l ren) (lhs β)) ∧
    mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) = Some τ ∧ 
    As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩)
          rdp_A [0..<length rdp_A] ∧
    join_list As = Some A ∧
    B = replace_at (to_pterm (l ⋅ τ)) q (Prule β (map (to_pterm ∘ τ ∘ ren_l ren) (var_rule β))) }"

lemma sim_cpI:
  assumes "A ∈ wf_pterm R" and "B ∈ wf_pterm S" 
    and "redex_patterns A = rdp_A" "redex_patterns B = [(β, q)]"
    and "renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A)"
    and "get_overlapping_part A B = Some A"
    and "l = replace_at (hd renamed_lhs_αs) q (map_vars_term (ren_l ren) (lhs β))"
    and "q = [] ∨ snd (hd rdp_A) = []" 
    and "mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) = Some τ"
    and "As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩)
          rdp_A [0..<length rdp_A]" 
    and "join_list As = Some A"
    and "B = replace_at (to_pterm (l ⋅ τ)) q (Prule β (map (to_pterm ∘ τ ∘ (ren_l ren)) (var_rule β)))" 
  shows "(A, B) ∈ sim_cp" 
  using assms unfolding sim_cp_def mem_Collect_eq by blast

lemma sim_cp_A_not_empty:
  assumes "(A, B) ∈ sim_cp"
  shows "¬ is_empty_step A"
proof-
  from assms obtain As s τ rdp_A where "join_list As = Some A" and rdp:"rdp_A = redex_patterns A" and
    As:"As = map (λ((αi, pi), i). replace_at s pi (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))))) (zip rdp_A [0..<length rdp_A])"
    using sim_cp_def by auto 
  then show ?thesis
    by (metis (no_types, lifting) join_list.simps(1) length_nth_simps(1) list.simps(8) 
     option.distinct(1) redex_patterns_to_pterm source_empty_step upt_0 zip.simps(1)) 
qed

lemma rename_redex_patterns_eq_rename_list:
  "map fst (rename_redex_patterns rs) = rename_list (map (λ (α, p). lhs α) rs)" 
proof(induct rs rule:rev_induct)
  case Nil
  then show ?case unfolding rename_redex_patterns_def rename_list_def by simp
next
  case (snoc x xs)
  have *:"zip [0..<length (xs @ [x])] (xs @ [x]) = zip [0..<length xs] xs @ [(length xs, x)]" by simp 
  have 1:"map fst (rename_redex_patterns (xs @ [x])) = (map fst (rename_redex_patterns xs)) @ [map_vars_term (rename_many' ren (length xs)) (lhs (fst x))]"
    unfolding rename_redex_patterns_def * map_append list.map by (simp add: case_prod_beta)
  have *:"zip [0..<length (xs @ [x])] (map (λ(α, p). lhs α) (xs @ [x])) = zip [0..<length xs] (map (λ(α, p). lhs α) xs) @ [(length xs, lhs (fst x))]" 
    unfolding map_append list.map by (simp add: case_prod_beta) 
  have 2:"rename_list (map (λ (α, p). lhs α) (xs @ [x])) = rename_list (map (λ (α, p). lhs α) xs) @ [(map_vars_term (rename_many' ren (length xs)) (lhs (fst x)))]"
    unfolding rename_list_def length_map * unfolding map_append list.map by simp
  show ?case unfolding 1 2 snoc by simp
qed

lemma distinct_linear_renamed_vars:
  assumes "∀s ∈ set ss. linear_term s" 
  shows "distinct (concat (map vars_term_list (rename_list ss)))"
  using assms proof(induct ss rule:rev_induct)
  case Nil
  then show ?case unfolding rename_list_def zip.simps list.map by simp
next
  case (snoc s ss)
  then have IH:"distinct (concat (map vars_term_list (rename_list ss)))"
    by simp
  let ?s_renamed="map_vars_term ((rename_many' ren) (length ss)) s"
  from snoc(2) have "linear_term s" by simp
  then have distinct_s:"distinct (vars_term_list ?s_renamed)"
    using renameN(3) by (metis distinct_map inj_map_vars_term_the_inv linear_term_distinct_vars vars_map_vars_term)
  have *:"zip [0..<length (ss @ [s])] (ss @ [s]) = zip [0..<length ss] ss @ [(length ss, s)]" by simp 
  {fix x assume "x ∈ set (concat (map vars_term_list (rename_list ss)))"
    then obtain i where "x ∈ set (map vars_term_list (map2 (λi. map_vars_term (rename_many' ren i)) [0..<length ss] ss) ! i)" and i:"i < length ss" 
      unfolding rename_list_def set_concat by (smt (verit) UN_E in_set_idx length_map map_nth map_snd_zip) 
    then have "x ∈ set (vars_term_list (map_vars_term ((rename_many' ren) i) (ss!i)))"
      by simp
    with i have "x ∉ vars_term ?s_renamed"
      using renameN(2) by (smt (verit) Collect_mem_eq Int_Collect dual_order.irrefl emptyE image_iff rangeI set_vars_term_list term.set_map(2))
  }
  then have "set (concat (map vars_term_list (rename_list ss))) ∩ set (vars_term_list ?s_renamed) = {}"
    by auto 
  with distinct_s IH show ?case 
    unfolding rename_list_def * map_append by simp
qed

lemma disjoint_concat_renamed_vars:
  shows "set (concat (map vars_term_list (rename_list ss))) ∩ set (vars_term_list (map_vars_term (rename_single ren) t)) = {}"
proof(induct ss rule:rev_induct)
  case Nil
  then show ?case unfolding rename_list_def by simp
next
  case (snoc s ss)
  {fix x assume "x ∈ set (concat (map vars_term_list (rename_list (ss@[s]))))"
    then obtain i where "x ∈ set (map vars_term_list (map2 (λi. map_vars_term (rename_many' ren i)) [0..<Suc (length ss)] (ss@[s]))!i)" 
      and i:"i < Suc (length ss)" 
      unfolding rename_list_def set_concat by (smt (verit, best) UN_E in_set_idx length_append_singleton length_map map_nth map_snd_zip) 
    then have "x ∈ set (vars_term_list (map_vars_term ((rename_many' ren) i) ((ss@[s])!i)))"
      by (metis (no_types, lifting) add.left_neutral case_prod_conv length_append_singleton length_map map_nth map_snd_zip nth_map nth_upt nth_zip)
    then have "x ∉ set (vars_term_list (map_vars_term (rename_single ren) t))"
      using renameN(1) by (smt (verit, best) disjoint_iff imageE rangeI set_vars_term_list term.set_map(2))
  }
  then show ?case by auto
qed

end

locale ren_wf_trs = ren + R:left_lin_wf_trs R + S:left_lin_wf_trs S
begin

lemma sim_cp_co_init:
  assumes "(A, B) ∈ sim_cp"
  shows "source A = source B" 
proof-
  from assms obtain τ rdp_A l β q As renamed_lhs_αs 
    where ren_αs:"renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A)" 
      and l:"l = (ctxt_of_pos_term q (hd renamed_lhs_αs))⟨map_vars_term (rename_single ren) (lhs β)⟩" 
      and mgu:"mgu_list (map2 (λx y. (x, l |_ y)) renamed_lhs_αs (map snd rdp_A)) = Some τ"
      and As:"As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩)
          rdp_A [0..<length rdp_A]" 
      and A:"⨆ As = Some A" 
      and B:"B = (ctxt_of_pos_term q (to_pterm (l ⋅ τ)))⟨Prule β (map (to_pterm ∘ τ ∘ rename_single ren) (var_rule β))⟩" 
      and B_wf:"B ∈ wf_pterm S" and rdp_B:"redex_patterns B = [(β, q)]" 
      and A_wf:"A ∈ wf_pterm R" and rdp_A:"redex_patterns A = rdp_A"
      and root:"q = [] ∨ snd (hd rdp_A) = []" 
      and overlap:"get_overlapping_part A B = Some A"
    unfolding sim_cp_def by blast
  have len:"length As = length rdp_A" 
    unfolding rdp_A As by simp
  have B_single:"B = ll_single_redex (source B) q β" 
    using S.single_steps_singleton[OF B_wf] rdp_B by simp
  moreover from rdp_B B_wf have "q ∈ poss (source B)" 
    using left_lin_no_var_lhs.redex_patterns_label S.ll_no_var_lhs by fastforce 
  moreover from rdp_B B_wf have β:"to_rule β ∈ S"
    by (simp add: left_lin_no_var_lhs.redex_pattern_rule_symbol S.ll_no_var_lhs) 
  ultimately have possL_B:"possL B = {q @ q' |q'. q' ∈ fun_poss (lhs β)}"
    using S.single_redex_possL by fastforce 
  from assms As A have len:"length rdp_A > 0" 
    by force 
  then obtain α0 p0 rdps where rdp_A':"rdp_A = (α0, p0)#rdps"
    by (metis length_greater_0_conv list.collapse split_pairs)
  have ind:"[0..<length rdp_A] = 0 # map (λi. (Suc i)) [0..<length rdps]"  
    unfolding rdp_A' length_Cons using map_upt_Suc[of id "length rdps"] by auto
  then have hd_ren_α:"hd renamed_lhs_αs = map_vars_term (rename_many' ren 0) (lhs α0)" 
    unfolding ren_αs rename_list_def length_map ind unfolding rdp_A' by simp 
  {fix i αi pi assume i:"i < length rdp_A" and αipi:"rdp_A ! i = (αi, pi)"
    then have Ai:"single_steps A ! i = ll_single_redex (source A) pi αi" 
      unfolding rdp_A by simp
    moreover from rdp_A A_wf αipi i have "pi ∈ poss (source A)" 
      using left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs nth_mem by fastforce 
    moreover from rdp_B B_wf have αi:"to_rule αi ∈ R"
      using left_lin_no_var_lhs.redex_pattern_rule_symbol R.ll_no_var_lhs by (metis A_wf αipi i nth_mem rdp_A) 
    ultimately have possL_A:"possL (single_steps A ! i) = {pi @ p' |p'. p' ∈ fun_poss (lhs αi)}" 
      using R.single_redex_possL by fastforce 
    have "measure_ov (single_steps A ! i) B ≠ 0" proof-
      let ?As="filter (λA'. measure_ov A' B ≠ 0) (single_steps A)" 
      from overlap have "⨆ ?As = Some A" 
        unfolding get_overlapping_part_def by simp
      then have "set (single_steps A) =  ⋃ (set (map (set ∘ single_steps) ?As))"
        by (metis (no_types, lifting) A_wf filter_is_subset in_mono R.single_step_wf R.single_steps_join_list) 
      moreover have "⋃ (set (map (set ∘ single_steps) ?As)) = set ?As" proof-
        {fix Ai assume Ai:"Ai ∈ set ?As"
          from Ai have src:"source Ai = source A"
            by (intro R.source_single_step[OF _ A_wf], auto)
 
 
          from Ai obtain αi pi where Ai':"Ai = ll_single_redex (source A) pi αi" and "(αi, pi) ∈ set (redex_patterns A)"  
            by auto
          then have *:"redex_patterns Ai = [(αi, pi)]" 
            using A_wf left_lin_no_var_lhs.redex_patterns_single left_lin_no_var_lhs.redex_pattern_rule_symbol 
              left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs by blast 
          have "(set ∘ single_steps) Ai = {Ai}"
            unfolding comp_apply * list.map case_prod_conv using Ai' src by simp
        }
        then show ?thesis unfolding set_map
          by (smt (verit, ccfv_threshold) Inf.INF_cong UN_singleton)
      qed
      ultimately have "single_steps A ! i ∈ set ?As" 
        using i by (metis (no_types, lifting) length_map nth_mem rdp_A) 
      then show ?thesis
        by simp 
    qed
    then have possL:"{pi @ p' |p'. p' ∈ fun_poss (lhs αi)} ∩ {q @ q' |q'. q' ∈ fun_poss (lhs β)} ≠ {}" 
      unfolding possL_A possL_B by force
    with possL_B possL_A consider "q ≤⇩p pi" | "pi <⇩p q"
      by (smt (verit, ccfv_threshold) card_eq_0_iff disjoint_iff less_eq_pos_simps(1) mem_Collect_eq pos_cases pos_less_eq_append_not_parallel) 
    then have "(∃q'. q@q' = pi ∧ q' ∈ fun_poss (lhs β)) ∨ (∃p'. pi@p' = q ∧ p' ∈ fun_poss (lhs αi))"
    proof(cases)
      case 1
      then obtain q' where q':"pi = q@q'"
        using prefix_pos_diff by metis
      have "is_Fun (lhs β)" 
        using β using no_var_lhs.no_var_lhs S.no_var_lhs_axioms by fastforce
      with possL have "q' ∈ fun_poss (lhs β)" 
        unfolding q' using fun_poss_append_poss' by fastforce
      with q' show ?thesis by simp
    next
      case 2
      then obtain p' where p':"q = pi@p'"
        using less_pos_def' by blast 
      have "is_Fun (lhs αi)" 
        using αi using no_var_lhs.no_var_lhs R.no_var_lhs_axioms by fastforce
      with possL have "p' ∈ fun_poss (lhs αi)" 
        unfolding p' using fun_poss_append_poss' by fastforce
      with p' show ?thesis by simp
    qed
  }note poss_q_p=this
  have q:"q ∈ poss (lhs α0)" proof-
    consider "q = []" | "p0 = []" 
      using root rdp_A' by fastforce
    then show ?thesis proof(cases)
      case 1
      then show ?thesis by simp
    next
      case 2
      have 0:"0 < length rdp_A" "rdp_A ! 0 = (α0, p0)" 
        unfolding rdp_A' by simp_all
      consider "(∃q'. q @ q' = [] ∧ q' ∈ fun_poss (lhs β))" | "(∃p'. [] @ p' = q ∧ p' ∈ fun_poss (lhs α0))"
        using poss_q_p[OF 0] unfolding 2 by auto
      then show ?thesis by(cases, simp_all add: fun_poss_imp_poss)
    qed
  qed
  {fix i assume i:"i < length rdp_A" 
    let ?αi="fst (rdp_A ! i)" and ?pi="snd (rdp_A ! i)"
    have αipi:"(?αi, ?pi) ∈ set rdp_A"
      using i by simp  
    from A_wf αipi have 1:"to_rule ?αi ∈ R" 
      using rdp_A using left_lin_no_var_lhs.redex_pattern_rule_symbol R.ll_no_var_lhs by blast 
    have 2:"?pi ∈ poss l" proof(cases i)
      case 0
      then have 0:"?pi = p0"
        using rdp_A' by auto 
      consider "q = []" | "p0 = []"
        using rdp_A' root by fastforce 
      then show ?thesis proof(cases)
        case 1
        from poss_q_p[OF i, unfolded 1] consider "p0 = []" | "p0 ∈ fun_poss (lhs β)"
          by (metis "0" Nil_is_append_conv append_self_conv2 prod.collapse)   
        then show ?thesis by(cases, simp_all add: 0 1 l fun_poss_imp_poss)
      qed (simp add: 0)
    next
      case (Suc n)
      then have "q <⇩p ?pi" proof-
        consider (p0_less_pi) "p0 <⇩p ?pi" | (p0_par) "p0 ⊥ ?pi" 
          using left_lin_no_var_lhs.redex_patterns_order[OF R.ll_no_var_lhs] A_wf Suc i
          by (metis nth_Cons_0 parallel_pos_sym pos_cases prod.collapse rdp_A rdp_A' zero_less_Suc)
        note cases1=this
        from poss_q_p[of 0, unfolded rdp_A'] consider (q_less) "q ≤⇩p p0" | (p0_less_q) "∃p'. p0@p' = q ∧ p' ∈ fun_poss (lhs α0)"
          by force
        note cases2=this
        from poss_q_p[OF i] consider "q <⇩p ?pi" | (pi_less_q) "?pi ≤⇩p q"
          by (metis less_eq_pos_simps(1) prefix_order.less_le prod.collapse)
        note cases3=this
        from cases3 show ?thesis proof(cases)
          case pi_less_q
          from cases1 show ?thesis proof(cases)
            case p0_less_pi
            with cases2 show ?thesis proof(cases)
              case p0_less_q
              then obtain p' where p':"p0@p' = q" "p' ∈ fun_poss (lhs α0)" by auto
              from p0_less_pi obtain p'' where "p0@p'' = ?pi" "p'' ∉ fun_poss (lhs α0)"  
                using R.redex_patterns_below[OF A_wf]
                by (metis αipi len less_pos_def' nth_Cons_0 nth_mem rdp_A rdp_A')  
              with p' pi_less_q show ?thesis
                by (metis fun_poss_append_poss' less_eq_pos_simps(2) prefix_pos_diff)
            qed simp
          next
            case p0_par
            with cases2 show ?thesis proof(cases)
              case q_less
              with p0_par pi_less_q show ?thesis
                using prefix_order.trans parallel_pos by blast
            next
              case p0_less_q
              with p0_par show ?thesis
                using rdp_A' root by force 
            qed
          qed
        qed simp
      qed
      with poss_q_p[OF i] obtain q' where "q @ q' = ?pi" and "q' ∈ fun_poss (lhs β)"
        by (metis less_pos_simps(5) prod.collapse) 
      then show ?thesis unfolding l hd_ren_α using q
        by (metis fun_poss_imp_poss hole_pos_ctxt_of_pos_term hole_pos_poss poss_append_poss poss_map_vars_term subt_at_hole_pos)
    qed
    note 1 and 2
  }note rdp_i=this
  {fix Ai assume "Ai ∈ set As" 
    then obtain i where i:"i < length As" and Ai:"Ai = As ! i"
      by (meson in_set_idx)
    then have i:"i < length rdp_A" 
      unfolding As by auto
    then obtain αi pi where αipi:"rdp_A ! i = (αi, pi)"
      by fastforce 
    then have pi:"pi ∈ poss (l ⋅ τ)" and αi:"to_rule αi ∈ R"
      using rdp_i i len nth_mem by fastforce+
    from i have "i < length (zip rdp_A [0..<length rdp_A])" by auto
    moreover then have "zip rdp_A [0..<length rdp_A] ! i = ((αi, pi), i)"
      by (simp add: αipi)
    ultimately have Ai':"Ai = (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩"
      unfolding As Ai by simp
    have "Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))) ∈ wf_pterm R" 
      using to_pterm_wf_pterm αi by (simp add: wf_pterm.intros(3)) 
    then have "Ai ∈ wf_pterm R"
      unfolding Ai' using ctxt_wf_pterm[OF to_pterm_wf_pterm[of "(l ⋅ τ)"] p_in_poss_to_pterm[OF pi]] by simp 
  }note as_wf=this
  have src_A:"source A = l ⋅ τ" proof-
    from As obtain A0 As' where As:"As = A0 # As'" 
      and A0:"A0 = (ctxt_of_pos_term p0 (to_pterm (l ⋅ τ)))⟨Prule α0 (map (to_pterm ∘ τ) (map (rename_many' ren 0) (var_rule α0)))⟩"
      unfolding ind unfolding rdp_A' by simp
    have p0:"p0 ∈ poss l"
      using rdp_A' rdp_i(2) by force 
    let ?es="set (map2 (λx y. (x, l |_ y)) renamed_lhs_αs (map snd rdp_A))"
    have "(map_vars_term (rename_many' ren 0) (lhs α0), l |_ p0) ∈ ?es" 
      unfolding ren_αs length_map rename_list_def ind unfolding rdp_A' by simp
    moreover have "τ ∈ unifiers ?es" 
      using mgu_list_Some[OF mgu] unfolding is_imgu_def by blast
    ultimately have "l |_ p0 ⋅ τ = map_vars_term (rename_many' ren 0) (lhs α0) ⋅ τ" 
      by fastforce
    then have "l ⋅ τ |_ p0 = lhs α0 ⋅ ⟨map (τ ∘ rename_many' ren 0) (var_rule α0)⟩⇩α0"
      using p0 by (metis apply_subst_map_vars_term empty_pos_in_poss lhs_subst_var_rule subt_at.simps(1) subt_at_subst vars_term_subt_at) 
    then have "source A0 = l ⋅ τ" 
      unfolding A0 using p0 by (metis (no_types, lifting) context_source list.map_comp poss_imp_subst_poss replace_at_ident 
          source.simps(2) source.simps(3) source_to_pterm term.inject(2) to_pterm.simps(2) to_pterm_ctxt_of_pos_apply_term) 
    then show ?thesis 
      using left_lin_no_var_lhs.source_join_list[OF R.ll_no_var_lhs] A as_wf As by simp
  qed
  have src_B:"source B = l ⋅ τ" proof-
    from q have q2:"q ∈ poss l" 
      unfolding l by (metis hd_ren_α hole_pos_ctxt_of_pos_term hole_pos_poss poss_map_vars_term) 
    have "l ⋅ τ |_ q = map_vars_term (rename_single ren) (lhs β) ⋅ τ" 
      unfolding l subst_apply_term_ctxt_apply_distrib
      by (metis hd_ren_α hole_pos_ctxt_of_pos_term hole_pos_subst poss_map_vars_term q subt_at_hole_pos)
    then have "l ⋅ τ |_ q = lhs β ⋅ ⟨map (τ ∘ rename_single ren) (var_rule β)⟩⇩β"
      by (smt (verit, ccfv_SIG) comp_def eval_eq_map_vars eval_term.simps(1) lhs_subst_var_rule vars_term_poss_subt_at vars_term_subt_at) 
    then have "source (Prule β (map (to_pterm ∘ τ ∘ rename_single ren) (var_rule β))) = l ⋅ τ |_ q"
      unfolding source.simps map_map comp_apply source_to_pterm by simp
    then show ?thesis unfolding B using q2
      by (simp add: replace_at_ident source_to_pterm_ctxt to_pterm_ctxt_at_pos)
  qed
  from src_A src_B show ?thesis by simp
qed

end

hide_const (open) FuncSet.compose

locale tau =
  fixes ss :: "('f, 'v) term list" and t :: "('f, 'v) term"
    and ps :: "pos list" 
  assumes l:"length ss = length ps"
    and lin_t:"linear_term t" and lin_s:"∀s ∈ set ss. linear_term s"
    and poss:"∀p ∈ set ps. p ∈ poss t" 
    and disj:"∀s ∈ set ss. vars_term s ∩ vars_term t = {}" "∀i j. i < j ∧ j < length ss ⟶ vars_term (ss!i) ∩ vars_term (ss!j) = {}" 
begin

definition "τs = (map2 (λ s p. linear_unifier s (t|_p)) ss ps)"

definition "τ = compose (map2 (λ s p. linear_unifier s (t|_p)) ss ps)" 

(*The slightly awkward introduction of τ' is used in one of the lemmas for Okui's theorem. 
For more explanation see the comment for lemma σ_τ'_y below.*)
lemma apply_tau_t_var: 
  assumes tau:"τ' = compose (drop k (map2 (λ s p. linear_unifier s (t|_p)) ss ps))"
    and k:"k ≤ length ss"
    and r:"r ∈ var_poss t" "t|_r = Var x" 
  shows "τ' x = Var x ∨ (∃i r'. i < length ss ∧ ps!i @ r' = r ∧ r' ∈ poss (ss!i) ∧ τ' x = ss!i|_r')" 
proof-
  from r have x:"x ∈ vars_term t"
    by (metis vars_term_var_poss_iff) 
  {assume tau_x:"τ' x ≠ Var x" 
    from assms(2) l have k:"k ≤ length (map2 (λx y. linear_unifier x (t |_ y)) ss ps)" by simp
    let ?τs="drop k (map2 (λ s p. linear_unifier s (t|_p)) ss ps)"
    obtain i where i:"i < length ?τs" "∀j < i. (?τs!j) x = Var x" "(?τs!i) x ≠ Var x"  
      using compose_exists_subst[OF tau_x[unfolded tau]] by blast 
    then have ik:"i + k < length (map2 (λ s p. linear_unifier s (t|_p)) ss ps)" by auto
    let ?τ1="compose (take i ?τs)"
    let ?τ2="compose (drop (i+1) ?τs)" 
    have tau_decomp:"τ' = compose [?τ1, ?τs!i, ?τ2]" 
      using i(1) unfolding tau by (metis (no_types, lifting) Cons_nth_drop_Suc Suc_eq_plus1 append_self_conv append_take_drop_id compose_append compose_simps(3)) 
    from disj have 1:"vars_term (ss ! (i+k)) ∩ vars_term (t |_ ps ! (i+k)) = {}"
      by (metis (no_types, lifting) Int_left_commute ik inf.orderE inf_bot_right length_map length_zip min_less_iff_conj nth_mem poss vars_term_subt_at)
    from lin_s i(1) have 2:"linear_term (ss ! (i+k))" by simp
    from lin_t i(1) l poss have 3:"linear_term (t|_(ps!(i+k)))" by (simp add: subt_at_linear)
    from i(1) have drop_k:"drop k (map2 (λx y. linear_unifier x (t |_ y)) ss ps) ! i = (map2 (λx y. linear_unifier x (t |_ y)) ss ps) ! (i+k)"
      by (metis (no_types, lifting) Cons_nth_drop_Suc drop_drop nth_via_drop) 
    from x disj i(1) poss have "x ∉ vars_term (ss!(i+k))" by auto
    then obtain u where u:"(?τs!i) x = u" "(x,u) ∈ set (right_substs (ss!(i+k)) (t|_(ps!(i+k))))" 
      using i(3) ik linear_unifier_obtain_binding[OF 1 2 3] unfolding drop_k by auto  
    obtain q where q:"q ∈ poss (ss!(i+k))" "q ∈ poss (t |_ ps ! (i+k))" "t |_ ps ! (i+k) |_ q = Var x" 
      and tau_i: "(?τs!i) x = (ss!(i+k))|_q"
      using right_substs_imp_props[OF u(2)] using fun_poss_imp_poss u(1) by blast
    from i(2) have tau_1:"?τ1 x = Var x" using compose_exists_subst i(1) by force  
    (*Show that ss!i_q is not affected by any of the taus afterwards*)
    have "(ss!(i+k))|_q ⋅ ?τ2 = (ss!(i+k))|_q" proof-
      {fix τj assume tau_j:"τj ∈ set (drop (i+1) ?τs)" 
        then have "i+1 < length ?τs" using not_less_less_Suc_eq by fastforce  
        with tau_j obtain j where j:"j < length ?τs" "i < j" "τj = ?τs!j" 
          by (smt (verit) Suc_eq_plus1 add.commute drop_eq_nths in_set_conv_nth length_drop lessI less_diff_conv less_imp_le_nat nth_drop trans_less_add2) 
        then have jk':"j + k < length (map2 (λx y. linear_unifier x (t |_ y)) ss ps)" by auto
        then have jk:"k + j < length (zip ss ps)" by auto
        then have zip:"(zip ss ps)!(j+k) = (ss!(j+k), ps!(j+k))" by simp
        then have tau_j_eq:"τj = linear_unifier (ss!(j+k)) (t|_(ps!(j+k)))"
          unfolding j(3) nth_drop[OF k] nth_map[OF jk] by (simp add: add.commute)
        from j disj(2) have "vars_term (ss!(i+k)) ∩ vars_term (ss!(j+k)) = {}" by simp 
        then have "set (map fst (left_substs (ss!(j+k)) (t|_(ps!(j+k))))) ∩ vars_term (ss!(i+k)) = {}" 
          using map_fst_left_substs by fastforce
        moreover have "set (map fst (right_substs (ss!(j+k)) (t|_(ps!(j+k))))) ∩ vars_term (ss!(i+k)) = {}" 
          using map_fst_right_substs disj(1) j jk' l nth_mem poss vars_term_subt_at by fastforce
        ultimately have "(ss!(i+k)) ⋅ τj = ss!(i+k)" unfolding tau_j_eq subst_of_append subst_compose
          by (smt (verit, del_insts) disjoint_iff eval_same_vars_cong eval_term.simps(1) not_elem_subst_of subst_apply_term_empty)
      }
      then show ?thesis
        by (smt (verit, ccfv_threshold) compose_exists_subst eval_same_vars eval_term.simps(1) nth_mem q(1) subst_apply_term_empty subt_at_subst vars_term_poss_subt_at)
    qed
    then have "τ' x = (ss!(i+k))|_q" 
      unfolding tau_decomp compose_simps subst_compose tau_1 eval_term.simps tau_i by force 
    moreover from q lin_t r have "ps!(i+k) @ q = r"
      by (metis (no_types, lifting) ik l length_map length_zip linear_term_unique_vars min.idem nth_mem pos_append_poss poss subt_at_append var_poss_imp_poss)
    ultimately have "∃i r'. i < length ss ∧ ps!i @ r' = r ∧ r' ∈ poss (ss!i) ∧ τ' x = ss!i|_r'"
      using ik q by auto
  }
  then show ?thesis by blast 
qed

lemma apply_tau_t_var': 
  assumes r:"r ∈ var_poss t" "t|_r = Var x" 
  shows "τ x = Var x ∨ (∃i r'. i < length ss ∧ ps!i @ r' = r ∧ r' ∈ poss (ss!i) ∧ τ x = ss!i|_r')" 
proof-
  have *:"τ = compose (drop 0 (map2 (λ s p. linear_unifier s (t|_p)) ss ps))"
    by (simp add: τ_def) 
  show ?thesis using apply_tau_t_var[OF * le0 r] by simp 
qed

lemma apply_tau_ss_var: 
  assumes i:"i < length ss"
    and x:"x ∈ vars_term (ss!i)" and r:"r ∈ var_poss (ss!i)" "(ss!i)|_r = Var x" 
  shows "τ x = Var x ∨ (r ∈ poss (t|_(ps!i)) ∧ τ x = t|_(ps!i) |_ r ⋅ compose (drop (Suc i) (map2 (λ s p. linear_unifier s (t|_p)) ss ps)))" 
proof-
  {assume tau_x:"τ x ≠ Var x" 
    from i l have i:"i < length (map2 (λx y. linear_unifier x (t |_ y)) ss ps)" by simp
    let ?τs="map2 (λ s p. linear_unifier s (t|_p)) ss ps"
    let ?τ1="compose (take i ?τs)"
    let ?τ2="compose (drop (Suc i) ?τs)" 
    have tau_decomp:"τ = compose [?τ1, ?τs!i, ?τ2]" 
      using i by (metis (mono_tags, lifting) Cons_nth_drop_Suc τ_def append_take_drop_id compose_append compose_simps(1) compose_simps(3) subst_monoid_mult.mult_1_right) 
    have "∀j < length ss. j ≠ i ⟶ (?τs!j) x = Var x" proof-
      {fix j assume j:"j < length ss" "j ≠ i" 
        from disj(2) j i x have "x ∉ vars_term (ss!j)"
          using nat_neq_iff by auto
        moreover from disj(1) i x poss have "x ∉ vars_term (t|_(ps!j))"
          by (metis (mono_tags, lifting) assms(1) disjoint_iff in_mono j(1) l nth_mem vars_term_subt_at)
        moreover from j i have "?τs!j = linear_unifier (ss!j) (t|_(ps!j))" by (simp add: l) 
        ultimately have "(?τs!j) x = Var x"
          by (smt (verit) add_lessD1 assms(1) canonically_ordered_monoid_add_class.lessE disj(1) inf.absorb_iff1 inf_bot_right inf_left_commute 
              j l lin_s lin_t linear_unifier_obtain_binding nth_mem poss subt_at_linear vars_term_subt_at) 
      }
      then show ?thesis by simp
    qed note tau_i_x=this
    then have tau1_x:"?τ1 x = Var x"
      using i by (smt (verit, best) compose_exists_subst length_map length_take length_zip min_less_iff_conj nth_take) 
    from tau_i_x i have "∀j < length (drop (Suc i) ?τs). (?τs!(j + Suc i)) x = Var x" by simp
    then have tau2_x:"?τ2 x = Var x" 
      using i by (metis (no_types, lifting) Suc_leI add.commute compose_exists_subst nth_drop)  
    from disj have 1:"vars_term (ss ! i) ∩ vars_term (t |_ ps ! i) = {}"
      by (metis (no_types, lifting) Int_left_commute i inf.orderE inf_bot_right length_map length_zip min_less_iff_conj nth_mem poss vars_term_subt_at)
    from lin_s i have 2:"linear_term (ss ! i)" by simp
    from lin_t i l poss have 3:"linear_term (t|_(ps!i))" by (simp add: subt_at_linear)
    from tau_x tau1_x tau2_x have "(?τs!i) x ≠ Var x"
      by (metis (no_types, lifting) τ_def compose_exists_subst length_map length_zip min_less_iff_conj tau_i_x) 
    then obtain u where tau_i:"(?τs!i) x = u" and xu:"(x,u) ∈ set (left_substs (ss!i) (t|_(ps!i)))" 
      using i linear_unifier_obtain_binding[OF 1 2 3] x 1 by auto
    then have r:"r ∈ poss (t|_(ps!i))" and u:"u = t|_(ps!i) |_r " 
      using left_substs_imp_props[OF xu] r lin_s i linear_term_unique_vars var_poss_imp_poss by fastforce+
    from tau1_x have "τ x = (?τs!i) x ⋅ ?τ2" 
      unfolding tau_decomp compose_simps by (simp add: subst_compose)  
    then have "r ∈ poss (t|_(ps!i)) ∧ τ x = t|_(ps!i) |_ r ⋅ ?τ2" 
      unfolding tau_i u using assms(1) l poss r by auto 
  }
  then show ?thesis by blast 
qed

lemma apply_tau_var: 
  assumes "∀i < length ss. x ∉ vars_term (ss!i)" and "x ∉ vars_term t"
  shows "τ x = Var x" 
proof-
  from assms(1) l poss disj have "(compose (map2 (λ s p. linear_unifier s (t|_p)) ss ps)) x = Var x" 
  proof(induct "length ss" arbitrary:ss ps)
    case (Suc n)
    then obtain s ss' where ss:"ss = s#ss'"
      by (metis length_Suc_conv) 
    from Suc obtain p ps' where ps:"ps = p#ps'"
      by (metis length_Suc_conv) 
    let ?τ="compose (map2 (λx y. linear_unifier x (t |_ y)) ss' ps')" 
    have tau:"(compose (map2 (λ s p. linear_unifier s (t|_p)) ss ps)) = linear_unifier s (t|_p) ∘⇩s ?τ" 
      unfolding ss ps by simp
    from Suc(1)[of ss' ps'] have IH:"?τ x = Var x"
      by (smt (verit, del_insts) Suc Suc_leI le_imp_less_Suc length_Suc_conv list.inject list.set_intros(2) nth_Cons_Suc ps ss) 
    have "(linear_unifier s (t|_p)) x = Var x" proof-
      from Suc(3) have "x ∉ vars_term s" unfolding ss by auto
      moreover have "x ∉ (vars_term (t|_p))" 
        using assms(2) using Suc.prems(3) ps vars_ctxt_pos_term by auto 
      ultimately show ?thesis 
        using linear_unifier_id by metis 
    qed
    with IH show ?case unfolding tau
      by (simp add: subst_compose)
  qed simp
  then show ?thesis
    using τ_def by presburger 
qed

lemma var_at_t_tau:
  assumes "t ⋅ τ |_ r = Var x" "r ∈ poss (t ⋅ τ)" 
  shows "(r ∈ poss t ∧ t |_ r = Var x) ∨ 
  (∃i r1 r2 y. r = ps!i@r1@r2 ∧ r1 ∈ poss (ss ! i) ∧ r2 ∈ poss (ss!i |_ r1) ∧ ps!i @ r1 ∈ poss t ∧ 
    t |_ (ps!i@r1) = Var y ∧ τ y |_ r2 = Var x ∧ τ y = ss!i |_ r1 ∧ i < length ss)" 
proof(cases "r ∈ poss t ∧ t |_ r = Var x")
  case False
  with assms obtain r1 r2 y where r:"r = r1@r2" and r1:"r1 ∈ poss t" "t |_ r1 = Var y" and r2:"r2 ∈ poss (τ y)" "τ y |_ r2 = Var x"
    by (smt (verit, best) is_FunE poss_subst_choice subst_apply_eq_Var subt_at_subst term.distinct(1))
  then obtain i r' where "i < length ss" "ps ! i @ r' = r1" "r' ∈ poss (ss ! i)" "τ y = ss ! i |_ r'" 
    using apply_tau_t_var' by (smt (verit, ccfv_SIG) False append.right_neutral poss_append_poss subt_at.simps(1) var_pos_maximal var_poss_iff)
  then show ?thesis
    by (metis append_assoc r r1 r2)
qed simp

lemma tau_is_unifier:
  assumes ts:"unify (zip ss (map (λp. t|_p) ps)) [] = Some ts" 
    and τ':"subst_of ts = τ'"
    and "⋀i j r. i < j ⟹ j < length ps ⟹ ¬ (ps ! i @ r) ⊥ ps ! j ⟹ r ∈ var_poss (t|_(ps!i)) ⟹ r ∉ fun_poss (ss!i)" 
  shows "τ = τ'"
proof-
  have τ_alt:"τ = compose (subst_of [] # map2 linear_unifier ss (map ((|_) t) ps))"
    unfolding τ_def by (simp add: map_zip_map2)
  have lin:"∀t∈set (map fst (zip ss (map ((|_) t) ps))) ∪ set (map snd (zip ss (map ((|_) t) ps))). linear_term t" 
    using lin_t lin_s l poss subt_at_linear by fastforce 
  {fix i j σi assume i:"i < j" and j:"j < length (zip ss (map ((|_) t) ps))" 
      and "σi = linear_unifier (fst (zip ss (map ((|_) t) ps) ! i)) (snd (zip ss (map ((|_) t) ps) ! i))"
    then have σi:"σi = linear_unifier (ss ! i) (t |_ (ps ! i))"
      by auto 
    obtain ssj tj where ssj_tj:"zip ss (map ((|_) t) ps) ! j = (ssj, tj)"
      by force 
    have vars_subst_σi:"vars_subst σi ⊆ vars_term (ss ! i) ∪ vars_term (t |_ (ps!i))"
      unfolding σi using vars_subst_linear_unifier by simp
    have "ssj ⋅ σi = ssj" proof-
      from vars_subst_σi have "vars_term ssj ∩ vars_subst σi = {}" 
        using disj i j ssj_tj  by (smt (verit, ccfv_threshold) Un_iff disjoint_iff dual_order.strict_trans 
            fst_conv in_mono l length_zip min_less_iff_conj nth_mem nth_zip poss vars_term_subt_at)
      then show ?thesis
        by (simp add: boolean_algebra.conj_disj_distrib subst_apply_term_ident vars_subst_def)
    qed
    moreover have "tj ⋅ σi = tj" proof-
      {fix y assume y:"y ∈ vars_term tj" "σi y ≠ Var y" 
        then have "y ∈ vars_subst σi"
          by (metis UnCI notin_subst_domain_imp_Var vars_subst_def)
        with vars_subst_σi have y_in_ti:"y ∈ vars_term (t |_ (ps!i))" 
          using ssj_tj disj(1) i j l nth_mem poss vars_term_subt_at y(1) by fastforce
        have vars_term_disj:"vars_term (ss ! i) ∩ vars_term (t |_ (ps ! i)) = {}" 
          using i disj(1) j poss vars_term_subt_at by fastforce 
        from i j have lin_ssi:"linear_term (ss ! i)"
          using lin_s by auto 
        from i j have lin_ti:"linear_term (t |_ ps ! i)"
          by (simp add: lin_t poss subt_at_linear) 
        obtain u where u:"(y, u) ∈ set (right_substs (ss ! i) (t |_ (ps ! i)))" "σi y = u"
          using linear_unifier_obtain_binding[OF vars_term_disj lin_ssi lin_ti] y(2)[unfolded σi] y_in_ti σi vars_term_disj by force  
        then obtain r where r:"r ∈ fun_poss (ss ! i)" "(ss ! i) |_ r = u" "r ∈ poss (t |_ ps ! i)" "(t |_ ps ! i) |_ r = Var y"   
          using right_substs_imp_props by metis
        {assume "(ps ! i @ r) ⊥ ps ! j" 
          then have False using lin_t r(3,4) y_in_ti
            by (smt (verit, best) disjoint_iff dual_order.strict_trans i j l length_map linear_subterms_disjoint_vars map_nth_conv map_snd_zip nth_mem 
                pos_append_poss poss snd_conv ssj_tj subt_at_append term.set_intros(3) vars_term_poss_subt_at vars_term_subt_at y(1)) 
        }
        then have not_orth:"¬ (ps ! i @ r) ⊥ ps ! j" 
          by fastforce 
        from j have j:"j < length ps"
          by simp 
        from assms(3)[OF i j not_orth] r have False
          using var_poss_iff by blast
      }
      then show ?thesis
        using term_subst_eq by force
    qed
    ultimately have "fst (zip ss (map ((|_) t) ps) ! j) ⋅ σi = fst (zip ss (map ((|_) t) ps) ! j) ∧
                     snd (zip ss (map ((|_) t) ps) ! j) ⋅ σi = snd (zip ss (map ((|_) t) ps) ! j)"
      using ssj_tj by simp
  } moreover 
  {fix i assume i:"i < length (zip ss (map ((|_) t) ps))" 
    then have "vars_term (fst (zip ss (map ((|_) t) ps) ! i)) = vars_term (ss ! i)"
      by simp 
    moreover have "vars_term (snd (zip ss (map ((|_) t) ps) ! i)) ⊆ vars_term t"
      by (metis i l length_zip min_less_iff_conj nth_map nth_mem nth_zip snd_conv tau.poss tau_axioms vars_term_subt_at) 
    ultimately have "vars_term (fst (zip ss (map ((|_) t) ps) ! i)) ∩ vars_term (snd (zip ss (map ((|_) t) ps) ! i)) = {}" 
      using disj(1) i by force
  }
  ultimately show ?thesis 
    using unify_linear_terms[OF ts τ_alt[symmetric] lin] τ' by presburger  
qed

lemma ss_i_τ_eq_t_τ:
  assumes "∃ts. unify (zip ss (map (λp. t|_p) ps)) [] = Some ts"  
  and i:"i < length ss"
  and "⋀i j r. i < j ⟹ j < length ps ⟹ ¬ (ps ! i @ r) ⊥ ps ! j ⟹ r ∈ var_poss (t|_(ps!i)) ⟹ r ∉ fun_poss (ss!i)" 
  shows "ss!i ⋅ τ = t |_ (ps!i) ⋅ τ"
proof-
  from assms(1) obtain ts where ts:"unify (zip ss (map (λp. t|_p) ps)) [] = Some ts"
    by force 
  let ?es="zip ss (map (λp. t|_p) ps)"
  have ss_i:"ss ! i = fst (?es ! i)"
    using i l by auto 
  have t_at_pi:"t |_ (ps ! i) = snd (?es ! i)"
    using i l by force 
  obtain τ' where τ':"subst_of ts = τ'"
    by simp 
  then have "is_imgu τ' (set ?es)" 
    using unify_sound[OF ts] by simp
  then have *:"ss!i ⋅ τ' = t |_ (ps!i) ⋅ τ'" 
    unfolding ss_i t_at_pi by (metis i in_unifiersE is_imgu_def l length_map length_zip min_less_iff_conj nth_mem) 
  from tau_is_unifier[OF ts τ' assms(3)] have "τ = τ'" .
  with * show ?thesis
    by auto 
qed

lemma linear_term_t_tau:
  shows "linear_term (t ⋅ τ)" 
proof- 
  {fix r1 r2 x assume r1:"r1 ∈ poss (t ⋅ τ)" "t ⋅ τ |_ r1 = Var x" 
                  and r2:"r2 ∈ poss (t ⋅ τ)" "t ⋅ τ |_ r2 = Var x"
                  and r1r2:"r1 ≠ r2" 
  have False proof(cases "r1 ∈ poss t ∧ t|_r1 = Var x")
    case True
    then have x:"x ∈ vars_term t"
      by (metis var_poss_iff vars_term_var_poss_iff)
    show ?thesis proof(cases "r2 ∈ poss t ∧ t|_r2 = Var x")
      case True
      with ‹r1 ∈ poss t ∧ t|_r1 = Var x› show ?thesis 
        using r1r2 lin_t by (meson linear_term_unique_vars)
    next 
      case False
      then obtain i p1 p2 y where "p1 ∈ poss (ss ! i)" "p2 ∈ poss (ss ! i |_ p1)" "τ y |_ p2 = Var x" 
        "τ y = ss ! i |_ p1" and i:"i < length ss"
        using var_at_t_tau[OF r2(2) r2(1)] by auto
      then have "x ∈ vars_term (ss!i)"
        by (metis (no_types, lifting) subsetD term.set_intros(3) vars_term_subt_at) 
      with x show ?thesis 
        using disj(1) i by (meson disjoint_iff nth_mem)
    qed
  next
    case False
    then obtain i p1 p2 y where p1:"p1 ∈ poss (ss ! i)" "t |_ (ps ! i @ p1) = Var y" "ps!i @ p1 ∈ poss t"
        and p2:"p2 ∈ poss (ss ! i |_ p1)" "ss ! i |_ p1 |_ p2 = Var x" 
        and i:"i < length ss" and r1':"r1 = ps ! i @ p1 @ p2" 
      using var_at_t_tau[OF r1(2) r1(1)] by metis
    then have x:"x ∈ vars_term (ss!i)"
      by (metis (no_types, lifting) subsetD term.set_intros(3) vars_term_subt_at)
    show ?thesis proof(cases "r2 ∈ poss t ∧ t |_ r2 = Var x")
      case True
      then have "x ∈ vars_term t"
        by (metis subsetD term.set_intros(3) vars_term_subt_at) 
      with x show ?thesis 
        using disj(1) i by (meson disjoint_iff nth_mem)
    next
      case False
      then obtain j q1 q2 z where q1:"q1 ∈ poss (ss ! j)" "t |_ (ps ! j @ q1) = Var z" "ps!j @ q1 ∈ poss t"
        and q2:"q2 ∈ poss (ss ! j |_ q1)" "ss ! j |_ q1 |_ q2 = Var x" 
        and j:"j < length ss" and r2':"r2 = ps ! j @ q1 @ q2" 
        using var_at_t_tau[OF r2(2) r2(1)] by metis
      then have x2:"x ∈ vars_term (ss!j)" 
        by (metis (no_types, lifting) subsetD term.set_intros(3) vars_term_subt_at)
      show ?thesis proof(cases "i = j")
        case True
        then show ?thesis proof(cases "p1 = q1")
          case True
          have "linear_term (ss!i)" 
            using lin_s i nth_mem by blast
          moreover from p1 p2 have "ss!i |_ (p1 @ p2) = Var x" "p1 @ p2 ∈ poss (ss!i)" by simp_all
          moreover from q1 q2 ‹i=j› ‹p1=q1› have "ss!i |_ (p1 @ q2) = Var x" "p1 @ q2 ∈ poss (ss!i)" by simp_all
          ultimately show ?thesis 
            using linear_term_unique_vars by (metis True ‹i = j› r1' r1r2 r2')
        next
          case False
          with p1 q1 have "p1 ⊥ q1" 
            unfolding True using var_poss_parallel by (smt (verit, ccfv_threshold) subterm_poss_conv var_poss_iff) 
          then have "p1 @ p2 ≠ q1 @ q2"
            by (metis less_eq_pos_simps(1) pos_less_eq_append_not_parallel) 
          moreover have "linear_term (ss!i)" 
            using lin_s i nth_mem by blast
          ultimately show ?thesis 
            using p1 p2 q1 q2 linear_term_unique_vars True by fastforce
        qed
      next
        case False
        with x x2 show ?thesis 
          using disj(2) i j by (meson disjoint_iff_not_equal linorder_neqE_nat)  
      qed
    qed 
  qed
  }
  then show ?thesis using distinct_vars_linear_term Proof_Term_Utils.distinct_vars by metis
qed

end

context ren_wf_trs
begin

(*Helper lemma*)
lemma source_subst_renamed_lhs:
  assumes rdp:"(α, p) ∈ set (redex_patterns A)" and A_wf:"A ∈ wf_pterm R"
    and "lhs' = map_vars_term (rename_many' ren n) (lhs α)" 
    and sigma_vars:"∀i < length (var_poss_list lhs'). σ (vars_term_list lhs'!i) = (source A)|_(p@(var_poss_list lhs'!i))" 
  shows "lhs' ⋅ σ = (source A)|_p" 
proof-
  let ?xs="map source (map (to_pterm ∘ (λpi. (source A) |_ (p @ pi))) (var_poss_list (lhs α)))"
  let ?R="{}"
  have ll:"left_lin ?R"
    by (simp add: left_lin.intro left_linear_trs_def)
  from rdp have "to_rule α ∈ R" 
    using A_wf by (metis labeled_source_to_term labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs poss_term_lab_to_term) 
  then have lin:"linear_term (lhs α)"
    using R.left_lin using left_linear_trs_def by fastforce
  from rdp A_wf have p:"p ∈ poss (source A)"
    using left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs by blast
  have "source (ll_single_redex (source A) p α) = source A"
    using A_wf rdp using left_lin_wf_trs.source_single_step R.left_lin_wf_trs_axioms by auto
  then have "(lhs α) ⋅ ⟨?xs⟩⇩α  = (source A)|_p" 
    unfolding ll_single_redex_def using left_lin.source_ctxt_apply_term[OF ll] replace_at_subt_at[OF p] 
    by (smt (verit) p p_in_poss_to_pterm source.simps(3) source_ctxt_to_pterm to_pterm_trs_ctxt) 
  then have "lhs' ⋅ (mk_subst Var (zip (vars_distinct lhs') ?xs)) = (source A)|_p"
    using mk_subst_rename renameN(3) by (metis (mono_tags, lifting) assms(3) lin length_map length_var_poss_list linear_term_var_vars_term_list)  
  with sigma_vars show ?thesis using substitution_subterm_at
    by (metis length_var_poss_list p subt_at_append)
qed

end

locale overlapping_part = ren_wf_trs +
  fixes rdp_A A B s As α1 p1 β q
  assumes A_wf:"A ∈ wf_pterm R" 
    and rdp_A:"rdp_A = filter (λ(α, p). measure_ov (ll_single_redex s p α)  B ≠ 0) (redex_patterns A)" 
    and As:"As = map (λ(α, p). ll_single_redex s p α) rdp_A" 
    and α1p1:"(α1, p1) = hd rdp_A" 
    and not_empty:"rdp_A ≠ []"
    and s:"source A = s" "source B = s"
    and B:"B = ll_single_redex s q β" and q:"q ∈ poss s" and β:"to_rule β ∈ S"
begin
abbreviation "Δ1 ≡ ll_single_redex s p1 α1"

definition "renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A)"
definition "renamed_lhs_α1 = map_vars_term (rename_many' ren 0) (lhs α1)"
definition "renamed_lhs_β = map_vars_term (ren_l ren) (lhs β)" 
definition "p = (if q <⇩p p1 then q else p1)"
definition "l = replace_at renamed_lhs_α1 (pos_diff q p) renamed_lhs_β"
definition "ss = (renamed_lhs_α1 |_ (pos_diff q p)) # (tl renamed_lhs_αs)"
definition "ps = (pos_diff p1 p) # (map (λpi. pos_diff pi q) (map snd (tl rdp_A)))" 
definition "τ = tau.τ ss renamed_lhs_β ps"
definition "τs = tau.τs ss renamed_lhs_β ps" 
definition "σ_vars = concat (map vars_term_list renamed_lhs_αs) @ vars_term_list renamed_lhs_β"
definition "σ_terms = concat (map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A)) 
                     @ (map ((|_) (s |_ q)) (var_poss_list renamed_lhs_β))"
definition "σ = mk_subst Var (zip σ_vars σ_terms)"
definition "B' = replace_at (to_pterm (l ⋅ τ)) (pos_diff q p) (Prule β (map (to_pterm ∘ τ) (vars_term_list renamed_lhs_β)))"
definition "As' = map (λ((αi, pi), i). replace_at (to_pterm (l ⋅ τ)) (pos_diff pi p) (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))))) (zip rdp_A [0..<length rdp_A])" 

lemma length_renamed_lhs_αs: "length renamed_lhs_αs = length rdp_A" 
  unfolding renamed_lhs_αs_def rename_list_def by simp

lemma length_rdp_A:"length rdp_A = length As"
  by (simp add: As) 

lemma As_i_wf:
  assumes "Ai ∈ set As" 
  shows "Ai ∈ wf_pterm R"
proof-
  from assms obtain α p where "(α, p) ∈ set (redex_patterns A)" and "Ai = ll_single_redex s p α"
    unfolding As rdp_A by force
  then have "Ai ∈ set (single_steps A)"
    using s(1) by auto 
  with A_wf show ?thesis
    using R.single_step_wf by blast 
qed

lemma rdp_A_subs_A:"set rdp_A ⊆ set (redex_patterns A)"
  unfolding rdp_A by simp

lemma sorted_rdp_A:"sorted_wrt (ord.lexordp (<)) (map snd rdp_A)" 
proof-
  have "sorted_wrt (ord.lexordp (<)) (map snd (redex_patterns A))"
    using left_lin_no_var_lhs.redex_patterns_sorted[OF R.ll_no_var_lhs A_wf] by simp
  then show ?thesis 
    unfolding rdp_A using sorted_wrt_filter sorted_wrt_map by blast 
qed

lemma order_rdp_A: 
  assumes "i < j" and "j < length rdp_A" 
    and "rdp_A ! i = (αi, pi)" and "rdp_A ! j = (αj, pj)" 
  shows "¬ pj ≤⇩p pi" 
proof-
  from sorted_rdp_A have "(ord.lexordp (<)) pi pj " 
    using assms sorted_wrt_nth_less by fastforce 
  then show ?thesis
    by (metis prefix_def lexord_linorder.less_le_not_le ord.lexordp_eq_pref)     
qed

lemma As'_not_empty: "As' ≠ []" 
  unfolding As'_def using not_empty by simp

lemma α1p1_in_rdpA: "(α1, p1) ∈ set rdp_A"
  by (simp add: α1p1 not_empty) 

lemma Δ1: "Δ1 ∈ set (single_steps A)"
  using α1p1_in_rdpA rdp_A_subs_A s(1) by fastforce

lemma pi_poss:
  assumes rdp_i:"(αi, pi) ∈ set rdp_A"
  shows "pi ∈ poss s"
  using A_wf left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs rdp_A_subs_A rdp_i s(1) by blast

lemma αi_in_R:
  assumes rdp_i:"(αi, pi) ∈ set rdp_A"
  shows "to_rule αi ∈ R"
  using A_wf labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs rdp_A_subs_A rdp_i by fastforce 

lemma overlap:
  assumes rdp_i:"(αi, pi) ∈ set rdp_A"
    and Δ:"Δ = ll_single_redex s pi αi" 
  shows "measure_ov Δ B ≠ 0"
  using Δ rdp_A rdp_i by auto 

lemma overlap_Δ1:"measure_ov Δ1 B ≠ 0"
  using α1p1_in_rdpA overlap by blast

lemma pq:"q <⇩p p1 ∨ p1 ≤⇩p q" 
proof-
  from overlap_Δ1 obtain r where r:"r ∈ possL Δ1" "r ∈ possL B"
    by (metis card.empty disjoint_iff) 
  from r(1) obtain r1 where r1:"r = p1 @ r1" 
    using R.single_redex_possL α1p1_in_rdpA αi_in_R pi_poss by auto 
  from r(2) obtain r2 where r2:"r = q @ r2" 
    using S.single_redex_possL[OF β] using B q by auto 
  from r1 r2 show ?thesis
    by (metis less_eq_pos_simps(1) pos_cases pos_less_eq_append_not_parallel)
qed

lemma pq_pos_diff:"p @ pos_diff q p = q"
  using p_def pq by fastforce

lemma p_poss:"p ∈ poss s" 
  unfolding p_def using q α1p1_in_rdpA pi_poss by(cases "q <⇩p p1") auto

lemma diff_q_p_poss_α1: "pos_diff q p ∈ poss (lhs α1)" 
proof(cases "q <⇩p p1")
  case True
  then show ?thesis 
    by (metis (mono_tags, lifting) append_self_conv empty_pos_in_poss p_def pq_pos_diff)
next
  case False
  then have le:"p1 ≤⇩p q" using pq by auto 
  moreover have "possL Δ1 = {p1 @ r |r. r ∈ fun_poss (lhs α1)}" 
    using R.single_redex_possL α1p1_in_rdpA pi_poss αi_in_R by auto 
  moreover have "possL B = {q @ r |r. r ∈ fun_poss (lhs β)}"
    using S.single_redex_possL B β q by auto 
  ultimately obtain r1 r2 where "r1 ∈ fun_poss (lhs α1)" "r2 ∈ fun_poss (lhs β)" "p1@r1 = q@r2"
    using overlap_Δ1 by (smt (verit, best) card.empty disjoint_iff mem_Collect_eq) 
  with le show ?thesis
    by (metis False append.assoc fun_poss_imp_poss p_def poss_append_poss pq_pos_diff same_append_eq)
qed

lemma diff_q_p_poss_renamed_α1: "pos_diff q p ∈ poss renamed_lhs_α1"  
  using diff_q_p_poss_α1 unfolding renamed_lhs_α1_def by simp

lemma diff_q_p_poss_l: "pos_diff q p ∈ poss (to_pterm l)"
proof-
  have "pos_diff q p ∈ poss renamed_lhs_α1" 
    using diff_q_p_poss_α1 unfolding renamed_lhs_α1_def by simp
  then show ?thesis  
    unfolding l_def using p_in_poss_to_pterm by (metis (mono_tags, lifting) hole_pos_ctxt_of_pos_term hole_pos_poss) 
qed

lemma lin_lhs_αi:
  assumes i:"i < length rdp_A" 
  shows "linear_term (lhs (fst (rdp_A!i)))"
proof-
  from i obtain αi pi where rdp:"rdp_A ! i = (αi, pi)" by force 
  with i have "to_rule αi ∈ R"
    by (metis αi_in_R nth_mem) 
  then have lin:"linear_term (lhs αi)"
    using R.left_lin left_linear_trs_def by fastforce 
  with i rdp show ?thesis by simp
qed

lemma renamed_lhs_αi:
  assumes i:"i < length rdp_A"
  shows "renamed_lhs_αs!i = map_vars_term (rename_many' ren i) (lhs (fst (rdp_A!i)))" 
proof-
  from i have "zip [0..<length rdp_A] (map (λ(α, p). lhs α) (map (λ(α, p'). (α, p')) rdp_A)) ! i = (i, lhs (fst (rdp_A!i)))" 
    using split_beta by simp
  with i show ?thesis
    unfolding renamed_lhs_αs_def rename_list_def by simp
qed

lemma lin_renamed_lhs_αi:
  assumes "lhs_αi ∈ set renamed_lhs_αs"
  shows "linear_term lhs_αi" 
  using lin_lhs_αi renameN(3) renamed_lhs_αi linear_term_map_inj_on_linear_term length_renamed_lhs_αs
  by (smt (verit, best) all_nth_imp_all_set assms inj_on_def the_inv_f_f) 

lemma ren_lhs_α1_alt:"renamed_lhs_α1 = hd renamed_lhs_αs"
  by (metis α1p1 fst_eqD hd_conv_nth length_greater_0_conv length_renamed_lhs_αs not_empty renamed_lhs_α1_def renamed_lhs_αi) 

lemma lin_renamed_β: "linear_term renamed_lhs_β" 
proof-
  have "linear_term (lhs β)" 
    using β S.left_lin left_linear_trs_def by fastforce
  then show ?thesis
    unfolding renamed_lhs_β_def using Mgu_generic.renameN(4) linear_term_map_inj_on_linear_term inj_on_subset by blast
qed
  
lemma linear_l: "linear_term l"proof-
  have lin1:"linear_term renamed_lhs_α1"
    by (metis hd_in_set length_0_conv length_renamed_lhs_αs lin_renamed_lhs_αi not_empty ren_lhs_α1_alt) 
  have "vars_term renamed_lhs_α1 ∩ vars_term renamed_lhs_β = {}" 
    unfolding renamed_lhs_α1_def renamed_lhs_β_def
    using renameN(1) by (smt (verit, ccfv_threshold) disjoint_iff imageE rangeI term.set_map(2)) 
  then show ?thesis 
    unfolding l_def using linear_ctxt_of_pos_term[OF lin1 lin_renamed_β] using diff_q_p_poss_renamed_α1 by auto
qed

lemma pi_below_q:
  assumes i:"i < length rdp_A" "i > 0" 
    and αipi:"(αi, pi) = rdp_A ! i" 
  shows "q <⇩p pi"
proof-
  have α1:"to_rule α1 ∈ R"
    using α1p1_in_rdpA αi_in_R by blast 
  have αi:"to_rule αi ∈ R"
    by (metis αi_in_R αipi i(1) nth_mem) 
  have p1:"p1 ∈ poss s"
    by (metis α1p1_in_rdpA pi_poss)  
  have pi:"pi ∈ poss s"
    by (metis αipi i(1) nth_mem pi_poss)  
  have pos:"¬ pi ≤⇩p p1"
    using order_rdp_A i by (metis α1p1 αipi hd_conv_nth not_empty)
  have "measure_ov (ll_single_redex s pi αi) B ≠ 0"
    using αipi i(1) overlap by force 
  moreover have ai:"possL (ll_single_redex s pi αi) = {pi @ r |r. r ∈ fun_poss (lhs αi)}" 
    using R.single_redex_possL[OF αi pi] by simp
  moreover from S.single_redex_possL[OF β q] have b:"possL B = {q @ r |r. r ∈ fun_poss (lhs β)}" 
    unfolding B by simp
  ultimately consider "pi ≤⇩p q" | "q <⇩p pi"
    by (smt (verit, ccfv_SIG) card_eq_0_iff disjoint_iff less_eq_pos_simps(1) mem_Collect_eq prefix_order.less_le pos_append_cases)
  then show ?thesis proof(cases)
    case 1
    from R.single_redex_possL[OF α1 p1] have a1:"possL Δ1 = {p1 @ r |r. r ∈ fun_poss (lhs α1)}" by simp
    from pos consider (less) "p1 <⇩p pi" | (par) "p1 ⊥ pi"  
      using parallel_pos by force
    then show ?thesis proof(cases)
      case less
      with overlap_Δ1 a1 b 1 have q2:"q ∈ possL Δ1" 
        using p_def pq_pos_diff
        by (smt (verit, ccfv_threshold) append_assoc append_eq_append_conv fun_poss_append_poss' card_eq_0_iff 
            disjoint_iff mem_Collect_eq prefix_order.less_le prefix_pos_diff) 
      from i have Δi:"ll_single_redex s pi αi ∈ set (single_steps A)"
        using αipi rdp_A_subs_A s(1) by force
      have "measure_ov Δ1 (ll_single_redex s pi αi) = 0"
        using R.single_steps_measure[OF Δ1 Δi A_wf] less by (simp add: prefix_order.less_le p1 pi single_redex_neq)
      moreover from ai have "pi ∈ possL (ll_single_redex s pi αi)" proof-
        have "[] ∈ fun_poss (lhs αi)" 
          using αi R.no_var_lhs by fastforce 
        then show ?thesis using ai by simp
      qed
      ultimately have "pi ∉ possL Δ1"
        by (meson card_eq_0_iff disjoint_iff finite_Int finite_possL) 
      with 1 have "q ∉ possL Δ1" unfolding a1
        by (smt (z3) fun_poss_append_poss' less_eq_pos_simps(1) mem_Collect_eq pos pos_append_cases prefix_pos_diff)
      with q2 show ?thesis by simp
    next
      case par 
      then have False
        using 1 by (metis prefix_def prefix_order.dual_order.trans prefix_order.less_imp_le pos_less_eq_append_not_parallel pq) 
      then show ?thesis by simp
    qed
  qed simp
qed

section‹Properties for substitution τ›

lemma len_ss_ps: "length ss = length ps" 
  unfolding ss_def ps_def rename_list_def length_Cons length_tl length_map length_zip renamed_lhs_αs_def
  using not_empty Suc_diff_1 by simp

lemma ps_in_poss_ren_β:
  assumes "pi ∈ set ps" 
  shows "pi ∈ poss renamed_lhs_β" 
proof-
  from assms obtain i where i:"i < length ps" and pi:"ps!i = pi"
    by (metis in_set_idx) 
  then show ?thesis proof(cases i)
    case 0
    have "(pos_diff p1 p) ∈ poss renamed_lhs_β" proof(cases "q <⇩p p1")
      case False
      then show ?thesis
        unfolding p_def by (metis empty_pos_in_poss prefix_order.order_refl prefix_pos_diff self_append_conv) 
    next
      case True
      moreover have "possL Δ1 = {p1 @ r |r. r ∈ fun_poss (lhs α1)}" 
        using R.single_redex_possL using α1p1_in_rdpA αi_in_R pi_poss by force
      moreover have "possL B = {q @ r |r. r ∈ fun_poss (lhs β)}"
        using S.single_redex_possL B β q by auto 
      ultimately obtain r1 r2 where "r1 ∈ fun_poss (lhs α1)" "r2 ∈ fun_poss (lhs β)" "p1@r1 = q@r2"
        using overlap_Δ1 by (smt (verit, best) card.empty disjoint_iff mem_Collect_eq) 
      with True show ?thesis
        unfolding p_def by (metis (mono_tags) fun_poss_imp_poss less_eq_pos_simps(1) less_eq_pos_simps(2) 
        prefix_order.less_le_not_le poss_append_poss poss_map_vars_term prefix_pos_diff renamed_lhs_β_def)
    qed
    then show ?thesis
      using "0" pi ps_def by fastforce 
  next
    case (Suc n)
    let ?pi="snd (rdp_A ! i)"
    let ?αi="fst (rdp_A ! i)"
    let ?Δi="ll_single_redex s ?pi ?αi"
    have αipi:"(?αi, ?pi) ∈ set rdp_A"
      using i not_empty ps_def by auto
    from i have pi:"ps!i = pos_diff ?pi q" 
      unfolding Suc ps_def by (simp add: nth_tl)
    have "possL ?Δi = {?pi @ r |r. r ∈ fun_poss (lhs ?αi)}" 
      using R.single_redex_possL αipi αi_in_R pi_poss by blast
    moreover have "possL B = {q @ r |r. r ∈ fun_poss (lhs β)}"
      using S.single_redex_possL B β q by auto 
    moreover have "measure_ov ?Δi B ≠ 0"
      using αipi overlap by blast 
    ultimately obtain r1 r2 where "r1 ∈ fun_poss (lhs ?αi)" "r2 ∈ fun_poss (lhs β)" "?pi@r1 = q@r2"
      by (smt (verit, best) card.empty disjoint_iff mem_Collect_eq) 
    moreover have "q <⇩p ?pi" 
      using pi_below_q by (metis Suc bot_nat_0.not_eq_extremum hd_Cons_tl i length_map length_nth_simps(2) 
          lessI less_nat_zero_code prod.collapse ps_def not_empty)
    ultimately have "pos_diff ?pi q ∈ poss renamed_lhs_β"
      by (metis ctxt_supt_id fun_poss_imp_poss less_eq_pos_simps(1) less_eq_pos_simps(2) prefix_order.dual_order.strict_implies_order 
          poss_map_vars_term prefix_pos_diff renamed_lhs_β_def replace_at_below_poss)    
    then show ?thesis using pi ‹ps!i = pi› by simp
  qed 
qed

lemma vars_term_disjoint:
  assumes "ss_i ∈ set ss"
  shows "vars_term ss_i ∩ vars_term renamed_lhs_β = {}"
proof-
  from assms obtain i where i:"i < length ss" and ss_i:"ss!i = ss_i"
    by (metis in_set_idx)
  show ?thesis proof(cases i)
    case 0
    then have *:"ss_i = renamed_lhs_α1 |_ (pos_diff q p)" 
      unfolding ss_def ss_i[symmetric] by simp
    have "vars_term renamed_lhs_α1 ∩ vars_term renamed_lhs_β = {}" 
      unfolding renamed_lhs_α1_def renamed_lhs_β_def using renameN(1)
      by (smt (verit) disjoint_iff imageE rangeI term.set_map(2)) 
    then show ?thesis 
      unfolding * using vars_term_subt_at[OF diff_q_p_poss_renamed_α1] by blast
  next
    case (Suc n)
    then have "ss_i = renamed_lhs_αs!i"
      unfolding ss_i[symmetric] using i nth_tl ss_def by auto 
    then obtain u where "ss_i = map_vars_term (rename_many' ren i) u" 
      using renamed_lhs_αi i len_ss_ps length_renamed_lhs_αs by (simp add: not_empty ss_def) 
    then show ?thesis using renameN(1)
      by (smt (verit, best) disjoint_iff imageE rangeI renamed_lhs_β_def term.set_map(2))
  qed
qed

lemma vars_term_disjoint_ss:
  assumes i:"i < j" and j:"j < length ss"
  shows "vars_term (ss!i) ∩ vars_term (ss!j) = {}"
proof-
  from i j have "ss!j = renamed_lhs_αs!j"
    unfolding ss_def by (metis hd_Cons_tl length_0_conv length_renamed_lhs_αs less_imp_Suc_add nth_Cons_Suc not_empty) 
  then obtain u where u:"ss!j = map_vars_term (rename_many' ren j) u" 
    unfolding ss_def using renamed_lhs_αi j len_ss_ps length_renamed_lhs_αs by (simp add: ps_def not_empty) 
  then show ?thesis proof(cases i)
    case 0
    then have *:"ss!i = renamed_lhs_α1 |_ (pos_diff q p)" 
      unfolding ss_def by simp
    have "vars_term renamed_lhs_α1 ∩ vars_term (ss!j) = {}" 
      unfolding u unfolding renamed_lhs_α1_def using renameN(2)[of i j] using i unfolding 0 by (simp add: rename_many_disj)
    then show ?thesis 
      unfolding * using vars_term_subt_at[OF diff_q_p_poss_renamed_α1] by blast
  next
    case (Suc n)
    then have "ss!i = renamed_lhs_αs!i"
      unfolding ss_def by (metis hd_Cons_tl length_0_conv length_nth_simps(4) length_renamed_lhs_αs not_empty) 
    then obtain u' where u':"ss!i = map_vars_term (rename_many' ren i) u'" 
      using renamed_lhs_αi i j len_ss_ps length_renamed_lhs_αs by (simp add: ss_def)
    from i show ?thesis
      unfolding u u' using renameN(2) by (simp add: rename_many_disj)
  qed
qed

lemma tau:"tau ss renamed_lhs_β ps"
proof-
  have lin_ss:"∀s∈set ss. linear_term s" 
    unfolding ss_def using lin_renamed_lhs_αi diff_q_p_poss_renamed_α1
    by (metis hd_Cons_tl hd_in_set length_0_conv length_renamed_lhs_αs list.set_intros(2) not_empty ren_lhs_α1_alt set_ConsD subt_at_linear) 
  show ?thesis
    using tau.intro[OF len_ss_ps lin_renamed_β lin_ss] ps_in_poss_ren_β lin_renamed_lhs_αi vars_term_disjoint_ss vars_term_disjoint by simp
qed

lemma renamed_lhs_α1_τ:
  assumes x:"x ∈ vars_ctxt (ctxt_of_pos_term (pos_diff q p) renamed_lhs_α1)"
  shows "τ x = Var x" 
proof-
  {fix i assume i:"i < length ss"
    have "x ∉ vars_term (ss!i)" proof(cases i)
      case 0
      have "linear_term renamed_lhs_α1"
        using lin_renamed_lhs_αi ren_lhs_α1_alt by (metis hd_in_set length_0_conv length_renamed_lhs_αs not_empty) 
      with x show ?thesis unfolding 0 nth_Cons_0
        using diff_q_p_poss_renamed_α1 linear_term_ctxt ss_def by fastforce
    next
      case (Suc n)
      from x have "x ∈ vars_term renamed_lhs_α1"
        using diff_q_p_poss_renamed_α1 by (simp add: vars_ctxt_pos_term)
      then show ?thesis using tau.disj(2)[OF tau] unfolding Suc
        by (metis Int_iff Suc emptyE hd_Cons_tl i length_nth_simps(1) length_nth_simps(2) length_renamed_lhs_αs less_numeral_extra(3) 
            nth_Cons_Suc not_empty rename_many_disj renamed_lhs_α1_def renamed_lhs_αi ss_def zero_less_Suc) 
    qed
  }
  moreover have "x ∉ vars_term renamed_lhs_β"
    unfolding renamed_lhs_β_def using x by (metis ctxt_of_pos_term_hole_pos disjoint_iff hole_pos_poss 
        l_def linear_l linear_term_ctxt renamed_lhs_β_def replace_at_subt_at)
  ultimately show ?thesis
    using tau.apply_tau_var[OF tau] τ_def by presburger
qed

lemma l_τ:"l ⋅ τ = (ctxt_of_pos_term (pos_diff q p) renamed_lhs_α1)⟨renamed_lhs_β ⋅ τ⟩" 
proof- 
  have "ctxt_of_pos_term (pos_diff q p) renamed_lhs_α1 ⋅⇩c τ = ctxt_of_pos_term (pos_diff q p) renamed_lhs_α1"
    using ctxt_subst_eq ctxt_subst_id renamed_lhs_α1_τ by force
  then show ?thesis using l_def by auto 
qed

lemma linear_l_tau:"linear_term (l ⋅ τ)" 
proof-
 have lin_ren_lhs_β:"linear_term (renamed_lhs_β ⋅ τ)" 
    using tau.linear_term_t_tau[OF tau] τ_def by presburger
  have lin_α1:"linear_term renamed_lhs_α1"
    by (metis hd_in_set length_0_conv length_renamed_lhs_αs lin_renamed_lhs_αi not_empty ren_lhs_α1_alt) 
  {fix r1 r2 x assume r1:"r1 ∈ poss (l⋅τ)" "l ⋅ τ |_ r1 = Var x" "¬ pos_diff q p ≤⇩p r1"
      and r2:"r2 ∈ poss (l⋅τ)" "l ⋅ τ |_ r2 = Var x" "¬ pos_diff q p ≤⇩p r2"
      and r1r2:"r1 ≠ r2" 
    from r1 have par1:"pos_diff q p ⊥ r1"
      by (metis diff_q_p_poss_renamed_α1 l_τ less_pos_def' prefix_order.le_less pos_cases replace_at_below_poss var_pos_maximal) 
    then have 1:"l ⋅ τ |_ r1 = renamed_lhs_α1 |_ r1" 
      by (metis diff_q_p_poss_renamed_α1 l_τ parallel_poss_replace_at parallel_replace_at_subt_at r1(1)) 
    from r2 have par2:"pos_diff q p ⊥ r2"
      by (metis diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ less_pos_def' pos_cases var_pos_maximal) 
    then have 2:"l ⋅ τ |_ r2 = renamed_lhs_α1 |_ r2" 
      by (metis diff_q_p_poss_renamed_α1 l_τ parallel_poss_replace_at parallel_replace_at_subt_at r2(1)) 
    from 1 2 par1 par2 have False
      by (metis diff_q_p_poss_renamed_α1 l_τ lin_α1 linear_term_unique_vars parallel_poss_replace_at r1(1,2) r1r2 r2(1,2))
  } moreover 
  {fix r1 r2 x assume r1:"r1 ∈ poss (l⋅τ)" "l ⋅ τ |_ r1 = Var x" "pos_diff q p ≤⇩p r1"
                  and r2:"r2 ∈ poss (l⋅τ)" "l ⋅ τ |_ r2 = Var x" "¬ pos_diff q p ≤⇩p r2"
                  and r1r2:"r1 ≠ r2" 
    from r2 have par2:"pos_diff q p ⊥ r2"
      by (metis diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ less_pos_def' pos_cases var_pos_maximal) 
    then have r2_pos:"r2 ∈ poss renamed_lhs_α1"
      using diff_q_p_poss_renamed_α1 l_τ parallel_poss_replace_at r2(1) by auto 
    from par2 have 2:"l ⋅ τ |_ r2 = renamed_lhs_α1 |_ r2" 
      unfolding l_τ using parallel_replace_at_subt_at diff_q_p_poss_renamed_α1 l_τ parallel_poss_replace_at r2(1) by fastforce
    with r2(2) r2_pos have x:"x ∈ vars_term renamed_lhs_α1"
      by (simp add: vars_ctxt_pos_term)        
    from r1 obtain r1' where r1':"r1 = pos_diff q p @ r1'"
      using prefix_def by auto
    with r1(1) have r1'_pos:"r1' ∈ poss (renamed_lhs_β ⋅ τ)"
      by (simp add: diff_q_p_poss_renamed_α1 l_τ replace_at_subt_at) 
    have at_r1':"renamed_lhs_β ⋅ τ |_ r1' = Var x"
      by (metis diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ r1' r1(2) replace_at_subt_at subt_at_append) 
    have False proof(cases "r1' ∈ poss renamed_lhs_β ∧ renamed_lhs_β |_ r1' = Var x")
      case True
      with r1'_pos have "x ∈ vars_term renamed_lhs_β"
        by (metis subsetD term.set_intros(3) vars_term_subt_at)
      with x show ?thesis
        by (smt (verit, best) Mgu_generic.renameN(1) disjoint_iff imageE rangeI renamed_lhs_α1_def renamed_lhs_β_def term.set_map(2))
    next
      case False
      then obtain r11 r12 y where y:"renamed_lhs_β|_r11 = Var y" and r11:"r11 ∈ var_poss renamed_lhs_β" and r11r12:"r1' = r11 @ r12"
        by (smt (verit, best) at_r1' eval_term.simps(2) is_FunE poss_subst_choice r1'_pos subt_at_subst term.distinct(1) var_poss_iff)
      then have *:"renamed_lhs_β ⋅ τ |_ r1' = τ y |_ r12" 
        by (simp add: var_poss_iff) 
      from y r11 r11r12 False have "x ≠ y"
        by (metis "2" append_Nil2 diff_q_p_poss_renamed_α1 l_def par2 parallel_poss_replace_at parallel_replace_at_subt_at poss_append_poss r1'_pos r2(2) 
            r2_pos subt_at_subst var_pos_maximal var_poss_imp_poss)
      then have "τ y ≠ Var y" 
        using y r11 r1(1,2) False at_r1' r1'_pos r11r12 var_poss_iff by fastforce
      then obtain i r' where i:"i < length ss" "ps ! i @ r' = r11" and r':"r' ∈ poss (ss ! i)" and τy:"τ y = ss ! i |_ r'" 
        using tau.apply_tau_t_var'[OF tau r11 y] τ_def by auto
      with * have **:"ss ! i |_ r' |_ r12 = Var x"
        using at_r1' by presburger 
      with i r' τy * have x2:"x ∈ vars_term (ss!i)"
        by (smt (verit, ccfv_SIG) eval_term.simps(1) pos_append_poss r1'_pos r11 r11r12 subt_at_subst subterm_poss_conv var_poss_iff vars_term_var_poss_iff y)
      then show ?thesis proof(cases i)
        case 0      
        with x x2 2 show ?thesis
          using diff_q_p_poss_renamed_α1 lin_α1 linear_subterms_disjoint_vars par2 r2(2) r2_pos ss_def by fastforce
      next
        case (Suc n)
        have "vars_term (ss!i) ∩ vars_term renamed_lhs_α1 = {}"
          by (metis Suc Zero_neq_Suc hd_Cons_tl i(1) length_0_conv length_nth_simps(2) length_renamed_lhs_αs nth_Cons_Suc not_empty rename_many_disj renamed_lhs_α1_def renamed_lhs_αi ss_def) 
        with x x2 show ?thesis by blast
      qed
    qed
  } moreover 
  {fix r1 r2 x assume r1:"r1 ∈ poss (l⋅τ)" "l ⋅ τ |_ r1 = Var x" "pos_diff q p ≤⇩p r1"
                  and r2:"r2 ∈ poss (l⋅τ)" "l ⋅ τ |_ r2 = Var x" "pos_diff q p ≤⇩p r2"
                  and r1r2:"r1 ≠ r2" 
    from r1 obtain r1' where r1':"r1 = pos_diff q p @ r1'"
      using prefix_def by auto
    with r1(1) have r1'_pos:"r1' ∈ poss (renamed_lhs_β ⋅ τ)"
      by (simp add: diff_q_p_poss_renamed_α1 l_τ replace_at_subt_at)
    have at_r1':"renamed_lhs_β ⋅ τ |_ r1' = Var x"
      by (metis diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ r1' r1(2) replace_at_subt_at subt_at_append) 
    from r2 obtain r2' where r2':"r2 = pos_diff q p @ r2'"
      using prefix_def by auto
    with r2(1) have r2'_pos:"r2' ∈ poss (renamed_lhs_β ⋅ τ)"
      by (simp add: diff_q_p_poss_renamed_α1 l_τ replace_at_subt_at)
    have at_r2':"renamed_lhs_β ⋅ τ |_ r2' = Var x"
      by (metis diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ r2' r2(2) replace_at_subt_at subt_at_append) 
    have r1'r2':"r1' ≠ r2'" 
      using r1r2 r1' r2' by auto
    have False using lin_ren_lhs_β
      by (meson at_r1' at_r2' linear_term_unique_vars r1'_pos r1'r2' r2'_pos)   
  }
  ultimately show ?thesis
    using distinct_vars_linear_term Proof_Term_Utils.distinct_vars by metis
qed

section‹Substitution σ maps to subterms of s›

lemma distinct_vars_renamed_lhs_α:
  "distinct (concat (map vars_term_list renamed_lhs_αs))"
  using distinct_linear_renamed_vars
  by (metis (mono_tags, lifting) in_set_conv_nth length_map lin_lhs_αi map_nth_eq_conv renamed_lhs_αs_def split_beta) 

lemma distinct_vars_ren_β: "distinct (vars_term_list renamed_lhs_β)"
  using lin_renamed_β by (simp add: linear_term_distinct_vars)

lemma distinct_σ_vars: "distinct σ_vars"
  unfolding σ_vars_def using distinct_vars_ren_β distinct_vars_renamed_lhs_α distinct_append
  by (metis ren.disjoint_concat_renamed_vars renamed_lhs_αs_def renamed_lhs_β_def)

lemma length_vars_term_list_i:
  assumes i:"i < length renamed_lhs_αs"
  shows "length (map vars_term_list renamed_lhs_αs!i) = length (map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A)!i)" 
proof-
  from i obtain u p' where *:"(rename_redex_patterns rdp_A) ! i = (u, p')"
    by fastforce 
  with i have "renamed_lhs_αs!i = u"
     unfolding renamed_lhs_αs_def rename_redex_patterns_eq_rename_list[symmetric] by simp
  moreover from * i have "map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A)!i = map ((|_) (s |_p' )) (var_poss_list u)"
    unfolding renamed_lhs_αs_def rename_list_def length_map rename_redex_patterns_def by fastforce 
  ultimately show ?thesis
    using length_var_poss_list by (metis (no_types, lifting) i length_map nth_map) 
qed

lemma σ_y:
  assumes j:"j < length (vars_term_list renamed_lhs_β)" 
    and yj:"yj = vars_term_list renamed_lhs_β ! j"
    and qj:"qj = var_poss_list renamed_lhs_β ! j"
  shows "σ yj = s|_(q@qj)" 
proof- 
  have length:"length (map vars_term_list renamed_lhs_αs) = length (map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A))"
    unfolding renamed_lhs_αs_def rename_list_def length_map rename_redex_patterns_def by simp
  with length_vars_term_list_i have length_concat_vars_terms:"length (concat (map vars_term_list renamed_lhs_αs)) = length (concat (map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A)))"
    unfolding renamed_lhs_αs_def length_concat by (smt (verit, ccfv_SIG) list.map_comp map_eq_imp_length_eq map_equality_iff map_nth nth_map)
  have zip_sigma_alt:"zip σ_vars σ_terms = zip (concat (map vars_term_list renamed_lhs_αs)) 
                         (concat (map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A))) 
                         @ (zip (vars_term_list renamed_lhs_β) (map ((|_) (s |_ q)) (var_poss_list renamed_lhs_β)))" 
    unfolding σ_vars_def σ_terms_def using zip_append[OF length_concat_vars_terms] by presburger 
  have "yj ∉ set (concat (map vars_term_list renamed_lhs_αs))" proof-
    {fix i assume "i < length renamed_lhs_αs"
      then obtain u where "renamed_lhs_αs!i = map_vars_term (rename_many' ren i) u" 
        using renamed_lhs_αi by (simp add: length_renamed_lhs_αs)
      then have "yj ∉ set (vars_term_list (renamed_lhs_αs!i))" 
        using renameN(1) by (smt (verit, del_insts) disjoint_iff image_iff j nth_mem rangeI renamed_lhs_β_def set_vars_term_list term.set_map(2) yj) 
    }
    then show ?thesis unfolding set_concat
      by (smt (verit, best) UN_iff in_set_conv_nth length_map nth_map) 
  qed
  then have *:"σ yj = mk_subst Var (zip (vars_term_list renamed_lhs_β) (map ((|_) (s |_ q)) (var_poss_list renamed_lhs_β))) yj"
    using mk_subst_concat unfolding σ_def zip_sigma_alt by (metis (no_types, lifting) length_concat_vars_terms map_fst_zip)
  show ?thesis 
    unfolding * using mk_subst_distinct[OF distinct_vars_ren_β j]
    by (smt (verit, ccfv_SIG) j length_map length_var_poss_list nth_map q qj subt_at_append yj)
qed

lemma ren_lhs_β_σ: "renamed_lhs_β ⋅ σ = s|_q"
proof-
  let ?ys="map source (map (to_pterm ∘ (λpi. s |_ (q @ pi))) (var_poss_list (lhs β)))"
  have length:"length (var_rule β) = length (var_poss_list (lhs β))"
    by (metis β length_var_poss_list S.length_var_rule) 
  have "(lhs β) ⋅ ⟨?ys⟩⇩β  = s|_q" 
    using B unfolding ll_single_redex_def using R.source_ctxt_apply_term
    by (metis (no_types, lifting) p_in_poss_to_pterm q replace_at_subt_at s(2) source.simps(3) source_ctxt_to_pterm to_pterm_trs_ctxt)
  then have "renamed_lhs_β ⋅ (mk_subst Var (zip (vars_distinct renamed_lhs_β) ?ys)) = s|_q"
    unfolding renamed_lhs_β_def using length mk_subst_rename[of "lhs β" ?ys] renameN(4) unfolding length_map by metis
  with σ_y show ?thesis using substitution_subterm_at
    by (metis (no_types, lifting) q subt_at_append)
qed

lemma σ_x:
  assumes i:"i < length renamed_lhs_αs"
    and αipi:"(αi, pi) = rdp_A ! i"
    and j:"j < length (vars_term_list (renamed_lhs_αs!i))"
    and xj:"xj = vars_term_list (renamed_lhs_αs!i) ! j"
    and pj:"pj = var_poss_list (renamed_lhs_αs!i) ! j"
  shows "σ xj = s|_(pi@pj)"
proof- 
  have length:"length (map vars_term_list renamed_lhs_αs) = length (map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A))"
    unfolding renamed_lhs_αs_def rename_list_def length_map rename_redex_patterns_def by simp
  from j have j2:"j < length (var_poss_list (renamed_lhs_αs!i))"
    by (simp add: length_var_poss_list) 
  let ?x_vars="map vars_term_list renamed_lhs_αs"
  let ?x_terms="(map (λ(lhs_αi, pi). (map ((|_) (s |_pi )) (var_poss_list lhs_αi))) (rename_redex_patterns rdp_A))"
  have l_x:"length ?x_vars = length ?x_terms" 
    unfolding renamed_lhs_αs_def length_map rename_list_def rename_redex_patterns_def by simp
  {fix k assume "k < length rdp_A" 
    then have "length (?x_vars!k) = length (?x_terms!k)"
      using length_vars_term_list_i length_renamed_lhs_αs by presburger
  }note length_x_at_i=this
  with l_x have x_map_length:"map length ?x_vars = map length ?x_terms" 
    using list_eq_iff_nth_eq by (smt (verit, best) length_map length_vars_term_list_i nth_map) 
  then have x_map_length_i:"map length (take i ?x_vars) = map length (take i ?x_terms)"
    by (metis take_map) 
  let ?k="sum_list (map length (take i ?x_vars)) + j"
  have k2:"?k = sum_list (map length (take i ?x_terms)) + j" 
    using x_map_length_i by simp
  from i j have k_less:"?k < length (concat ?x_vars)"
    by (simp add: concat_nth_length) 
  moreover from i j have "concat ?x_vars ! ?k = xj" 
    by (simp add: concat_nth xj) 
  ultimately have 1:"σ_vars ! ?k = xj" 
    unfolding nth_append σ_vars_def by presburger 
  from k_less x_map_length have k_less2:"?k < length (concat ?x_terms)"
    by (simp add: length_concat)
  moreover have "concat ?x_terms ! ?k = s|_(pi@pj)" proof-
    have concat_k:"concat ?x_terms ! ?k = ?x_terms ! i ! j" 
      using j length_x_at_i concat_nth unfolding k2
      by (metis (no_types, lifting) i length length_vars_term_list_i list.map_comp map_equality_iff nth_map) 
    have i3:"i < length (rename_redex_patterns rdp_A)" 
      unfolding rename_redex_patterns_def length_map length_zip using i length_renamed_lhs_αs by auto 
    from i3 have "rename_redex_patterns rdp_A ! i = (map fst (rename_redex_patterns rdp_A) ! i, map snd (rename_redex_patterns rdp_A) ! i)"
      by simp 
    moreover have "map snd (rename_redex_patterns rdp_A) ! i = pi"
      unfolding nth_map[OF i3] unfolding rename_redex_patterns_def using αipi i unfolding length_renamed_lhs_αs
      by (metis (no_types, lifting) case_prod_conv length_map length_zip map_nth min.idem nth_map nth_zip old.prod.inject prod.collapse)
    ultimately have "rename_redex_patterns rdp_A ! i = (renamed_lhs_αs!i, pi)"
      unfolding rename_redex_patterns_eq_rename_list renamed_lhs_αs_def by simp
    then have at_i:"?x_terms ! i = map ((|_) (s |_ pi)) (var_poss_list (renamed_lhs_αs!i))" 
      unfolding nth_map[OF i3] by simp  
    show ?thesis 
      unfolding concat_k at_i nth_map[OF j2] by (metis αipi i length_renamed_lhs_αs nth_mem pi_poss pj subt_at_append)
  qed
  ultimately have 2:"σ_terms ! ?k = s|_(pi@pj)" 
    unfolding nth_append by (simp add: σ_terms_def nth_append)
  show ?thesis
    by (metis "1" "2" σ_def σ_terms_def σ_vars_def distinct_σ_vars k_less k_less2 length_append mk_subst_distinct trans_less_add1)
qed

lemma renamed_lhs_αi_σ:
  assumes i:"i < length renamed_lhs_αs"
    and pi:"pi = snd (rdp_A ! i)"
  shows "renamed_lhs_αs!i ⋅ σ = s|_pi"
proof-
  let ?αi="fst (rdp_A ! i)" 
  from i pi have elem:"(?αi, pi) ∈ set (redex_patterns A)"
    using length_renamed_lhs_αs rdp_A_subs_A by auto
  from i have "zip [0..<length rdp_A] (map (λ(α, p). lhs α) rdp_A) ! i = (i, lhs ?αi)" 
    unfolding renamed_lhs_αs_def rename_list_def length_zip length_map using nth_zip by (simp add: split_beta) 
  then have ren_i:"renamed_lhs_αs!i = map_vars_term (rename_many' ren i) (lhs ?αi)" 
    unfolding renamed_lhs_αs_def rename_list_def using i length_renamed_lhs_αs by auto
  show ?thesis
    using source_subst_renamed_lhs[OF elem A_wf ren_i] σ_x[OF i]
    by (simp add: length_var_poss_list pi s(1) split_pairs)
qed

section‹Composition of σ after τ maps to subterms of s›
(*The slightly awkward introduction of τ' is necessary, because later we want to be able to use 
this lemma for lemma σ_τ_x. A variable x of lhs(α⇩i) is first mapped to some subterm of lhs(β) by 
some component τ⇩j of τ. Then the remaining τ⇩j⇩+⇩1 ⋯ τ⇩n (hence the ‹τ' = compose (drop …›)  
map every variable of that subterm of lhs(β) to appropriate subterms of s.*)
lemma σ_τ'_y:
  assumes i:"i ≤ length ss"
    and τ':"τ' = compose (drop i (map2 (λx y. linear_unifier x (renamed_lhs_β |_ y)) ss ps))"
    and j:"j < length (vars_term_list renamed_lhs_β)" 
    and yj:"yj = vars_term_list renamed_lhs_β ! j" and qj:"qj = var_poss_list renamed_lhs_β ! j" 
  shows "(τ' ∘⇩s σ) yj = s|_(q@qj)"
proof-
  consider "τ' yj = Var yj" | "(∃i r'. i < length ss ∧ r' ∈ poss (ss ! i) ∧ ps ! i @ r' = qj ∧ τ' yj = ss ! i |_ r')"
   using tau.apply_tau_t_var[OF tau τ' i] by (metis j length_var_poss_list nth_mem qj var_poss_list_sound vars_term_list_var_poss_list yj) 
  then show ?thesis proof(cases)
    case 1
    then show ?thesis 
      using j σ_y qj yj by (simp add: subst_compose)
  next
    case 2
    then obtain i r where i:"i < length ss" and r:"r ∈ poss (ss ! i)" "ps ! i @ r = qj" "τ' yj = ss ! i |_ r" 
      by blast
    then have i2:"i < length rdp_A"
      by (simp add: length_renamed_lhs_αs not_empty ss_def) 
    show ?thesis proof(cases i)
      case 0
      then have pi:"ps!i = pos_diff p1 p"
        unfolding ps_def by auto
      have "renamed_lhs_α1 ⋅ σ = s |_ p1 "
        by (metis "0" α1p1 hd_conv_nth i2 length_0_conv length_renamed_lhs_αs not_empty ren_lhs_α1_alt renamed_lhs_αi_σ snd_conv) 
      then have "ss ! i ⋅ σ = s |_ p1 |_ (pos_diff q p)" 
        unfolding 0 by (metis diff_q_p_poss_renamed_α1 nth_Cons_0 ss_def subt_at_subst)
      then have "(τ' yj) ⋅ σ = s |_ p1 |_ (pos_diff q p) |_ r" 
        unfolding r(3) by (metis r(1) subt_at_subst) 
      then show ?thesis
        by (smt (verit, best) α1p1_in_rdpA append_eq_appendI append_self_conv prefix_order.eq_refl prefix_order.less_imp_le 
        overlapping_part.pi_poss overlapping_part_axioms p_def pi pq_pos_diff prefix_pos_diff q r(2) subst_compose_def subt_at_append)
    next
      case (Suc n)
      then have "ps!i = map (λpi. pos_diff pi q) (map snd (tl rdp_A)) ! n"
        using ps_def by force
      with i have "ps!i = map (λpi. pos_diff pi q) (map snd rdp_A) ! i"
        by (metis Suc hd_Cons_tl map_is_Nil_conv map_tl nth_Cons_Suc not_empty)
      with i have "ps!i = pos_diff (map snd rdp_A ! i) q"
        using i2 by auto
      moreover have "q ≤⇩p (map snd rdp_A ! i)" 
        using pi_below_q[OF i2] Suc i2 by (metis nth_map prefix_order.less_le prod.collapse zero_less_Suc)
      ultimately have pi:"q @ (ps!i) = (map snd rdp_A ! i)"
        using prefix_pos_diff by metis
      have "ss!i = renamed_lhs_αs!i "
        using Suc i nth_tl ss_def by auto
      then have "ss ! i ⋅ σ = s |_ ((map snd rdp_A) ! i)" 
        using renamed_lhs_αi_σ i2  by (simp add: length_renamed_lhs_αs)
      then have "(τ' yj) ⋅ σ = s |_ ((map snd rdp_A) ! i) |_ r" 
        unfolding r(3) by (metis r(1) subt_at_subst) 
      moreover have "((map snd rdp_A) ! i) @ r = q @ qj"
        using pi by (metis append_assoc r(2))
      ultimately show ?thesis
        by (metis i len_ss_ps nth_mem pi pos_append_poss poss_imp_subst_poss ps_in_poss_ren_β q ren_lhs_β_σ subst_compose subt_at_append)
    qed
  qed
qed

lemma renamed_lhs_β_τ'_σ:
  assumes i:"i ≤ length ss" 
    and τ':"τ' = compose (drop i (map2 (λx y. linear_unifier x (renamed_lhs_β |_ y)) ss ps))"
  shows "renamed_lhs_β ⋅ (τ' ∘⇩s σ) = s|_q" 
proof-
  let ?ys="map source (map (to_pterm ∘ (λpi. s |_ (q @ pi))) (var_poss_list (lhs β)))"
  have length:"length (var_rule β) = length (var_poss_list (lhs β))"
    by (metis β length_var_poss_list S.length_var_rule) 
  have "(lhs β) ⋅ ⟨?ys⟩⇩β  = s|_q" 
    using B unfolding ll_single_redex_def using S.source_ctxt_apply_term
    by (smt (verit, best) context_source q replace_at_subt_at s(2) source.simps(3) source_to_pterm to_pterm_ctxt_of_pos_apply_term)
  then have "renamed_lhs_β ⋅ (mk_subst Var (zip (vars_distinct renamed_lhs_β) ?ys)) = s|_q"
    using length mk_subst_rename[of "lhs β" ?ys] renameN(4) unfolding length_map renamed_lhs_β_def by metis
  with σ_τ'_y[OF i τ'] show ?thesis 
    using substitution_subterm_at by (metis q subt_at_append)
qed

lemma renamed_lhs_β_τ_σ:
  shows "renamed_lhs_β ⋅ (τ ∘⇩s σ) = s|_q" 
using renamed_lhs_β_τ'_σ[of 0] using τ_def tau tau.τ_def by force 

lemma σ_τ_x:
  assumes i:"i < length renamed_lhs_αs" 
    and j:"j < length (vars_term_list (renamed_lhs_αs!i))"
    and pi:"pi = snd (rdp_A ! i)" 
    and xj:"xj = vars_term_list (renamed_lhs_αs!i)!j"
    and pj:"pj = var_poss_list (renamed_lhs_αs!i)!j"
  shows "(τ ∘⇩s σ) xj = s|_(pi@pj)" 
proof- 
  let ?τ'="compose (drop (Suc i) (map2 (λx y. linear_unifier x (renamed_lhs_β |_ y)) ss ps))"
  from xj j have xj_vars_term:"xj ∈ vars_term (renamed_lhs_αs!i)"
    using nth_mem by fastforce 
  show ?thesis proof(cases i)
    case 0
    then have at_i:"renamed_lhs_αs ! i = renamed_lhs_α1"
      using hd_conv_nth i ren_lhs_α1_alt by force 
    from xj pj have x_at_pj:"renamed_lhs_α1 |_ pj = Var xj"
      using at_i j vars_term_list_var_poss_list by auto
    have lin_lhs_α1:"linear_term renamed_lhs_α1"
      using "0" i lin_renamed_lhs_αi ren_lhs_α1_alt by auto 
    from 0 have ss_i:"ss!i = renamed_lhs_α1 |_ (pos_diff q p)" 
      unfolding ss_def by simp
    show ?thesis proof(cases "pos_diff q p ≤⇩p pj")
      case True
      then obtain pj' where *:"(ss!i) |_ pj' = Var xj" "pj' ∈ poss (ss!i)" and pj':"pj = pos_diff q p @ pj'"
        unfolding ss_i using prefix_def x_at_pj
        by (metis at_i j length_var_poss_list nth_mem pj subterm_poss_conv var_poss_iff var_poss_list_sound)
      from * have 1:"xj ∈ vars_term (ss ! i)" 
        using vars_term_subt_at by fastforce 
      from * have 2:"pj' ∈ var_poss (ss ! i)"
        by (simp add: var_poss_iff) 
      consider "τ xj = Var xj" | "pj' ∈ poss (renamed_lhs_β |_ (ps!i)) ∧ τ xj = renamed_lhs_β |_ (ps!i) |_ pj' ⋅ ?τ'"
        using tau.apply_tau_ss_var[OF tau] * 0 1 2 τ_def ss_def by fastforce
      then show ?thesis proof(cases)
        case 1
        then show ?thesis unfolding xj using σ_x
          by (metis (mono_tags, lifting) "0" α1p1 eval_term.simps(1) hd_conv_nth i j pi pj not_empty snd_eqD subst_compose_def) 
      next
        case 2
        from renamed_lhs_β_τ'_σ have "renamed_lhs_β ⋅ (?τ' ∘⇩s σ) = s|_q"
          using Suc_le_eq 0 ss_def by simp 
        then have "renamed_lhs_β |_ (ps!i) |_ pj' ⋅ (?τ' ∘⇩s σ) = s|_q |_ (ps!i) |_ pj'"
          by (smt (verit, best) "0" "2" length_nth_simps(2) nth_mem ps_def ps_in_poss_ren_β subt_at_subst zero_less_Suc)
        with 2 have "(τ ∘⇩s σ) xj = s|_q |_ (ps!i) |_ pj'" 
          by (metis (mono_tags, lifting) subst_compose subst_subst_compose) 
        moreover have "q @ (ps!i) @ pj' = pi @ pj" proof-
          have "pi = p1"
            by (metis "0" α1p1 hd_conv_nth pi not_empty snd_conv)
          moreover have "q @ (pos_diff p1 p) = p1 @ (pos_diff q p)"
            by (metis prefix_order.dual_order.strict_implies_order prefix_order.order_refl p_def pq prefix_pos_diff self_append_conv)
          ultimately show ?thesis 
            unfolding pj' ps_def using "0" by auto 
        qed
        ultimately show ?thesis unfolding xj
          by (metis "0" α1p1_in_rdpA nth_Cons_0 prefix_order.dual_order.refl prefix_order.less_imp_le p_def pi_poss prefix_pos_diff ps_def q self_append_conv subt_at_append subterm_poss_conv)  
      qed
    next
      case False
      have x_not_in_b:"xj ∉ vars_term renamed_lhs_β" 
        using xj j unfolding at_i renamed_lhs_α1_def renamed_lhs_β_def
        by (metis (mono_tags, lifting) Mgu_generic.renameN(1) disjoint_iff imageE length_map nth_map rangeI term.set_map(2) vars_map_vars_term)  
      have "xj ∉ vars_term (ss!0)" 
        unfolding ss_def by (smt (verit, ccfv_SIG) "0" False at_i diff_q_p_poss_renamed_α1 j length_var_poss_list less_eq_pos_simps(1) lin_lhs_α1 
            linear_term_unique_vars nth_mem pj pos_append_poss ss_def ss_i subt_at_append var_poss_iff var_poss_list_sound vars_term_poss_subt_at x_at_pj) 
      moreover 
      {fix k assume k:"k < length ss" "k > 0" 
        have x:"xj ∈ vars_term renamed_lhs_α1"
          using at_i xj_vars_term by auto 
        obtain u where u:"ss!k = map_vars_term (rename_many' ren k) u"
          using k renamed_lhs_αi unfolding ss_def
          by (metis "0" Suc_diff_1 hd_Cons_tl i length_greater_0_conv length_nth_simps(2) length_renamed_lhs_αs nth_Cons_Suc) 
        from x have "xj ∉ vars_term (ss!k)"  
          unfolding u renamed_lhs_α1_def using k by (metis disjoint_iff not_gr_zero rename_many_disj) 
      }
      ultimately have "τ xj = Var xj" 
        using tau.apply_tau_var[OF tau] using x_not_in_b τ_def by auto
      then show ?thesis unfolding xj using σ_x[OF i]
        by (metis (no_types, lifting) "0" α1p1 eval_term.simps(1) hd_conv_nth j pi pj not_empty snd_eqD subst_compose_def) 
    qed 
  next
    case (Suc n)
    with i have ss_i:"renamed_lhs_αs!i = ss!i"
      unfolding renamed_lhs_αs_def by (simp add: nth_tl renamed_lhs_αs_def ss_def) 
    have 1:"xj ∈ vars_term (ss ! i)" 
      unfolding xj using j nth_mem ss_i by fastforce 
    have 2:"pj ∈ var_poss (ss ! i)"
      unfolding pj by (metis j length_var_poss_list nth_mem ss_i var_poss_list_sound) 
    have 3:"ss ! i |_ pj = Var xj"
      unfolding xj pj using j ss_i vars_term_list_var_poss_list by auto 
    consider "τ xj = Var xj" | "pj ∈ poss (renamed_lhs_β |_ (ps!i)) ∧ τ xj = renamed_lhs_β |_ (ps!i) |_ pj ⋅ ?τ'"
      using tau.apply_tau_ss_var[OF tau] 1 2 3 τ_def i length_renamed_lhs_αs not_empty ss_def by auto 
    then show ?thesis proof(cases)
      case 1
      then show ?thesis unfolding xj using σ_x[OF i]
        by (metis (mono_tags, opaque_lifting) eval_term.simps(1) j pi pj prod.collapse subst_compose)
    next
      case 2
      from renamed_lhs_β_τ'_σ have "renamed_lhs_β ⋅ (?τ' ∘⇩s σ) = s|_q"
        using Suc_le_eq i ss_def by auto 
      then have "renamed_lhs_β |_ (ps!i) |_ pj ⋅ (?τ' ∘⇩s σ) = s|_q |_ (ps!i) |_ pj"
        by (smt (verit) "2" hd_Cons_tl i len_ss_ps length_0_conv length_nth_simps(2) length_renamed_lhs_αs nth_mem ps_in_poss_ren_β not_empty ss_def subt_at_subst)
      with 2 have "(τ ∘⇩s σ) xj = s|_q |_ (ps!i) |_ pj" 
        by (metis (mono_tags, lifting) subst_compose subst_subst_compose) 
      moreover have "ps!i = pos_diff pi q"
        unfolding Suc ps_def pi by (metis Suc Suc_less_eq hd_Cons_tl i length_map length_nth_simps(2) length_renamed_lhs_αs nth_Cons_Suc nth_map not_empty) 
      ultimately show ?thesis unfolding xj pj
        by (metis Suc i length_renamed_lhs_αs nth_mem pi pi_below_q pi_poss prod.collapse q subt_at_append subt_at_pos_diff zero_less_Suc)
    qed
  qed
qed

lemma renamed_lhs_α_τ_σ:
  assumes i:"i < length renamed_lhs_αs"
    and pi:"pi = snd (rdp_A ! i)" 
  shows "renamed_lhs_αs!i ⋅ (τ ∘⇩s σ) = s|_pi" 
proof- 
  let ?αi="fst (rdp_A ! i)"
  from i have elem:"(?αi, pi) ∈ set (redex_patterns A)"
    using length_renamed_lhs_αs pi rdp_A_subs_A by auto
  from i have "zip [0..<length rdp_A] (map (λ(α, p). lhs α) rdp_A) ! i = (i, lhs ?αi)" 
    by (simp add: length_renamed_lhs_αs split_beta) 
  then have ren_i:"renamed_lhs_αs!i = map_vars_term (rename_many' ren i) (lhs ?αi)"
    using i length_renamed_lhs_αs renamed_lhs_αi by fastforce 
  show ?thesis 
    using source_subst_renamed_lhs[OF elem A_wf ren_i] σ_τ_x[OF i] by (metis length_var_poss_list pi s(1))
qed

lemma l_τ_σ:
  shows "l ⋅ (τ ∘⇩s σ) = s|_p" 
proof- 
  from renamed_lhs_α_τ_σ have "renamed_lhs_α1 ⋅ (τ ∘⇩s σ) = s|_p1"
    unfolding ren_lhs_α1_alt by (metis α1p1 hd_conv_nth length_greater_0_conv length_renamed_lhs_αs not_empty snd_conv)
  with renamed_lhs_β_τ_σ show ?thesis unfolding l_def using p_def
    by (smt (verit, ccfv_SIG) ctxt_supt_id diff_q_p_poss_renamed_α1 less_eq_pos_simps(1) less_eq_pos_simps(5) p_poss 
      pq_pos_diff replace_at_subt_at subst_apply_term_ctxt_apply_distrib subt_at.simps(1) subt_at_append subt_at_subst) 
qed

lemma B'_wf:"B' ∈ wf_pterm S" 
proof-
  have len:"length (var_rule β) = length (vars_term_list renamed_lhs_β)"
    using β unfolding renamed_lhs_β_def by (metis length_map S.length_var_rule vars_map_vars_term) 
  have "Prule β (map (to_pterm ∘ τ) (vars_term_list renamed_lhs_β)) ∈ wf_pterm S" 
    using wf_pterm.intros(3)[OF β] len by simp  
  then show ?thesis using ctxt_wf_pterm[OF to_pterm_wf_pterm[of "l ⋅ τ" S]] diff_q_p_poss_l
    unfolding B'_def by (simp add: to_pterm_subst)
qed

lemma p_above_pi:
  assumes i:"i < length rdp_A"
    and pi:"pi = snd (rdp_A ! i)" 
  shows "p ≤⇩p pi"
  by (metis (no_types, lifting) Suc_pred α1p1 hd_conv_nth i length_greater_0_conv less_Suc_eq_0_disj 
   less_eq_pos_simps(1) prefix_order.dual_order.strict_trans2 prefix_order.strict_implies_order prefix_order.order_refl 
   p_def pi pi_below_q pq_pos_diff prod.collapse not_empty snd_conv) 

lemma pos_diff_pi_p:
  assumes i:"i < length rdp_A"
    and pi:"pi = snd (rdp_A ! i)" 
  shows "pos_diff pi p ∈ poss l" 
proof(cases i)
  case 0
  then have p1:"pi = p1"
    by (metis α1p1 hd_conv_nth pi not_empty snd_conv)
  then show ?thesis proof(cases "p = p1")
    case True
    with p1 show ?thesis
      by (metis empty_pos_in_poss prefix_order.dual_order.refl prefix_pos_diff self_append_conv)
  next
    case False
    then have *:"p = q" 
      unfolding p_def by presburger 
    then have "pos_diff p1 q ∈ poss renamed_lhs_β"
      by (simp add: ps_def ps_in_poss_ren_β)
    with * show ?thesis unfolding l_def p1
      by (metis empty_pos_in_poss pq_pos_diff replace_at_subt_at self_append_conv subt_at.simps(1)) 
  qed
next
  case (Suc n)
  let ?αi="fst (rdp_A ! i)"
  have pi_poss_s:"pi ∈ poss s"
    by (metis i nth_mem pi pi_poss prod.exhaust_sel) 
  show ?thesis proof(cases "p = p1")
    case True
    have "q ≤⇩p pi"
      using pi_below_q i Suc prefix_order.less_le pi prod.collapse by blast
    then obtain r where r:"pi = q@r"
      using prefix_def by metis 
    have possL_B:"possL B = {q @ r |r. r ∈ fun_poss (lhs β)}"
      using S.single_redex_possL B β q by force 
    have "to_rule ?αi ∈ R"
      by (metis αi_in_R i nth_mem prod.exhaust_sel)
    then have possL_i:"possL (ll_single_redex s pi ?αi) = {pi @ r |r. r ∈ fun_poss (lhs ?αi)}"
      using R.single_redex_possL pi_poss_s by auto
    have "measure_ov (ll_single_redex s pi ?αi) B ≠ 0"
      using overlap i pi by simp
    then obtain r1 r2 where "r1 ∈ fun_poss (lhs ?αi)" "r2 ∈ fun_poss (lhs β)" "pi@r1 = q@r2"
      unfolding possL_B possL_i by (smt (verit, best) card.empty disjoint_iff mem_Collect_eq) 
    then have "r ∈ fun_poss (lhs β)" 
      unfolding r using fun_poss_append_poss' by auto 
    then show ?thesis
      by (smt (verit, best) ‹q ≤⇩p pi› append.assoc append_eq_append_conv diff_q_p_poss_renamed_α1 fun_poss_imp_poss 
          hole_pos_ctxt_of_pos_term hole_pos_poss_conv l_def prefix_order.order_trans p_def poss_map_vars_term pq pq_pos_diff prefix_pos_diff r renamed_lhs_β_def) 
  next 
    case False
    then have pq:"p = q" 
      unfolding p_def by presburger 
    from i have i':"i < length (map snd rdp_A)"
      unfolding length_map by simp
    from Suc i have "ps!i = map (λpi. pos_diff pi q) (map snd rdp_A) ! i"
      unfolding ps_def by (simp add: nth_tl) 
    also have "... = pos_diff pi q"
      using i pi by fastforce 
    finally have "pos_diff pi p = ps!i"
      unfolding pq by simp
    then show ?thesis using tau.poss[OF tau] i
      unfolding l_def by (metis diff_q_p_poss_renamed_α1 hd_Cons_tl len_ss_ps length_0_conv length_renamed_lhs_αs nth_mem 
          pq pq_pos_diff not_empty ren_lhs_α1_alt replace_at_subt_at self_append_conv ss_def subt_at.simps(1)) 
  qed
qed

lemma As'_As:
  assumes i:"i < length rdp_A"
  shows "replace_at (to_pterm s) p (As'!i ⋅ (to_pterm ∘ σ)) = As!i"
proof-
  obtain pi αi where redex_i:"(αi, pi) = rdp_A!i"
    by (metis surj_pair) 
  with i have As_i:"As!i = ll_single_redex s pi αi" 
    unfolding As by (metis case_prod_conv nth_map)  
  have pi:"p ≤⇩p pi" 
    using p_above_pi by (metis i redex_i snd_conv) 
  have pi_poss_s:"pi ∈ poss s"
    by (metis i nth_mem pi_poss redex_i)
  from i have pos_diff_pi_p':"pos_diff pi p ∈ poss (to_pterm (l ⋅ τ))"
    by (metis pos_diff_pi_p redex_i snd_conv p_in_poss_to_pterm poss_imp_subst_poss) 
  from pi have p_pi:"p @ pos_diff pi p = pi" by simp
  have A'_sigma:"As'!i ⋅ (to_pterm ∘ σ) = (ctxt_of_pos_term (pos_diff pi p) ((to_pterm s)|_p)) ⟨As!i|_pi⟩" proof-
    from i redex_i have zip1:"zip rdp_A [0..<length rdp_A] ! i = ((αi, pi), i)" by simp
    then have A'_i:"As'!i = replace_at (to_pterm (l ⋅ τ)) (pos_diff pi p) (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))))"
      using i As'_def by fastforce 
    have lhs_at_i:"renamed_lhs_αs!i = map_vars_term (rename_many' ren i) (lhs αi)"
      using renamed_lhs_αi redex_i by (metis fst_conv i)
    moreover have lin_lhs:"linear_term (renamed_lhs_αs!i)"
      by (simp add: i length_renamed_lhs_αs lin_renamed_lhs_αi) 
    ultimately have len:"length (var_rule αi) = length (vars_term_list (renamed_lhs_αs!i))"
      by (metis fst_eqD i length_map linear_term_var_vars_term_list overlapping_part.lin_lhs_αi overlapping_part_axioms redex_i vars_map_vars_term)
    then have len2:"length (var_rule αi) = length (var_poss_list (renamed_lhs_αs!i))"
      by (simp add: length_var_poss_list)
    have var_poss_list:"var_poss_list (rename_list (map (λ(α, p). lhs α) rdp_A) ! i) = var_poss_list (lhs αi)"
      using lhs_at_i var_poss_list_map_vars_term renamed_lhs_αs_def by auto
    let ?xs1="map (λs. s ⋅ (to_pterm ∘ σ)) (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))"
    let ?xs2="map (to_pterm ∘ (λp'. s |_ (pi @ p'))) (var_poss_list (renamed_lhs_αs!i))"
    {fix j assume j:"j < length (var_rule αi)" 
      let ?x="map (rename_many' ren i) (var_rule αi)!j" 
      have "?x = vars_term_list (renamed_lhs_αs!i)!j" 
        using lhs_at_i by (metis fst_conv i lin_lhs_αi linear_term_var_vars_term_list redex_i vars_map_vars_term)
      with j have *:"to_pterm (τ ?x) ⋅ (to_pterm ∘ σ) = to_pterm (s|_(pi @ var_poss_list (renamed_lhs_αs!i)!j))"
        using σ_τ_x[of i j] i redex_i unfolding length_map len by (metis length_renamed_lhs_αs snd_conv subst_compose to_pterm_subst) 
      then have "?xs1 ! j = ?xs2 ! j"
        using j len2 by force
    }
    then have "?xs1 = ?xs2"
      using len2 list_eq_iff_nth_eq[of ?xs1 ?xs2] unfolding length_map by simp
    then have "Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))) ⋅ (to_pterm ∘ σ) = Prule αi ?xs2"
      unfolding eval_term.simps by simp
    then have *:"Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))) ⋅ (to_pterm ∘ σ) = As!i|_pi" 
      unfolding As_i unfolding ll_single_redex_def var_poss_list using pi_poss_s
      by (simp add: p_in_poss_to_pterm renamed_lhs_αs_def replace_at_subt_at var_poss_list)
    have "to_pterm (l ⋅ τ) ⋅ (to_pterm ∘ σ) = to_pterm s |_ p" 
      using l_τ_σ by (metis ctxt_eq ctxt_supt_id p_in_poss_to_pterm p_poss subst_subst_compose to_pterm_ctxt_of_pos_apply_term to_pterm_subst)
    then show ?thesis 
      unfolding A'_i unfolding subst_apply_term_ctxt_apply_distrib ctxt_of_pos_term_subst[OF pos_diff_pi_p', symmetric] * by simp
  qed 
  show ?thesis
    unfolding As_i A'_sigma using ctxt_apply_ctxt_apply p_poss p_pi
    by (metis (no_types, lifting) ctxt_supt_id ll_single_redex_def p_in_poss_to_pterm pi_poss_s replace_at_subt_at)
qed

lemma As'_wf:
  assumes "Ai' ∈ set As'"
  shows "Ai' ∈ wf_pterm R"
proof-
  obtain j where "j < length As'" and a:"As'!j = Ai'"
    by (metis assms in_set_idx) 
  then have j:"j < length rdp_A" 
    unfolding As'_def length_map length_zip by simp
  have "As!j = replace_at (to_pterm s) p (Ai' ⋅ (to_pterm ∘ σ))"
    using As'_As[OF j] a by force
  then have "replace_at (to_pterm s) p (Ai' ⋅ (to_pterm ∘ σ)) ∈ wf_pterm R" 
    using As_i_wf As j by (metis length_map nth_mem)
  then have "Ai' ⋅ (to_pterm ∘ σ) ∈ wf_pterm R" 
    using subt_at_is_wf_pterm p_poss by (metis hole_pos_poss subt_at_hole_pos)
  then show ?thesis
    using subst_imp_well_def by auto
qed

lemma unifier:"∃ts. unify (zip ss (map ((|_) renamed_lhs_β) ps)) [] = Some ts" 
proof-
  {fix i assume i:"i < length (zip ss (map ((|_) renamed_lhs_β) ps))" 
    have "ss ! i ⋅ σ = (map ((|_) renamed_lhs_β) ps)!i ⋅ σ" 
    proof(cases i)
      case 0
      have "renamed_lhs_β |_ (pos_diff p1 p) ⋅ σ = s |_ (q @ (pos_diff p1 p))" 
        using ren_lhs_β_σ by (metis list.set_intros(1) ps_def q subt_at_append subt_at_subst tau tau.poss)  
      moreover have "renamed_lhs_α1 |_ pos_diff q p ⋅ σ = s |_ (p1 @ pos_diff q p)" 
        using renamed_lhs_αi_σ by (metis α1p1 α1p1_in_rdpA diff_q_p_poss_renamed_α1 fst_conv hd_conv_nth length_pos_if_in_set 
        length_renamed_lhs_αs pi_poss not_empty renamed_lhs_α1_def renamed_lhs_αi snd_conv subt_at_append subt_at_subst) 
      ultimately have "renamed_lhs_α1 |_ pos_diff q p ⋅ σ = renamed_lhs_β |_ (pos_diff p1 p) ⋅ σ"
        by (metis prefix_order.dual_order.refl prefix_order.dual_order.strict_implies_order p_def pq prefix_pos_diff self_append_conv) 
      then show ?thesis unfolding ss_def ps_def 0 by simp
    next
      case (Suc n)
      have ssi:"ss!i = renamed_lhs_αs ! i" 
        unfolding Suc by (metis hd_Cons_tl length_0_conv length_renamed_lhs_αs nth_Cons_Suc not_empty ss_def) 
      from i have i':"i < length (rdp_A)"
        by (simp add: length_renamed_lhs_αs not_empty ss_def) 
      then have psi:"ps ! i = (pos_diff (snd (rdp_A ! i)) q)" 
        unfolding Suc ps_def by (simp add: nth_tl)
      from i have i:"i < length ps"
        by simp 
      with psi have "(map ((|_) renamed_lhs_β) ps)!i ⋅ σ = s |_ (snd (rdp_A ! i))" 
        using ren_lhs_β_σ ps_in_poss_ren_β unfolding nth_map[OF i]
        by (metis Suc i' nth_mem pi_below_q prod.exhaust_sel q subt_at_pos_diff subt_at_subst zero_less_Suc) 
      with ssi show ?thesis
        using renamed_lhs_αi_σ i' length_renamed_lhs_αs by presburger
    qed
  }
  then have "σ ∈ unifiers (set (zip ss (map ((|_) renamed_lhs_β) ps)))" 
    unfolding unifiers_def by (smt (verit, del_insts) in_set_zip len_ss_ps length_map map_snd_zip mem_Collect_eq) 
  then show ?thesis 
    using ex_unify_if_unifiers_not_empty by blast 
qed

(*Step 6*)
lemma unifier_no_conflict:
  assumes i:"i < j" and j:"j < length ps" 
    and not_orth:"¬ (ps ! i @ r) ⊥ ps ! j" 
    and r:"r ∈ var_poss (renamed_lhs_β |_ (ps ! i))" 
  shows "r ∉ fun_poss (ss ! i)"
proof
  assume r2:"r ∈ fun_poss (ss ! i)"
  obtain αi pi where αipi:"(αi, pi) = rdp_A ! i"
    by (meson prod.collapse) 
  with i j have αipi_in_rdp:"(αi, pi) ∈ set rdp_A"
    using len_ss_ps length_renamed_lhs_αs ss_def by auto 
  obtain Δi where Δi:"Δi = ll_single_redex s pi αi"
    by simp 
  then have possLi:"possL Δi = {pi @ r |r. r ∈ fun_poss (lhs αi)}" 
    using R.single_redex_possL using αi_in_R αipi_in_rdp pi_poss by blast 
  obtain αj pj where αjpj:"(αj, pj) = rdp_A ! j"
    by (meson prod.collapse) 
  with j have αjpj_in_rdp:"(αj, pj) ∈ set rdp_A"
    using len_ss_ps length_renamed_lhs_αs ss_def by (simp add: not_empty)
  have is_fun:"is_Fun (lhs αj)"
    using αi_in_R αjpj_in_rdp R.no_var_lhs by blast 
  have ps_j:"ps ! j = pos_diff pj q" using αjpj i j unfolding ps_def
    by (smt (verit, best) Suc_less_eq length_map length_nth_simps(2) less_imp_Suc_add list.sel(3) nth_map nth_tl snd_conv)  
  obtain Δj where Δj:"Δj = ll_single_redex s pj αj"
    by simp 
  then have possLj:"possL Δj = {pj @ r |r. r ∈ fun_poss (lhs αj)}" 
    using R.single_redex_possL using αi_in_R αjpj_in_rdp pi_poss by blast  
  have src:"source Δj = s"
    unfolding Δj using αjpj_in_rdp  rdp_A
    by (intro R.source_single_step[OF _ A_wf, unfolded s(1)], auto) 
  have "measure_ov Δj B = 0" proof(cases i)
    case 0
    then have p1:"pi = p1" 
      using αipi by (metis α1p1 hd_conv_nth not_empty snd_eqD) 
    have ps_i:"ps ! i = pos_diff p1 p" 
      unfolding 0 ps_def by simp
    then have p_pi:"pi = p @ ps ! i"
      using p1 prefix_order.dual_order.refl prefix_order.less_imp_le p_def prefix_pos_diff by metis
    from not_orth have not_orth:"¬ (pi @ pos_diff q p @ r) ⊥ pj"
      unfolding ps_i ps_j p1
      by (smt (verit) "0" αjpj append_assoc i j len_ss_ps length_0_conv length_nth_simps(2) length_renamed_lhs_αs 
          less_eq_pos_simps(2) list.exhaust_sel prefix_order.dual_order.strict_implies_order p1 p_def p_pi parallel_pos pi_below_q 
          pq_pos_diff prefix_pos_diff ps_i not_empty self_append_conv ss_def)
    then have "¬ pi ⊥ pj"
      by (meson less_eq_pos_simps(1) prefix_order.dual_order.trans parallel_pos pos_less_eq_append_not_parallel)
    then have below:"pi <⇩p pj" 
      using i j αipi αjpj order_rdp_A
      by (metis One_nat_def Suc_pred αjpj_in_rdp len_ss_ps length_nth_simps(2) length_pos_if_in_set length_renamed_lhs_αs length_tl parallel_pos_sym pos_cases ss_def) 
    then obtain p' where p':"pj = pi @ p'"
      by (meson less_pos_def')  
    have "Δi ≠ Δj" 
      unfolding Δi Δj using below by (metis Pair_inject αipi_in_rdp αjpj_in_rdp prefix_order.less_le pi_poss single_redex_neq) 
    then have Δij:"measure_ov Δi Δj = 0"
      using R.single_steps_measure unfolding Δi Δj using αipi_in_rdp αjpj_in_rdp
      by (smt (verit, ccfv_SIG) A_wf list.set_map pair_imageI rdp_A_subs_A s(1) subsetD) 
    {fix r' assume r':"pi @ pos_diff q p @ r @ r' ∈ poss s" 
      have possL_B:"possL B = {q @ q' | q'. q' ∈ fun_poss (lhs β)}"
        by (simp add: B β q S.single_redex_possL) 
      have "ps ! i ∈ poss (lhs β)"
        using i j ps_in_poss_ren_β renamed_lhs_β_def by force 
      then have "(ps ! i) @ r @ r' ∉ fun_poss (lhs β)" 
        using r unfolding renamed_lhs_β_def by (metis append.right_neutral fun_poss_fun_conv fun_poss_imp_poss 
        fun_poss_map_vars_term subterm_poss_conv term.distinct(1) var_pos_maximal var_poss_iff) 
      then have "pi @ pos_diff q p @ r @ r' ∉ possL B" 
        unfolding p_pi possL_B by (smt (verit, ccfv_SIG) append_assoc mem_Collect_eq p1 p_def p_pi pq_pos_diff same_append_eq) 
    }note possL_B=this
    from r2 have "pos_diff q p @ r ∈ fun_poss renamed_lhs_α1"
      by (metis "0" diff_q_p_poss_renamed_α1 fun_poss_fun_conv fun_poss_imp_poss is_FunI nth_Cons_0 poss_append_poss poss_is_Fun_fun_poss ss_def subt_at_append) 
    then have "pos_diff q p @ r ∈ fun_poss (lhs αi)" 
      using αipi 0 by (metis α1p1 fst_conv fun_poss_map_vars_term hd_conv_nth not_empty renamed_lhs_α1_def) 
    then have pi:"pi @ pos_diff q p @ r ∈ possL Δi" 
      unfolding possLi p1 by simp
    {assume "pj ≤⇩p pi @ pos_diff q p @ r" 
      then obtain p'' where p'':"pj @ p'' = pi @ pos_diff q p @ r"
        by (meson prefix_pos_diff) 
      then have r:"pos_diff q p @ r = p' @ p''" 
        unfolding p' by simp
      have pj:"pj ∈ possL Δj" 
        unfolding possLj using is_fun by (simp add: poss_is_Fun_fun_poss)
      from pi have "pj ∈ possL Δi" 
        unfolding possLi p' p'' p1 using fun_poss_append_poss' r by auto
      with pj have False 
        using Δij by (simp add: disjoint_iff finite_labelposs)
    }
    then have "pi @ pos_diff q p @ r <⇩p pj"
      using not_orth prefix_order.less_le pos_cases by metis
    then show ?thesis using possLj possL_B src 
      by (smt (verit, ccfv_SIG) append.assoc card.empty disjoint_iff_not_equal mem_Collect_eq 
      prefix_order.dual_order.strict_implies_order possL_subset_poss_source prefix_pos_diff subsetD)
  next
    case (Suc n)
    have ps_i:"ps ! i = pos_diff pi q" 
      using αipi i j unfolding ps_def Suc
      by (metis Suc_lessD Suc_less_SucD hd_Cons_tl length_map length_nth_simps(2) less_trans_Suc nth_Cons_Suc nth_map not_empty snd_conv) 
    then have q_pi:"q @ (ps ! i) = pi"
      by (metis (mono_tags, lifting) Suc αipi hd_Cons_tl i j len_ss_ps length_0_conv length_nth_simps(2) length_renamed_lhs_αs 
          order.strict_trans prefix_order.less_imp_le pi_below_q prefix_pos_diff not_empty ss_def zero_less_Suc)
    from not_orth have not_orth:"¬ (pi@r) ⊥ pj"
      unfolding ps_i ps_j by (smt (verit, ccfv_SIG) Suc αipi αjpj append.assoc i j len_ss_ps length_0_conv length_nth_simps(2) length_renamed_lhs_αs 
      less_eq_pos_simps(2) list.exhaust_sel order.strict_trans prefix_order.le_less parallel_pos pi_below_q prefix_pos_diff not_empty ss_def zero_less_Suc) 
    then have "¬ pi ⊥ pj"
      by (metis less_eq_pos_simps(1) prefix_order.trans parallel_pos pos_less_eq_append_not_parallel) 
    then have below:"pi <⇩p pj" 
      using i j αipi αjpj order_rdp_A
      by (metis len_ss_ps length_0_conv length_renamed_lhs_αs list.collapse list.size(4) not_empty parallel_pos_sym pos_cases ss_def)
    then obtain p' where p':"pj = pi @ p'"
      by (meson less_pos_def')  
    have "Δi ≠ Δj" 
      unfolding Δi Δj using below by (metis Pair_inject αipi_in_rdp αjpj_in_rdp prefix_order.less_le pi_poss single_redex_neq) 
    then have Δij:"measure_ov Δi Δj = 0"
      using R.single_steps_measure unfolding Δi Δj using αipi_in_rdp αjpj_in_rdp
      by (smt (verit, ccfv_SIG) A_wf list.set_map pair_imageI rdp_A_subs_A s(1) subsetD) 
    {fix r' assume r':"pi @ r @ r' ∈ poss s" 
      have possL_B:"possL B = {q @ q' | q'. q' ∈ fun_poss (lhs β)}"
        by (simp add: B β q S.single_redex_possL) 
      have "ps ! i ∈ poss (lhs β)"
        using i j ps_in_poss_ren_β renamed_lhs_β_def by force 
      then have "(ps ! i) @ r @ r' ∉ fun_poss (lhs β)" 
        using r unfolding renamed_lhs_β_def  by (metis append.right_neutral fun_poss_fun_conv fun_poss_imp_poss 
        fun_poss_map_vars_term subterm_poss_conv term.distinct(1) var_pos_maximal var_poss_iff) 
      then have "pi @ r @ r' ∉ possL B" 
        unfolding q_pi[symmetric] possL_B by simp
    }note possL_B=this
    from r2 have "r ∈ fun_poss (renamed_lhs_αs ! i)" 
      unfolding ss_def by (metis Suc hd_Cons_tl length_0_conv length_renamed_lhs_αs nth_Cons_Suc not_empty)
    then have "r ∈ fun_poss (lhs αi)" 
      using αipi by (metis Suc_diff_1 Suc_lessD α1p1_in_rdpA fst_conv fun_poss_map_vars_term i j len_ss_ps 
          length_nth_simps(2) length_pos_if_in_set length_renamed_lhs_αs length_tl less_trans_Suc renamed_lhs_αi ss_def) 
    then have pi:"pi @ r ∈ possL Δi" 
      unfolding possLi by simp
    {assume "pj ≤⇩p pi @ r" 
      then obtain p'' where p'':"pj @ p'' = pi @ r"
        by (meson prefix_pos_diff) 
      then have r:"r = p' @ p''" 
        unfolding p' by simp
      have pj:"pj ∈ possL Δj" 
        unfolding possLj using is_fun by (simp add: poss_is_Fun_fun_poss)
      from pi have "pj ∈ possL Δi" 
        unfolding possLi p' p'' r using fun_poss_append_poss' by blast  
      with pj have False 
        using Δij by (simp add: disjoint_iff finite_labelposs)
    }
    then have "pi @ r <⇩p pj"
      using not_orth prefix_order.less_le pos_cases by metis
    then show ?thesis using possLj possL_B src
      by (smt (verit, ccfv_SIG) append.assoc card.empty disjoint_iff_not_equal mem_Collect_eq 
      prefix_order.dual_order.strict_implies_order possL_subset_poss_source prefix_pos_diff subsetD)
  qed
  then show False 
    using overlap[OF αjpj_in_rdp Δj] by simp
qed

lemma tau_is_mgu:
  shows "mgu_list (map2 (λx y. (x, l |_ y)) renamed_lhs_αs (map (λ(αi, pi). pos_diff pi p) rdp_A)) = Some τ"
proof-
  let ?q="pos_diff q p" 
  let ?p="pos_diff p1 p"
  let ?ps="map (λ(αi, pi). pos_diff pi p) rdp_A"
  obtain ss' where ss':"unify (zip ss (map ((|_) renamed_lhs_β) ps)) [] = Some ss'" 
    using unifier by blast
  have "unify (map2 (λx y. (x, l |_ y)) renamed_lhs_αs ?ps) [] = unify (zip ss (map ((|_) renamed_lhs_β) ps)) []" 
  proof-
    let ?zips1="map2 (λx y. (x, l |_ y)) renamed_lhs_αs ?ps" 
    let ?zips2="zip ss (map ((|_) renamed_lhs_β) ps)" 
    have ctxt2:"l |_ ?p = replace_at renamed_lhs_α1 ?q (renamed_lhs_β |_ pos_diff p1 p)"
      using  l_def by (metis empty_pos_in_poss prefix_order.dual_order.refl p_def prefix_pos_diff replace_at_subt_at self_append_conv subt_at.simps(1))
    obtain tl1 where tl1:"renamed_lhs_αs = renamed_lhs_α1 # tl1" "tl1 = (tl renamed_lhs_αs)"
      by (metis hd_Cons_tl length_0_conv length_renamed_lhs_αs not_empty ren_lhs_α1_alt) 
    obtain tl2 where tl2:"?ps = pos_diff p1 p # tl2" "tl2 = tl ?ps"
      using list.collapse[OF not_empty] unfolding α1p1[symmetric] by (smt (verit, best) Cons_eq_map_conv case_prod_conv map_tl)
    have len:"length ?ps = length ps" 
      unfolding ps_def by (simp add: not_empty)
    {fix i assume i:"i < length rdp_A" "i > 0"
      then obtain j where j:"i = Suc j"
        using not0_implies_Suc by blast 
      let ?pi="map snd rdp_A ! i"
      obtain pi where pi:"pi = ?ps ! i" 
        by simp
      with i have pi_pos_diff:"pi = pos_diff ?pi p" 
        unfolding nth_map[OF i(1)] by (metis case_prod_conv prod.collapse)
      obtain pi' where pi':"pi' = ps ! i" 
        by simp
      from i(1) have pi'':"pi' = pos_diff ?pi q" 
        unfolding pi' ps_def j using tl2(1) by force 
      have "q ≤⇩p ?pi" 
        using pi_below_q[OF i] by (metis eq_snd_iff i(1) nth_map prefix_order.le_less)
      then have "pi = (pos_diff q p) @ pi'" 
        unfolding pi'' pi_pos_diff by (metis append.assoc less_eq_pos_simps(1) pq_pos_diff prefix_pos_diff same_append_eq) 
      then have "l |_ pi =  renamed_lhs_β |_ pi'"
        unfolding l_def by (simp add: diff_q_p_poss_renamed_α1 replace_at_below_poss replace_at_subt_at)
      then have "map ((|_) l) ?ps ! i = map ((|_) renamed_lhs_β) ps ! i"
        using i(1) len pi pi' by auto
    }
    then have "tl (map ((|_) l) ?ps) = tl (map ((|_) renamed_lhs_β) ps)" 
      using list_tl_eq not_empty len by (metis length_map)
    then have tl_zips:"tl ?zips1 = tl ?zips2" 
      unfolding tl1(1) tl2(1) ss_def ps_def zip_Cons_Cons list.map list.sel(3)
      using tl1(2) by (metis zip_map2)
    have "?zips1 = (renamed_lhs_α1, l |_ ?p) # (tl ?zips1)"
      unfolding tl1(1) tl2(1) list.map zip_Cons_Cons by simp
    then have *:"?zips1 = (renamed_lhs_α1, l |_ ?p) # (tl ?zips2)"
      using tl_zips by simp 
    show ?thesis using unify_ctxt_same unfolding * ss_def ps_def list.map zip_Cons_Cons list.sel(3) unfolding ctxt2
      by (metis diff_q_p_poss_renamed_α1 replace_at_ident)
  qed
  then have "unify (map2 (λx y. (x, l |_ y)) renamed_lhs_αs ?ps) [] = Some ss'" 
    unfolding ss' by simp
  moreover have "τ = subst_of ss'"
    using tau.tau_is_unifier[OF tau ss'] unifier_no_conflict unfolding τ_def by blast 
  ultimately show ?thesis unfolding mgu_list_def by simp
qed


lemma fun_poss_l_tau:
  assumes r:"r ∈ fun_poss (l ⋅ τ)" 
  shows "p@r ∈ possL B ∨ (∃A ∈ set As. p@r ∈ possL A)" 
proof(cases "r ∈ fun_poss l")
 case True
  then show ?thesis proof(cases "pos_diff q p ≤⇩p r")
    case True
    with ‹r ∈ fun_poss l› have "pos_diff r (pos_diff q p) ∈ fun_poss renamed_lhs_β"
      unfolding l_def by (metis diff_q_p_poss_renamed_α1 fun_poss_in_ctxt hole_pos_ctxt_of_pos_term prefix_pos_diff) 
    then show ?thesis
      by (smt (verit, del_insts) B True β append.assoc fun_poss_map_vars_term mem_Collect_eq pq_pos_diff prefix_pos_diff q renamed_lhs_β_def S.single_redex_possL)
  next
    case False
    with ‹r ∈ fun_poss l› have "r ∈ fun_poss renamed_lhs_α1"  
      unfolding l_def using diff_q_p_poss_renamed_α1 replace_at_fun_poss_not_below by auto 
    then have "p@r ∈ possL (ll_single_redex s p1 α1)"
      by (metis (mono_tags, lifting) False α1p1_in_rdpA αi_in_R append_self_conv fun_poss_map_vars_term less_eq_pos_simps(1,2) 
          mem_Collect_eq overlapping_part.p_def overlapping_part_axioms pi_poss pq_pos_diff renamed_lhs_α1_def R.single_redex_possL)
    then have "p@r ∈ possL (hd As)"
      by (metis As case_prod_conv hd_map overlapping_part.α1p1 overlapping_part_axioms not_empty) 
    then show ?thesis
      using As not_empty hd_in_set by blast
  qed
next
  case False
  with r obtain r' where r':"r = (pos_diff q p) @ r'" and "r' ∈ fun_poss (renamed_lhs_β ⋅ τ)" 
    unfolding l_τ using diff_q_p_poss_renamed_α1 fun_poss_ctxt_apply_term hole_pos_ctxt_of_pos_term l_def by metis
  with False obtain r1 r2 y where r1:"renamed_lhs_β|_r1 = Var y" "r1 ∈ poss renamed_lhs_β" and r2:"r2 ∈ fun_poss (τ y)" and r1r2:"r' = r1@r2"
    by (smt (verit, best) diff_q_p_poss_renamed_α1 fun_poss_fun_conv fun_poss_imp_poss hole_pos_ctxt_of_pos_term hole_pos_poss is_FunI l_def 
        poss_append_poss poss_is_Fun_fun_poss poss_subst_choice replace_at_subt_at subt_at_append)
  from r1 have r1_poss:"r1 ∈ var_poss renamed_lhs_β"
    using var_poss_iff by blast 
  then obtain i r'' where i:"i < length ss" and ps_i:"ps ! i @ r'' = r1" "r'' ∈ poss (ss ! i)" "τ y = ss ! i |_ r''"
    using tau.apply_tau_t_var'[OF tau r1_poss r1(1)] τ_def r2 by auto
  with r2 have fun_poss:"r''@r2 ∈ fun_poss (ss!i)"
    by (smt (verit) fun_poss_fun_conv fun_poss_imp_poss is_FunI poss_append_poss poss_is_Fun_fun_poss subt_at_append)
  have poss:"r' = ps!i @ r'' @ r2" 
    using ps_i(1) r1r2 by simp
  have "p@r ∈ possL (As!i)" proof(cases i)
    case 0
    then have p0:"ps!i = pos_diff p1 p" unfolding ps_def by simp
    with poss have poss:"r' = pos_diff p1 p @ r'' @ r2" 
      by simp
    have "p@r ∈ possL (ll_single_redex s p1 α1)" proof(cases "q <⇩p p1")
      case True
      then have p:"p = q" unfolding p_def by simp
      from fun_poss have "r''@r2 ∈ fun_poss (lhs α1)" 
        unfolding 0 p using fun_poss_map_vars_term p pq_pos_diff by (metis nth_Cons_0 renamed_lhs_α1_def self_append_conv ss_def subt_at.simps(1)) 
      then show ?thesis unfolding p r' poss
        by (smt (verit, best) True α1p1_in_rdpA αi_in_R append_assoc mem_Collect_eq prefix_order.dual_order.strict_implies_order p pi_poss pq_pos_diff prefix_pos_diff R.single_redex_possL)
    next
      case False
      then have p:"p = p1" unfolding p_def by simp
      from fun_poss have "r ∈ fun_poss (lhs α1)"
        unfolding 0 p r' poss
        by (metis append_eq_append_conv2 diff_q_p_poss_renamed_α1 fun_poss_fun_conv fun_poss_imp_poss fun_poss_map_vars_term nth_Cons_0 
            prefix_order.dual_order.refl p pos_append_poss poss_is_Fun_fun_poss prefix_pos_diff renamed_lhs_α1_def self_append_conv ss_def subt_at_append term.disc(2))
      then show ?thesis 
        using α1p1_in_rdpA αi_in_R p p_def p_poss R.single_redex_possL by force 
    qed
    then have "p@r ∈ possL (hd As)"
      by (metis As case_prod_conv hd_map overlapping_part.α1p1 overlapping_part_axioms not_empty) 
    then show ?thesis
      by (simp add: "0" As not_empty hd_conv_nth)
  next
    case (Suc n)
    from i have i':"i < length ps"
      using length_renamed_lhs_αs len_ss_ps by force 
    let ?pi="snd (rdp_A ! i)" and ?αi="fst (rdp_A ! i)"
    have red_i:"(?αi, ?pi) = rdp_A ! i" by simp
    have i'':"i < length rdp_A"
      using i length_renamed_lhs_αs not_empty ss_def by fastforce
    then have αi:"to_rule ?αi ∈ R"
      by (metis αi_in_R nth_mem red_i)
    from i' have pi:"ps!i = pos_diff ?pi q" 
      unfolding Suc nth_Cons_Suc ps_def by (simp add: nth_tl)
    have poss:"p@r = ?pi @ r'' @ r2" 
      unfolding r' pi poss
      by (metis Suc append_assoc i'' prefix_order.dual_order.strict_implies_order pi_below_q pq_pos_diff prefix_pos_diff red_i zero_less_Suc)
    have ss_i:"ss ! i = renamed_lhs_αs ! i" 
      using Suc i nth_tl ss_def by auto
    then have "r2 ∈ fun_poss (renamed_lhs_αs ! i |_r'')" 
      using r2(1) ps_i(3) by auto
    then have "r'' @ r2 ∈ fun_poss (renamed_lhs_αs ! i)"
      using ss_i fun_poss by presburger 
    then have "r''@ r2 ∈ fun_poss (lhs ?αi)"
      by (simp add: fun_poss_map_vars_term i'' length_renamed_lhs_αs renamed_lhs_αi) 
    then have "p@r ∈ possL (ll_single_redex s ?pi ?αi)" 
      unfolding poss using R.single_redex_possL[OF αi] by (metis (mono_tags, lifting) i'' mem_Collect_eq nth_mem pi_poss red_i) 
    moreover from red_i i'' have "As!i = ll_single_redex s ?pi ?αi" 
      by (metis (no_types, lifting) As nth_map split_beta)
    ultimately show ?thesis by simp
  qed
  with i show ?thesis
    using As not_empty length_rdp_A length_renamed_lhs_αs ss_def
    by (metis One_nat_def Suc_pred add.right_neutral add_Suc_right length_greater_0_conv length_tl list.size(4) nth_mem)
qed

(*Step 7 of main proof*)
lemma renamed_lhs_αi_τ:
  assumes i:"i < length rdp_A"
    and pi:"pi = snd (rdp_A ! i)"  
  shows "renamed_lhs_αs!i ⋅ τ = l|_(pos_diff pi p) ⋅ τ"
proof(cases i)
  case 0
  then have pi:"pi = p1" 
    unfolding pi by (metis α1p1 hd_conv_nth not_empty snd_conv) 
  from 0 have α1:"renamed_lhs_αs ! i = renamed_lhs_α1"
    by (metis hd_conv_nth i length_greater_0_conv length_renamed_lhs_αs ren_lhs_α1_alt) 
  have "renamed_lhs_α1 |_ pos_diff q p ⋅ τ = renamed_lhs_β |_ (pos_diff p1 p) ⋅ τ"
    using tau.ss_i_τ_eq_t_τ[OF tau unifier] unifier_no_conflict τ_def ps_def ss_def by force 
  then show ?thesis unfolding pi α1 using l_τ
    by (metis (lifting) append_self_conv assms(2) diff_q_p_poss_renamed_α1 i l_def p_above_pi
        p_def pi pq_pos_diff prefix_pos_diff replace_at_ident replace_at_subt_at
        subst_apply_term_ctxt_apply_distrib subt_at.simps(1))
next
  case (Suc n)
  then have αi:"renamed_lhs_αs ! i = ss ! i"
    by (metis length_0_conv length_renamed_lhs_αs list.collapse nth_Cons_Suc not_empty ss_def)
  have pi:"ps ! i = pos_diff pi q"
    unfolding ps_def Suc by (metis Suc Suc_less_eq i length_map length_nth_simps(2) length_nth_simps(4) list.collapse nth_map pi not_empty) 
  have below:"pos_diff q p ≤⇩p pos_diff pi p"
    by (metis Suc assms(2) i less_eq_pos_simps(2) prefix_order.dual_order.strict_implies_order p_above_pi pi_below_q pq_pos_diff prefix_pos_diff prod.collapse zero_less_Suc)
  have "ss ! i ⋅ τ = renamed_lhs_β |_ (ps!i) ⋅ τ"
    using tau.ss_i_τ_eq_t_τ[OF tau unifier] unifier_no_conflict by (simp add: τ_def i length_renamed_lhs_αs not_empty ss_def) 
  then show ?thesis unfolding αi l_def pi using below
    by (smt (verit, best) append.assoc assms(2) diff_q_p_poss_renamed_α1 i l_def less_eq_pos_simps(1) overlapping_part.pos_diff_pi_p 
        overlapping_part_axioms p_above_pi poss_append_poss pq_pos_diff prefix_pos_diff replace_at_subt_at same_append_eq subt_at_append)
qed

lemma Ai'_single_redex:
  assumes i:"i < length rdp_A" and redex_i:"rdp_A ! i = (αi, pi)"
  shows "As'!i = ll_single_redex (l ⋅ τ) (pos_diff pi p) αi" 
proof-
  from i redex_i have zip1:"zip rdp_A [0..<length rdp_A] ! i = ((αi, pi), i)" by simp
  then have A'_i:"As'!i = replace_at (to_pterm (l ⋅ τ)) (pos_diff pi p) (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))))"
    unfolding As'_def using i by fastforce
  have "to_rule αi ∈ R"
    by (metis αi_in_R i nth_mem redex_i)
  then have len:"length (var_rule αi) = length (var_poss_list (lhs αi))"
    by (metis length_var_poss_list R.length_var_rule)
  {fix j assume j:"j < length (var_rule αi)"
    let ?xj="(rename_many' ren i) (var_rule αi ! j)"
    let ?pj="pos_diff pi p @ (var_poss_list (lhs αi) ! j)"
    have "renamed_lhs_αs ! i = map_vars_term (rename_many' ren i) (lhs αi)" 
      using renamed_lhs_αi by (metis fst_conv i redex_i) 
    then have "τ ?xj = l ⋅ τ |_ ?pj" using renamed_lhs_αi_τ
      by (smt (verit, ccfv_SIG) eval_term.simps(1) fst_conv i j len length_map lin_lhs_αi linear_term_var_vars_term_list nth_map nth_mem 
      pos_diff_pi_p poss_imp_subst_poss redex_i snd_conv subt_at_append subt_at_subst var_poss_imp_poss var_poss_list_map_vars_term var_poss_list_sound vars_map_vars_term vars_term_list_var_poss_list) 
    then have "map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)) ! j = map (to_pterm ∘ (λpia. l ⋅ τ |_ (pos_diff pi p @ pia))) (var_poss_list (lhs αi)) ! j"
      using j len nth_map by simp
  }
  with len have "map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)) = map (to_pterm ∘ (λpia. l ⋅ τ |_ (pos_diff pi p @ pia))) (var_poss_list (lhs αi))" 
    using list_eq_iff_nth_eq by (metis length_map)
  then show ?thesis 
    unfolding A'_i ll_single_redex_def by presburger
qed

lemma source_As'_i:
  assumes i:"i < length rdp_A"
  shows "source (As'!i) = l ⋅ τ" 
  using Ai'_single_redex 
proof-
  from assms obtain pi αi where redex_i:"(αi, pi) = rdp_A!i" 
    using prod.collapse by blast 
  with i have Ai'_single:"As'!i = ll_single_redex (l ⋅ τ) (pos_diff pi p) αi" 
    using Ai'_single_redex by auto
  have *:"pos_diff pi p ∈ poss (l ⋅ τ)" 
    using i redex_i by (metis pos_diff_pi_p poss_imp_subst_poss snd_eqD) 
  have ren_lhs_αi_τ:"renamed_lhs_αs!i ⋅ τ = l ⋅ τ |_ (pos_diff pi p)"
    by (metis i pos_diff_pi_p redex_i renamed_lhs_αi_τ snd_conv subt_at_subst) 
  have "renamed_lhs_αs!i ⋅ τ = lhs αi ⋅ ⟨map (λpia. l ⋅ τ |_ (pos_diff pi p @ pia)) (var_poss_list (lhs αi))⟩⇩αi" proof-
    let ?σ1="(λx. Var ((rename_many' ren i) x)) ∘⇩s τ"
    let ?σ2="⟨map (λpia. l ⋅ τ |_ (pos_diff pi p @ pia)) (var_poss_list (lhs αi))⟩⇩αi"
    {fix x assume "x ∈ vars_term (lhs αi)" 
      then obtain j where j:"j < length (vars_term_list (lhs αi))" "vars_term_list (lhs αi) ! j = x"
        by (metis in_set_conv_nth set_vars_term_list) 
      then have j':"j < length (var_rule αi)"
        by (metis αi_in_R i R.length_var_rule nth_mem redex_i) 
      let ?pj="var_poss_list (lhs αi) ! j"
      have x':"x = var_rule αi ! j"
        by (metis i j(2) lin_lhs_αi linear_term_var_vars_term_list prod.sel(1) redex_i)
      have "?σ2 x = l ⋅ τ |_ (pos_diff pi p @ ?pj)" 
        using j lhs_subst_var_i[OF x' j'] by (metis (no_types, lifting) length_map length_var_poss_list nth_map) 
      then have "?σ1 x = ?σ2 x" using ren_lhs_αi_τ
        by (smt (verit, ccfv_SIG) "*" fst_conv i j(1) j(2) length_var_poss_list nth_map nth_mem overlapping_part.renamed_lhs_αi 
         overlapping_part_axioms redex_i subst_compose_def subt_at_append subt_at_subst var_poss_imp_poss 
         var_poss_list_map_vars_term var_poss_list_sound vars_map_vars_term vars_term_list_var_poss_list) 
    }  
    then show ?thesis
      by (smt (verit, best) fst_conv i map_vars_term_as_subst overlapping_part.renamed_lhs_αi overlapping_part_axioms 
       redex_i subst_compose subst_subst_compose term_subst_eq) 
  qed
  then have "lhs αi ⋅ ⟨map (λpia. l ⋅ τ |_ (pos_diff pi p @ pia)) (var_poss_list (lhs αi))⟩⇩αi = l|_(pos_diff pi p) ⋅ τ" 
    using renamed_lhs_αi_τ[OF i] redex_i unfolding length_map length_zip by (simp add: split_pairs)
  then show ?thesis
    unfolding Ai'_single source_single_redex[OF *] by (metis "*" ctxt_supt_id i pos_diff_pi_p redex_i snd_conv subt_at_subst) 
qed

lemma rdp_Ai':
  assumes i:"i < length rdp_A"
    and αipi:"(αi, pi) = rdp_A ! i"
  shows "redex_patterns (As'!i) = [(αi, pos_diff pi p)]"
proof-
  from assms have zip1:"zip rdp_A [0..<length rdp_A] ! i = ((αi, pi), i)" by simp
  then have A'_i:"As'!i = replace_at (to_pterm (l ⋅ τ)) (pos_diff pi p) (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi))))"
    unfolding As'_def using i by fastforce
  have pos_pi:"(pos_diff pi p) ∈ poss (l ⋅ τ)"
    by (metis i pos_diff_pi_p poss_imp_subst_poss αipi snd_eqD) 
  have αi:"to_rule αi ∈ R"
    by (metis αi_in_R αipi i nth_mem)
  have "redex_patterns (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))) = [(αi, [])]"
    using left_lin_no_var_lhs.redex_patterns_prule[OF R.ll_no_var_lhs] αi
    by (smt (verit, best) length_map length_var_poss_list R.length_var_rule list.map_comp)
  then have "redex_patterns (As'!i) = [(αi, pos_diff pi p)]"
    unfolding A'_i left_lin_no_var_lhs.redex_patterns_context[OF R.ll_no_var_lhs pos_pi] by simp
  with αipi i show ?thesis by simp
qed

lemma single_steps_Ai':
  assumes i:"i < length rdp_A" 
  shows "single_steps (As'!i) = [As'!i]" 
proof-
  from assms obtain pi αi where redex_i:"(αi, pi) = rdp_A!i" 
    using prod.collapse by blast 
  with i have "As'!i = ll_single_redex (l ⋅ τ) (pos_diff pi p) αi" 
    using Ai'_single_redex by auto
  moreover have "redex_patterns (As'!i) = [(αi, pos_diff pi p)]" 
    using rdp_Ai'[OF i redex_i] by simp 
  ultimately show ?thesis
    using redex_i i source_As'_i by force
qed

lemma B'_single_redex: "B' = ll_single_redex (l ⋅ τ) (pos_diff q p) β" 
proof-
 have ren_lhs_β_τ:"renamed_lhs_β ⋅ τ = l ⋅ τ |_ (pos_diff q p)"
    by (simp add: diff_q_p_poss_renamed_α1 l_τ replace_at_subt_at)
  {fix j assume j:"j < length (vars_term_list renamed_lhs_β)"
    let ?yj="vars_term_list renamed_lhs_β ! j"
    let ?pj="var_poss_list (lhs β) ! j"
    have pj:"var_poss_list renamed_lhs_β ! j = ?pj"
      by (simp add: renamed_lhs_β_def var_poss_list_map_vars_term) 
    with j have pj':"renamed_lhs_β |_ ?pj = Var ?yj"
      by (simp add: vars_term_list_var_poss_list) 
    with ren_lhs_β_τ have "τ ?yj = l ⋅ τ |_ (pos_diff q p) |_ ?pj"
      by (metis eval_term.simps(1) j length_var_poss_list nth_mem pj subt_at_subst var_poss_imp_poss var_poss_list_sound) 
    with j have "(to_pterm ∘ τ) ?yj = (to_pterm ∘ (λpi. l ⋅ τ |_ (pos_diff q p @ pi))) ?pj"
      by (simp add: diff_q_p_poss_renamed_α1 l_τ replace_at_below_poss)
    then have "map (to_pterm ∘ τ) (vars_term_list renamed_lhs_β) ! j = map (to_pterm ∘ (λpi. l ⋅ τ |_ (pos_diff q p @ pi))) (var_poss_list (lhs β)) ! j" 
      using j unfolding renamed_lhs_β_def by (metis (mono_tags, lifting) length_map length_var_poss_list nth_map vars_map_vars_term)
  }
  then show ?thesis unfolding B'_def ll_single_redex_def renamed_lhs_β_def
    by (smt (verit) length_map length_var_poss_list nth_equalityI vars_map_vars_term) 
qed

lemma src_B':"source B' = l ⋅ τ" 
proof-
  have *:"pos_diff q p ∈ poss (l ⋅ τ)"
    by (metis diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ)
  have ren_lhs_β_τ:"renamed_lhs_β ⋅ τ = l ⋅ τ |_ (pos_diff q p)"
    by (simp add: diff_q_p_poss_renamed_α1 l_τ replace_at_subt_at)
  {fix y assume y:"y ∈ vars_term (lhs β)"
    then obtain j where j:"j < length (vars_term_list (lhs β))" "vars_term_list (lhs β) ! j = y"
      by (metis in_set_idx set_vars_term_list) 
    let ?pj="var_poss_list (lhs β) ! j"
    let ?σ1="(λx. Var (rename_single ren x)) ∘⇩s τ"    
    let ?σ2="⟨map (λpi. l ⋅ τ |_ (pos_diff q p @ pi)) (var_poss_list (lhs β))⟩⇩β"
    from j have pj:"lhs β |_ ?pj = Var y"
      using vars_term_list_var_poss_list by force
    have j':"j < length (var_rule β)"
      using j(1) β S.length_var_rule by auto 
    have y':"y = var_rule β ! j"
      by (metis β comp_eq_dest_lhs j(2) length_remdups_eq length_rev S.length_var_rule rev_rev_ident) 
    have "?σ2 y = l ⋅ τ |_ (pos_diff q p @ ?pj)" 
      using j lhs_subst_var_i[OF y' j'] by (metis (no_types, lifting) length_map length_var_poss_list nth_map) 
    then have "?σ1 y = ?σ2 y" using ren_lhs_β_τ
      by (smt (verit, del_insts) "*" j(1) j(2) length_var_poss_list nth_map nth_mem renamed_lhs_β_def 
      subst_compose_def subt_at_append subt_at_subst var_poss_imp_poss var_poss_list_map_vars_term var_poss_list_sound 
      vars_map_vars_term vars_term_list_var_poss_list)
  }
  then have "renamed_lhs_β ⋅ τ = lhs β ⋅ ⟨map (λpi. l ⋅ τ |_ (pos_diff q p @ pi)) (var_poss_list (lhs β))⟩⇩β"
    unfolding renamed_lhs_β_def map_vars_term_as_subst by (smt (verit, best) subst.cop_add term_subst_eq_conv)
  with ren_lhs_β_τ show ?thesis unfolding B'_single_redex source_single_redex[OF *]
    by (simp add: "*" ctxt_supt_id)  
qed

lemma B'_in_B: "B = replace_at (to_pterm s) p (B' ⋅ (to_pterm ∘ σ))" 
proof-
  have B'_sigma:"B' ⋅ (to_pterm ∘ σ) = (ctxt_of_pos_term (pos_diff q p) ((to_pterm s)|_p)) ⟨B|_q⟩" proof-
    have *:"pos_diff q p ∈ poss (to_pterm (l ⋅ τ))"
      by (simp add: diff_q_p_poss_l to_pterm_subst)
    {fix i assume i:"i < length (vars_term_list renamed_lhs_β)" 
      let ?x="vars_term_list renamed_lhs_β!i" 
      have tau_alt:"τ = compose (drop 0 (map2 (λx y. linear_unifier x (renamed_lhs_β |_ y)) ss ps))"
        unfolding τ_def using tau tau.τ_def by fastforce 
      have "to_pterm (τ ?x) ⋅ (to_pterm ∘ σ) = to_pterm ((τ ∘⇩s σ) ?x)"
        by (simp add: subst_compose_def to_pterm_subst)
      with i have "to_pterm (τ ?x) ⋅ (to_pterm ∘ σ) = to_pterm (s|_(q @ var_poss_list (lhs β)!i))"
        using σ_τ'_y[of 0] unfolding tau_alt by (simp add: renamed_lhs_β_def var_poss_list_map_vars_term)  
    }
    then have "Prule β (map (to_pterm ∘ τ) (vars_term_list renamed_lhs_β)) ⋅ (to_pterm ∘ σ) = Prule β (map (to_pterm ∘ (λpi. s |_ (q @ pi))) (var_poss_list (lhs β)))"
      unfolding eval_term.simps renamed_lhs_β_def by (smt (verit, ccfv_SIG) comp_apply length_map length_var_poss_list map_nth_eq_conv var_poss_list_map_vars_term)
    then show ?thesis unfolding B'_def unfolding subst_apply_term_ctxt_apply_distrib ctxt_of_pos_term_subst[OF *, symmetric] B ll_single_redex_def
      by (metis (no_types, lifting) ctxt_supt_id l_τ_σ p_in_poss_to_pterm p_poss q replace_at_subt_at subst_subst_compose to_pterm_ctxt_of_pos_apply_term to_pterm_subst) 
  qed
  show ?thesis unfolding B B'_sigma using ctxt_apply_ctxt_apply p_poss pq_pos_diff
    by (metis (no_types, lifting) ctxt_supt_id ll_single_redex_def p_in_poss_to_pterm q replace_at_subt_at) 
qed

lemma join_As':
  assumes "a1 ∈ set As'" and "a2 ∈ set As'"
  shows "a1 ⊔ a2 ≠ None"
proof- 
  from assms(1) obtain j where j:"j < length As'" and a1:"As'!j = a1" 
    by (metis (no_types, lifting) in_set_idx) 
  have length:"length As' = length rdp_A" 
    unfolding As'_def length_map length_zip by simp
  have as1:"As!j = replace_at (to_pterm s) p (a1 ⋅ (to_pterm ∘ σ))"
    using As'_As[OF j[unfolded length]] unfolding a1 by simp
  from length j have aj:"As!j ∈ set (single_steps A)"
    unfolding As using filter_ex_index in_set_conv_nth rdp_A s(1) by fastforce
  from assms(2) obtain i where i:"i < length As'" and a2:"As'!i = a2" 
    by (metis (no_types, lifting) in_set_idx) 
  have as2:"As!i = replace_at (to_pterm s) p (a2 ⋅ (to_pterm ∘ σ))"
    using As'_As[OF i[unfolded length]] unfolding a2 by simp
  from length i have ai:"As!i ∈ set (single_steps A)"
    unfolding As using filter_ex_index in_set_conv_nth rdp_A s(1) by fastforce
  have co_init:"source a1 = source a2"
    using source_As'_i a1 a2 i j unfolding length by fastforce
  show ?thesis proof(cases "i = j")
    case True
    then have "a1 = a2" 
      using a1 a2 by fastforce 
    then show ?thesis
      by (simp add: join_same)
  next
    case False
    have "As!i ≠ As!j" proof
      assume same:"As!i = As!j" 
      obtain i' j' where i':"i' < length (redex_patterns A)" "As!i = single_steps A ! i'"
        and j':"j' < length (redex_patterns A)" "As!j = single_steps A ! j'" and neq:"i' ≠ j'" 
        using filter_index_neq[OF False] i j unfolding As'_def unfolding rdp_A length_map length_zip
        by (smt (verit, best) As diff_zero length_upt min.idem nth_map prod.case_eq_if rdp_A s(1))
      from i' obtain αi pi where at_i':"redex_patterns A ! i' = (αi, pi)"
        using prod.exhaust_sel by blast 
      then have pi_pos:"pi ∈ poss (source A)"
        by (metis A_wf i'(1) left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs nth_mem) 
      from j' obtain αj pj where at_j':"redex_patterns A ! j' = (αj, pj)"
        using prod.exhaust_sel by blast 
      then have pj_pos:"pj ∈ poss (source A)"
        by (metis A_wf j'(1) left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs nth_mem) 
      have "redex_patterns A ! i' ≠ redex_patterns A ! j'" 
        using left_lin_no_var_lhs.distinct_snd_rdp[OF R.ll_no_var_lhs A_wf] neq i'(1) j'(1) using distinct_map nth_eq_iff_index_eq by blast 
      with same show False
        unfolding i'(2) j'(2) at_i' at_j' nth_map[OF i'(1)] nth_map[OF j'(1)] using single_redex_neq pj_pos pi_pos by fastforce
    qed
    then have "As!i ⊥⇩p As!j"
      using R.single_steps_orth[OF ai aj A_wf] by blast
    moreover have "ctxt_of_pos_term p (to_pterm s) ∈ wf_pterm_ctxt R"
      using p_poss by (simp add: p_in_poss_to_pterm to_pterm_trs_ctxt) 
    ultimately have "a2 ⋅ (to_pterm ∘ σ) ⊥⇩p a1 ⋅ (to_pterm ∘ σ)"
      unfolding as1 as2 using R.orthogonal_ctxt by presburger 
    then have "a2 ⊥⇩p a1" 
      using left_lin_no_var_lhs.orthogonal_subst[OF R.ll_no_var_lhs] co_init As'_wf assms by presburger
    then show ?thesis using R.orth_imp_join_defined assms
      by (metis (mono_tags, lifting) As'_wf Residual_Join_Deletion.join_sym)
  qed
qed

lemma exists_A':"∃ A'. Some A'= ⨆ As' ∧ A' ∈ wf_pterm R" 
  using left_lin_no_var_lhs.join_list_defined[OF R.ll_no_var_lhs, of As'] join_As' As'_wf As'_not_empty by auto

lemma exists_p': "∃p'. p' ∈ poss A ∧ source_ctxt (ctxt_of_pos_term p' A) = ctxt_of_pos_term p s" 
proof(cases "q <⇩p p1")
  case True
  then have pq:"p = q" 
    unfolding p_def by simp
  have "get_label (labeled_source B |_ p) = Some (β, 0)" 
    using single_redex_at_p_label[OF p_poss] β pq using B S.no_var_lhs by fastforce
  then have p_posL_B:"p ∈ possL B"
    by (simp add: get_label_imp_labelposs pq q s(2))
  have "get_label (labeled_source A |_ p) = None" proof(rule ccontr)
    assume "get_label (labeled_source A |_ p) ≠ None" 
    then obtain α n where "get_label (labeled_source A |_ p) = Some (α, n)"
      by fastforce 
    then obtain Ai where Ai:"Ai ∈ set (single_steps A)" "get_label (labeled_source Ai |_ p) = Some (α, n)" 
      using left_lin_no_var_lhs.label_single_step[OF R.ll_no_var_lhs] p_poss A_wf s(1) by force
    then have src_Ai:"source Ai = s"
      using A_wf s(1) R.source_single_step by blast
    with Ai have p:"p ∈ possL Ai"
      by (simp add: get_label_imp_labelposs p_poss) 
    from Ai(1) obtain β r where Ai_single:"Ai = ll_single_redex s r β" and rdp:"(β, r) ∈ set (redex_patterns A)" 
      using s(1) by auto
    then have rβ:"r ∈ poss s" "to_rule β ∈ R"
      using A_wf labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs s(1) by fastforce+
    from p p_posL_B have ov:"measure_ov Ai B ≠ 0"
      by (meson card_eq_0_iff disjoint_iff finite_Int finite_labelposs)
    from Ai p obtain r' where r:"r' ≤⇩p p" "get_label (labeled_source Ai |_ r') = Some (α, 0)"
      using As_i_wf append_take_drop_id less_eq_pos_simps(1) obtain_label_root
      by (metis (mono_tags, lifting) A_wf ‹source Ai = s› labeled_source_to_term poss_term_lab_to_term pq q R.single_step_wf)
    then have "(α, r') ∈ set (redex_patterns Ai)"
      by (metis (no_types, lifting) A_wf Ai(1) left_lin_no_var_lhs.redex_patterns_label left_lin_wf_trs.single_step_wf 
          R.left_lin_wf_trs_axioms prefix_def R.ll_no_var_lhs map_eq_conv poss_append_poss pq q split_beta src_Ai)  
    with Ai_single rβ have "β = α" "r = r'" 
      using left_lin_no_var_lhs.redex_patterns_single[OF R.ll_no_var_lhs] by fastforce+
    then have "(α, r') ∈ set rdp_A" unfolding rdp_A
      using Ai_single ov rdp by force
    with r(1) show False
      using True R.ll_no_var_lhs pq p_above_pi
      by (metis α1p1 hd_conv_nth in_set_conv_nth linorder_neqE_nat not_empty not_less_zero prefix_order.leD pi_below_q snd_conv) 
  qed
  then show ?thesis 
    using R.poss_labeled_source_None A_wf pq q s(1) by fastforce
next
  case False
  then have "p = p1" 
    unfolding p_def by simp
  then have "(α1, p) ∈ set (redex_patterns A)"
    using α1p1_in_rdpA rdp_A_subs_A by auto 
  then have "get_label (labeled_source A |_ p) = Some (α1, 0)"
    using A_wf left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs by blast 
  then show ?thesis
    using R.poss_labeled_source p_poss A_wf s(1) R.left_lin by force
qed


context 
  fixes A'
  assumes A':"Some A'= ⨆ As'" and A'_wf:"A' ∈ wf_pterm R"
begin

lemma rdp_A':"set (redex_patterns A') = ⋃ (set (map (set ∘ redex_patterns) As'))" 
  using left_lin_no_var_lhs.redex_patterns_join_list[OF R.ll_no_var_lhs] by (simp add: A' As'_wf)

lemma rdp_A_eq_rdp_A':"set rdp_A = (λ(αi, pi). (αi, p@pi)) ` (set (redex_patterns A'))" 
proof-
  {fix αi pi assume "(αi, pi) ∈ set rdp_A"
    then obtain i where i:"rdp_A ! i = (αi, pi)" "i < length rdp_A"
      using in_set_idx by force
    then have As'_i:"As'!i = (ctxt_of_pos_term (pos_diff pi p) (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩" 
      unfolding As'_def by simp
    from i have p:"pos_diff pi p  ∈ poss (l ⋅ τ)"
      using pos_diff_pi_p poss_imp_subst_poss by fastforce
    have "(αi, []) ∈ set (redex_patterns (Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))))" 
      unfolding redex_patterns.simps by simp
    then have "(αi, pos_diff pi p) ∈ set (redex_patterns (As'!i))"
      using rdp_Ai' i by fastforce
    moreover have "As'!i ∈ set As'"
      using i(2) unfolding As'_def by (smt (verit) in_set_conv_nth length_map map_nth zip_eq_conv)
    ultimately have "(αi, pos_diff pi p) ∈ set (redex_patterns A')" 
      unfolding rdp_A' set_map o_apply using UN_iff by blast
    then have "(αi, pi) ∈ (λ(αi, pi). (αi, p@pi)) ` (set (redex_patterns A'))"
      using i p_above_pi by force 
  } moreover
  {fix αi pi assume "(αi, pi) ∈ (λ(αi, pi). (αi, p@pi)) ` (set (redex_patterns A'))"
    then obtain pi' where p:"pi = p@pi'" and "(αi, pi') ∈ set (redex_patterns A')" 
      by force
    then obtain Ai where Ai:"Ai ∈ set As'" "(αi, pi') ∈ (set ∘ redex_patterns) Ai" 
      unfolding rdp_A' using UN_iff[of "(αi, pi')" "(set ∘ redex_patterns)" "set As'"] unfolding set_map by blast
    then obtain i where i:"i < length As'" "As'!i = Ai"
      by (meson in_set_conv_nth) 
    then have i':"i < length rdp_A" unfolding As'_def by simp
    from rdp_Ai'[OF i'] Ai(2) have "redex_patterns (As'!i) = [(αi, pi')]" 
      unfolding i(2) by (metis comp_apply in_set_simps(2) prod.collapse)
    then have "rdp_A ! i = (αi, pi)" 
      using rdp_Ai'[OF i'] p i' p_above_pi by (metis fst_conv list.sel(1) prefix_pos_diff prod.collapse snd_conv) 
    then have "(αi, pi) ∈ set rdp_A" 
      using i(1) using nth_mem by (metis i')
  }
  ultimately show ?thesis by (meson pred_equals_eq2) 
qed

lemma rdp_A_eq:"rdp_A = map (λ(αi, pi). (αi, p@pi)) (redex_patterns A')" (is "_ = ?rdp_A'") 
proof-
  have "sorted_wrt (ord.lexordp (<)) (map snd (redex_patterns A'))"
    using A'_wf left_lin_no_var_lhs.redex_patterns_sorted R.ll_no_var_lhs by blast 
  then have sorted_rdp_A':"sorted_wrt (ord.lexordp (<)) (map snd ?rdp_A')"
    by (smt (verit, del_insts) Pair_inject old.prod.case ord.lexordp_append_leftI prod.exhaust_sel sorted_wrt_iff_nth_less sorted_wrt_map) 
  have linord:"class.linorder (ord.lexordp_eq ((<) :: nat ⇒ nat ⇒ bool)) (ord.lexordp (<))"
    using linorder.lexordp_linorder[OF linorder_class.linorder_axioms] by simp
  then have map_snd:"map snd rdp_A = map snd ?rdp_A'" 
    using linorder.strict_sorted_equal[OF linord sorted_rdp_A sorted_rdp_A'] rdp_A_eq_rdp_A' by force
  have dist:"distinct (map snd rdp_A)"
    using lexord_linorder.strict_sorted_iff sorted_rdp_A by auto 
  {fix x y assume x:"x ∈ set rdp_A" and y:"y ∈ set ?rdp_A'" and xy:"snd x = snd y"
    {assume "x ≠ y"
      then have "fst x ≠ fst y" 
        using xy by (simp add: prod_eq_iff) 
      then have False 
        using x y xy dist rdp_A_eq_rdp_A' by (smt (verit, ccfv_threshold) distinct_conv_nth image_set in_set_idx length_map nth_map)
    }
    then have "x = y" by auto
  }
  then show ?thesis 
    using map_snd list.inj_map_strong by blast
qed 

lemma src_A':"source A' = l ⋅ τ" 
proof-
  obtain A' where "A' ∈ set As'" and "source A' = l ⋅ τ" 
    using As'_not_empty source_As'_i by (meson length_greater_0_conv nth_mem not_empty) 
  then show ?thesis 
    using left_lin_no_var_lhs.source_join_list[OF R.ll_no_var_lhs A'[symmetric]] As'_wf by force
qed

lemma lin_A':"linear_term A'"
  using linear_l_tau linear_source_imp_linear_pterm[OF A'_wf] src_A' by simp

lemma hd_rdp_A':"hd (redex_patterns A') = (α1, pos_diff p1 p)"
proof-
  from rdp_A_eq obtain α' p' where hd:"hd (redex_patterns A') = (α', p')" and *:"(λ(αi, pi). (αi, p @ pi)) (α', p') = (α1, p1)"
    by (metis (no_types, lifting) α1p1 hd_map map_is_Nil_conv prod.collapse not_empty) 
  then have "α' = α1"
    by fastforce 
  moreover have "p' = pos_diff p1 p" 
    using * by (metis case_prod_conv less_eq_pos_simps(1) prefix_pos_diff same_append_eq snd_conv) 
  ultimately show ?thesis 
    using hd by simp
qed

lemma single_steps_A':"single_steps A' = As'" 
proof-
  have "length (redex_patterns A') = length rdp_A"
    using rdp_A_eq by simp
  then have len:"length (redex_patterns A') = length As'" 
    unfolding length_map As'_def length_zip by simp
  {fix i assume i':"i < length As'" 
    then have i:"i < length rdp_A" 
      unfolding As'_def length_map length_zip by simp
    obtain αi pi where αipi:"(αi, pi) = rdp_A ! i"
      by (metis surj_pair) 
    then have rdp_i:"redex_patterns A' ! i = (αi, pos_diff pi p)" 
      using rdp_A_eq i by (smt (verit, del_insts) Pair_inject length_map nth_map old.prod.case p_above_pi prefix_pos_diff prod.collapse same_append_eq) 
    have "single_steps A' ! i = ll_single_redex (l ⋅ τ) (pos_diff pi p) αi" 
      unfolding nth_map[OF i'[unfolded len[symmetric]]] rdp_i src_A' by simp
    moreover have "As' ! i = ll_single_redex (l ⋅ τ) (pos_diff pi p ) αi" proof- 
      have *:"redex_patterns (As' ! i) = [(αi, pos_diff pi p)]" 
        using rdp_Ai'[OF i αipi] by simp
      have "single_steps (As' ! i) = [ll_single_redex (l ⋅ τ) (pos_diff pi p) αi]" 
        unfolding * source_As'_i[OF i] by simp
      then show ?thesis
        using single_steps_Ai'[OF i] by simp
    qed
    ultimately have "single_steps A' ! i = As' ! i" 
      by simp
  }
  with len show ?thesis
    by (simp add: list_eq_iff_nth_eq)
qed

(*Step 8 of main proof*)
context 
  fixes p'
  assumes p':"p' ∈ poss A" and ctxt_A:"source_ctxt (ctxt_of_pos_term p' A) = ctxt_of_pos_term p s"
begin 

definition "ρ = mk_subst Var (match_substs A' (A|_p'))"

lemma A'_rho:"A' ⋅ ρ = A|_p'" 
proof-
  have A_at_p'_wf:"A|_p' ∈ wf_pterm R" 
    using p' A_wf subt_at_is_wf_pterm by blast 
  {fix α r assume αr:"(α, r) ∈ set (redex_patterns A')" 
    from αr have fun_poss:"r ∈ fun_poss (source A')"
      by (metis A'_wf get_label_imp_labelposs labeled_source_to_term labelposs_subs_fun_poss_source left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs option.distinct(1) poss_term_lab_to_term) 
    from αr obtain ai where "ai ∈ set (As')" and rdp:"(α, r) ∈ set (redex_patterns ai)" 
      unfolding rdp_A' using UN_iff[of "(α, r)" "set ∘ redex_patterns" "set As'"] by force
    then obtain i where i:"i < length As'" "ai = As'!i"
      by (meson in_set_idx)
    from i(1) have i':"i < length rdp_A" 
      unfolding As'_def length_map length_zip by force
    let ?αi="fst (rdp_A ! i)" and ?pi="snd (rdp_A ! i)"
    from i(2) have set_rdp:"set (redex_patterns ai) = {(?αi, pos_diff ?pi p)}"
      using i' rdp_Ai' by (metis list.simps(15) prod.collapse set_empty)
    have "(?αi, ?pi) ∈ set (redex_patterns A)"
      using i' rdp_A_subs_A by auto
    then have "(?αi, pos_diff ?pi p) ∈ set (redex_patterns (A|_p'))"
      using left_lin_no_var_lhs.redex_patterns_label[OF R.ll_no_var_lhs]
      by (smt (verit, best) s(1) A_wf A_at_p'_wf ctxt_A ctxt_supt_id i' R.label_source_ctxt labeled_source_to_term p' p_above_pi p_poss poss_term_lab_to_term prefix_pos_diff replace_at_subt_at subterm_poss_conv) 
    with rdp set_rdp fun_poss have "(α, r) ∈ set (redex_patterns (A|_p')) ∧ r ∈ fun_poss (source A')"
      by simp
  } moreover 
  {fix α r assume αr:"(α, r) ∈ set (redex_patterns (A|_p'))" and r:"r ∈ fun_poss (source A')"
    then have αpr:"(α, p@r) ∈ set (redex_patterns A)"
      using A_at_p'_wf s(1) A_wf ctxt_A ctxt_supt_id R.label_source_ctxt labeled_source_to_term left_lin_no_var_lhs.redex_patterns_label[OF R.ll_no_var_lhs]
      by (smt (verit, ccfv_threshold) p' p_poss poss_append_poss poss_term_lab_to_term replace_at_subt_at subt_at_append)
    have pr_poss:"p@r ∈ poss s"
      using s(1) A_wf αpr left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs by blast
    have α:"to_rule α ∈ R"
      by (metis A_wf αpr labeled_source_to_term labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label R.ll_no_var_lhs poss_term_lab_to_term)
    then obtain f ts where lhs:"lhs α = Fun f ts"
      using R.no_var_lhs by fastforce 
    have pr_possL:"p@r ∈ possL (ll_single_redex s (p@r) α)"
      using R.single_redex_possL[OF α pr_poss] unfolding lhs by simp
    from r have "r ∈ fun_poss (l ⋅ τ)"
      using src_A' by auto 
    then consider "p@r ∈ possL B" | "∃a ∈ set As. p@r ∈ possL a" 
      using fun_poss_l_tau by blast
    then have "measure_ov (ll_single_redex s (p@r) α) B ≠ 0" proof(cases)
      case 1
      then show ?thesis 
        using pr_possL by (meson card_eq_0_iff disjoint_iff finite_Int finite_possL)
    next
      case 2
      then obtain Ai where Ai:"Ai ∈ set As" "p@r ∈ possL Ai"
        by blast 
      then obtain αi pi where Ai':"Ai = ll_single_redex s pi αi" and pi:"pi ∈ poss s"
        using s(1) left_lin_no_var_lhs.redex_patterns_label[OF R.ll_no_var_lhs A_wf] using As rdp_A by auto
      moreover 
      {assume neq:"(αi, pi) ≠ (α, p@r)" 
        from Ai have "Ai ∈ set (single_steps A)"
          using As rdp_A_subs_A s(1) by force 
        moreover from αpr have "ll_single_redex s (p@r) α ∈ set (single_steps A)"
          using s(1) by fastforce 
        ultimately consider "Ai = ll_single_redex s (p@r) α" | "measure_ov Ai (ll_single_redex s (p@r) α) = 0" 
          using R.single_steps_measure A_wf by meson
        then have False proof(cases)
          case 1
          then show ?thesis unfolding Ai' using single_redex_neq[OF neq pi pr_poss] by simp
        next
          case 2
          then show ?thesis
            by (meson Ai(2) card_eq_0_iff disjoint_iff finite_Int finite_possL pr_possL)
        qed
      }
      ultimately have "Ai = ll_single_redex s (p@r) α"
        by fastforce
      with Ai(1) show ?thesis 
        unfolding As using overlap by force
    qed
    with αpr have "(α, p@r) ∈ set rdp_A"
      using rdp_A by simp
    then have "(α, r) ∈ set (redex_patterns A')" 
      using rdp_A_eq_rdp_A' by auto
  }
  moreover have "source A' ⋅ σ = source (A|_p')"
    unfolding src_A' by (metis s(1) A_wf ctxt_A ctxt_eq ctxt_of_pos_term_well ctxt_supt_id l_τ_σ p' p_poss R.source_ctxt_apply_term subst_subst_compose)
  ultimately show ?thesis
    unfolding ρ_def using left_lin_no_var_lhs.proof_term_matches[OF R.ll_no_var_lhs A'_wf A_at_p'_wf lin_A'] by blast
qed

lemma A_key_lemma:"A = (ctxt_of_pos_term p' A) ⟨A' ⋅ ρ⟩"
  using A'_rho ctxt_supt_id[OF p'] by simp

lemma rho_x_wf:"ρ x ∈ wf_pterm R" 
proof(cases "x ∈ vars_term A'")
  case True
  then show ?thesis using A'_rho A_wf
    by (metis p' subst_well_def subt_at_is_wf_pterm) 
next
  case False
  then have "ρ x = Var x" 
    unfolding ρ_def match_substs_def by (simp add: mk_subst_not_mem) 
  then show ?thesis by simp
qed 

lemma source_rho:
  assumes "x ∈ vars_term (l ⋅ τ)"
  shows "(source ∘ ρ) x = σ x" 
proof-
  have "source (A' ⋅ ρ) = (source A') ⋅ σ" proof-
    have "source (A' ⋅ ρ) = s|_p"
      using A'_rho by (metis A_wf s(1) A_key_lemma ctxt_A ctxt_of_pos_term_well p' p_poss replace_at_subt_at R.source_ctxt_apply_term) 
    then show ?thesis  using l_τ_σ src_A' by simp
  qed
  then have "∀ x ∈ vars_term A'. (source ∘ ρ) x = σ x"
    using A'_wf source_apply_subst term_subst_eq_rev vars_term_source by fastforce
  then show ?thesis
    using A'_wf assms src_A' vars_term_source by force 
qed

lemma B'_src_ρ:"target B' ⋅ (source ∘ ρ) = target B' ⋅ σ"
proof-
  have "vars_term B' = vars_term (l ⋅ τ)" 
    using vars_term_source[OF B'_wf] src_B' by simp
  then have "vars_term (target B') ⊆ vars_term (l ⋅ τ)" 
    using S.vars_term_target[OF B'_wf] by simp 
  with source_rho show ?thesis
    using term_subst_eq_conv by force 
qed

end

(*Step 9 of main proof*)
lemma overlap_As'_B':
  assumes "Ai' ∈ set As'"
  shows "measure_ov Ai' B' ≠ 0"
proof-
  from assms obtain i where i:"i < length As'" and Ai':"Ai' = As' ! i"
    by (meson in_set_idx) 
  from i have i':"i < length rdp_A" 
    unfolding As'_def length_map length_zip by simp
  obtain αi pi where αipi:"(αi, pi) = rdp_A ! i"
    by (meson prod.collapse) 
  let ?Δ="ll_single_redex s pi αi"
  have ctxt:"ctxt_of_pos_term p (source (to_pterm s)) = source_ctxt (ctxt_of_pos_term p (to_pterm s))"
    by (simp add: p_poss source_ctxt_to_pterm) 
  have possL1:"possL ?Δ = {p @ q |q. q ∈ possL Ai'}" proof-
    have "(ctxt_of_pos_term p (to_pterm s))⟨Ai' ⋅ (to_pterm ∘ σ)⟩ = As ! i" 
      using As'_As[OF i'] Ai' by simp
    moreover have "As ! i = ?Δ" 
      using As i' αipi by (metis case_prod_conv nth_map)  
    ultimately have Δ1:"?Δ = (ctxt_of_pos_term p (to_pterm s))⟨Ai' ⋅ (to_pterm ∘ σ)⟩" 
      by simp
    have possL:"possL ?Δ = {p @ q |q. q ∈ possL (Ai' ⋅ (to_pterm ∘ σ))}"
      using R.label_ctxt[OF to_pterm_wf_pterm[of s R] ctxt] p_poss 
      unfolding Δ1 source_to_pterm labeled_source_simple_pterm by (simp add: p_in_poss_to_pterm)
    have wf:"Ai' ⋅ (to_pterm ∘ σ) ∈ wf_pterm R"
      by (simp add: As'_wf apply_subst_wf_pterm assms) 
    have "possL (Ai' ⋅ (to_pterm ∘ σ)) = possL Ai'" 
      using possL_apply_subst[OF wf] unfolding o_apply labeled_source_simple_pterm by auto
    with possL show ?thesis 
      by simp
  qed
  have possL2:"possL B = {p @ q |q. q ∈ possL B'}" proof-
    have possL:"possL B = {p @ q |q. q ∈ possL (B' ⋅ (to_pterm ∘ σ))}"
      using R.label_ctxt[OF to_pterm_wf_pterm[of s R] ctxt] p_poss 
      unfolding B'_in_B source_to_pterm labeled_source_simple_pterm by (simp add: p_in_poss_to_pterm)
    have wf:"B' ⋅ (to_pterm ∘ σ) ∈ wf_pterm S"
      by (simp add: B'_wf apply_subst_wf_pterm) 
    then have "possL (B' ⋅ (to_pterm ∘ σ)) = possL B'"
      using possL_apply_subst[OF wf] unfolding o_apply labeled_source_simple_pterm by auto
    with possL show ?thesis
      by simp
  qed
  from overlap have ov:"measure_ov ?Δ B ≠ 0" 
    using i' αipi by simp
  show ?thesis proof(rule ccontr)
    assume "¬ measure_ov Ai' B' ≠ 0" 
    then have "possL Ai' ∩ possL B' = {}"
      by (simp add: finite_possL)  
    with ov show False unfolding possL1 possL2
      by (smt (verit, best) card.empty disjoint_iff mem_Collect_eq same_append_eq)
  qed
qed

lemma A'_B'_sim_cp:"(A', B') ∈ sim_cp" proof-
 obtain rdp_A' where rdp_A':"redex_patterns A' = rdp_A'"
    by simp 
  have rdp_B':"redex_patterns B' = [(β, pos_diff q p)]" 
    unfolding B'_single_redex using left_lin_no_var_lhs.redex_patterns_single[OF S.ll_no_var_lhs]
    by (metis β diff_q_p_poss_renamed_α1 hole_pos_ctxt_of_pos_term hole_pos_poss l_τ)
  obtain ren_lhs_αs where ren_lhs_αs:"ren_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A')"
    by simp
  have ren_lhs_αs_alt:"ren_lhs_αs = renamed_lhs_αs" 
    unfolding ren_lhs_αs renamed_lhs_αs_def rdp_A'[symmetric] rename_list_def using rdp_A_eq
    by (simp add: map_nth_eq_conv split_beta)  
  then have hd_ren_lhs_αs:"hd ren_lhs_αs = renamed_lhs_α1"
    by (simp add: ren_lhs_α1_alt)
  let ?q="pos_diff q p" 
  let ?p="pos_diff p1 p"
  have p_hd:"?p = snd (hd rdp_A')"
    using hd_rdp_A' rdp_A' by force 
  obtain l' where l':"l' = replace_at (hd ren_lhs_αs) ?q (map_vars_term (ren_l ren) (lhs β))"
    by simp 
  have l_alt:"l = l'"
    unfolding l_def l' renamed_lhs_β_def hd_ren_lhs_αs by simp
  have overlap:"get_overlapping_part A' B' = Some A'" proof-
    have "filter (λA''. measure_ov A'' B' ≠ 0) As' = As'" 
      using overlap_As'_B' by (smt (verit, best) filter_True in_set_idx) 
    then show ?thesis using A' single_steps_A' unfolding get_overlapping_part_def 
      by (smt (verit, ccfv_threshold) option.sel)
  qed
  have pq:"?q = [] ∨ snd (hd rdp_A') = []" proof(cases "p = q")
    case True
    show ?thesis unfolding True
      using prefix_pos_diff by fast
  next
    case False
    then have p:"p = p1" 
      unfolding p_def by auto
    then show ?thesis 
      using prefix_pos_diff by (metis hd_rdp_A' less_eq_pos_simps(5) prefix_order.dual_order.eq_iff rdp_A' snd_eqD)
  qed
  have rdp_A'_alt:"map snd rdp_A' = map (λ(αi, pi). pos_diff pi p) rdp_A" proof-
    have len:"length rdp_A' = length rdp_A"
      unfolding rdp_A' rdp_A_eq by simp 
    {fix i assume i:"i < length rdp_A'"
      then obtain αi pi where αipi:"rdp_A' ! i = (αi, pi)"
        by fastforce 
      with i have "(map (λ(αi, pi). (αi, p @ pi)) rdp_A') ! i = (αi, p @ pi)"  
        by simp
      then have "map (λ(αi, pi). pos_diff pi p) (map (λ(αi, pi). (αi, p @ pi)) rdp_A') ! i = pi"
        unfolding map_map nth_map[OF i] o_apply by (metis case_prod_conv less_eq_pos_simps(1) prefix_pos_diff same_append_eq)  
      with i have "(map snd rdp_A') ! i = map (λ(αi, pi). pos_diff pi p) rdp_A ! i" 
        unfolding rdp_A' rdp_A_eq by (simp add: αipi)
    }
    with len show ?thesis
      by (metis length_map nth_equalityI)
  qed
  from tau_is_mgu have τ:"mgu_list (map2 (λx y. (x, l' |_ y)) ren_lhs_αs (map snd rdp_A')) = Some τ"
    using rdp_A'_alt ren_lhs_αs_alt l_alt by simp
  have As:"As' = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l' ⋅ τ)))
  ⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩) rdp_A' [0..<length rdp_A']"
  proof-
    have len:"length As' = length rdp_A'" 
      unfolding rdp_A'[symmetric] As'_def by (simp add: rdp_A_eq) 
    then have len':"length (zip rdp_A' [0..<length rdp_A']) = length As'" by simp
    {fix i assume i:"i < length As'" 
      then have i':"i < length (zip rdp_A [0..<length rdp_A])" 
        unfolding As'_def length_zip length_map by simp
      let ?αi="fst (rdp_A' ! i)"
      let ?pi="snd (rdp_A' ! i)" 
      obtain αi pi where αipi:"rdp_A' ! i = (αi, pi)" "?αi = αi" "?pi = pi"
        by fastforce 
      then have "rdp_A ! i = (αi, p @ pi)" 
        using rdp_A_eq i len unfolding rdp_A' by simp
      moreover then have "zip rdp_A [0..<length rdp_A] ! i = ((αi, p @ pi), i)" 
        using i unfolding As'_def length_map length_zip by auto
      ultimately have "As' ! i = (ctxt_of_pos_term pi (to_pterm (l' ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule αi)))⟩" 
        using i unfolding As'_def l_alt rdp_A' length_map length_zip nth_map[OF i']
        by (metis (no_types, lifting) case_prod_conv min.strict_boundedE p_above_pi prefix_pos_diff same_append_eq snd_conv)
      then have "As' ! i = (ctxt_of_pos_term ?pi (to_pterm (l' ⋅ τ)))⟨Prule ?αi (map (to_pterm ∘ τ) (map (rename_many' ren i) (var_rule ?αi)))⟩" 
        using αipi by simp
    }
    then show ?thesis
      using map_nth_eq_conv[OF len'] prod.collapse prod.simps(2)
      by (smt (verit, del_insts) add.left_neutral diff_zero len length_upt nth_upt nth_zip) 
  qed
  have qp_poss: "q -⇩p p ∈ poss (hd ren_lhs_αs)"
    by (simp add: diff_q_p_poss_renamed_α1 hd_ren_lhs_αs)
  have join:"join_list As' = Some A'" using A' by simp
  have B':"B' = (ctxt_of_pos_term (pos_diff q p) (to_pterm (l' ⋅ τ)))⟨Prule β (map (to_pterm ∘ τ ∘ rename_single ren) (var_rule β))⟩"
    unfolding B'_def l_alt renamed_lhs_β_def
    by (smt (verit, best) β case_prodD S.left_lin left_linear_trs_def linear_term_var_vars_term_list map_vars_term_compose vars_map_vars_term) 
  show ?thesis 
    using sim_cpI[OF A'_wf B'_wf rdp_A' rdp_B' ren_lhs_αs overlap l' pq τ As join B'] .
qed

end

(*Helper lemma for Step 10*)
lemma target_B:"target B = (ctxt_of_pos_term p s)⟨target B' ⋅ σ⟩"
  unfolding B'_in_B unfolding to_pterm_ctxt_at_pos[OF p_poss] target_to_pterm_ctxt 
  using S.target_apply_subst[OF B'_wf] by (metis B'_wf target_to_pterm S.tgt_subst_simp to_pterm_subst)

end

context ren_wf_trs
begin

(* generalized to commutation version *)
lemma okui_strongly_confluent:
 assumes closed:"⋀A B. (A, B) ∈ sim_cp ⟹ ∃v. (target A, v) ∈ (rstep S)⇧* ∧ (target B, v) ∈ mstep R"
    and mstep:"(s,t) ∈ mstep R" and rstep:"(s, u) ∈ rstep S"
  shows "∃v. (t, v) ∈ (mstep S)⇧* ∧ (u, v) ∈ mstep R"
proof-
  from mstep obtain A where A:"source A = s ∧ target A = t" "A ∈ wf_pterm R"
    using R.mstep_to_pterm R.varcond by blast 
  (*also used in Step 2 of paper proof*)
  obtain B q β where B:"source B = s ∧ target B = u" "B = ll_single_redex s q β" and q:"q ∈ poss s" and β:"to_rule β ∈ S"
    using S.rstep_exists_single_redex[OF rstep] S.varcond S.left_lin by blast 
  have B_wf:"B ∈ wf_pterm S" 
    using single_redex_wf_pterm[OF β, of q s] q β S.left_lin unfolding B(2) left_linear_trs_def by fastforce  
  show ?thesis proof(cases "measure_ov A B")
    case 0
    from measure_zero_imp_orthogonal[OF R.ll_no_var_lhs S.ll_no_var_lhs _ A(2) B_wf 0] A B
    have "A ⊥⇩p B" by auto
    from orth_imp_residual_defined[OF _ _ this A(2) B_wf]
    have "A re B ≠ None"
      using R.wf_trs_alt S.wf_trs_alt wf_trs_imp_lhs_Fun by fastforce

    with A B B_wf obtain D where d:"A re B = Some D ∧ target B = source D ∧ D ∈ wf_pterm R"
      by (metis not_Some_eq residual_src_tgt residual_well_defined) 
    from 0 have "measure_ov B A = 0" using measure_ov_symm[of A B] by simp 
    from measure_zero_imp_orthogonal[OF S.ll_no_var_lhs R.ll_no_var_lhs _ B_wf A(2) this]
    have "B ⊥⇩p A" using A B by auto
    from orth_imp_residual_defined[OF _ _ this B_wf A(2)]  
    have "B re A ≠ None" 
      using R.wf_trs_alt S.wf_trs_alt wf_trs_imp_lhs_Fun by fastforce 
    with A B B_wf obtain C where c:"B re A = Some C ∧ target A = source C ∧ C ∈ wf_pterm S"
      by (metis not_Some_eq residual_src_tgt residual_well_defined) 
    from c d A B B_wf have "target C = target D" 
      using residual_tgt_tgt by blast 
    with c d A B show ?thesis 
      using pterm_to_mstep by (metis r_into_rtrancl)
  next
    case (Suc n)
    (*Step 1*)
    obtain rdp_A where rdp_A:"rdp_A = filter (λ(α, p). measure_ov (ll_single_redex s p α)  B ≠ 0) (redex_patterns A)"
      by blast
    obtain α1 p1 where α1p1:"(α1, p1) = hd rdp_A"
      by (metis surj_pair) 
    from Suc have not_empty:"rdp_A ≠ []" 
      unfolding rdp_A by (smt (verit, del_insts) A(1) A(2) Zero_not_Suc case_prodI empty_filter_conv left_lin_no_var_lhs.measure_ov_imp_single_step_ov R.ll_no_var_lhs R.single_step_redex_patterns) 
    let ?As="map (λ(α, p). ll_single_redex s p α) rdp_A"
    have overlapping_part:"overlapping_part R S rdp_A A B s ?As α1 p1 β q"
      using overlapping_part.intro[OF ren_wf_trs_axioms] overlapping_part_axioms.intro[OF A(2) rdp_A] α1p1 not_empty A B q β by force 
    (*Step 4*)
    let ?p="overlapping_part.p p1 q"
    let ?σ="overlapping_part.σ ren rdp_A s β q" 
    (*Step 7*)
    let ?B'="overlapping_part.B' ren rdp_A α1 p1 β q"
    let ?As'="overlapping_part.As' ren rdp_A α1 p1 β q"
    obtain A' where A':"Some A'= ⨆ ?As'" and A'_wf:"A' ∈ wf_pterm R" 
      using overlapping_part.exists_A'[OF overlapping_part] by auto
    (*Step 8*)
    from overlapping_part.exists_p'[OF overlapping_part] 
    obtain p' where p':"p' ∈ poss A" and ctxt_A:"source_ctxt (ctxt_of_pos_term p' A) = ctxt_of_pos_term ?p s"
      by blast
    let ?ρ="overlapping_part.ρ A A' p'" 
    (*step 9*)
    have "(A', ?B') ∈ sim_cp"
      using overlapping_part.A'_B'_sim_cp[OF overlapping_part A' A'_wf] by auto  
    (*step 10*)
    with closed obtain v' where seq:"(target A', v') ∈ (rstep S)⇧*" and ms:"(target ?B', v') ∈ mstep R"
      by blast
    from ms obtain D' where D':"source D' = (target ?B')" "target D' = v'" "D' ∈ wf_pterm R"
      using R.mstep_to_pterm R.varcond by blast 
    let ?v="target (replace_at A p' (to_pterm v' ⋅ ?ρ))"
    let ?D="replace_at A p' (D' ⋅ ?ρ)" 
    have 1:"(t, ?v) ∈ (mstep S)⇧*" proof-
      have "target A = target (ctxt_of_pos_term p' A)⟨to_pterm (target A') ⋅ ?ρ⟩" 
        using context_target[of "(ctxt_of_pos_term p' A)"] overlapping_part.A_key_lemma[OF overlapping_part A' A'_wf p' ctxt_A] 
          R.tgt_subst_simp[OF A'_wf] by metis
      then have "(target A, ?v) ∈ (rstep S)⇧*" 
        using context_target rewrite_tgt[OF seq, of "(ctxt_of_pos_term p' A)" ?ρ] by simp
      with A(1) show ?thesis
        by (meson basic_trans_rules(31) rstep_mstep_subset rtrancl_mono) 
    qed
    have 2:"(u, ?v) ∈ mstep R" proof-
      have "source ?D = target B" proof-
        have ctxt_well:"ctxt_of_pos_term p' A ∈ wf_pterm_ctxt R" 
          using A(2) p' by (simp add: ctxt_of_pos_term_well) 
        have "target B = (ctxt_of_pos_term ?p s)⟨target ?B' ⋅ ?σ⟩"
          using overlapping_part.target_B[OF overlapping_part] .
        then show ?thesis 
          unfolding R.source_ctxt_apply_term[OF ctxt_well] source_apply_subst[OF D'(3)] D'(1) 
          unfolding overlapping_part.B'_src_ρ[OF overlapping_part A' A'_wf p' ctxt_A]
          using ctxt_A by auto
      qed
      moreover have "target ?D = ?v" 
        using D' by (metis (no_types, lifting) context_target R.tgt_subst_simp)
      moreover have "?D ∈ wf_pterm R" 
        using ctxt_wf_pterm[OF A(2) p'] apply_subst_wf_pterm[OF D'(3)] 
          overlapping_part.rho_x_wf[OF overlapping_part A' A'_wf p' ctxt_A] by force
      ultimately show ?thesis
        using B(1) pterm_to_mstep by fastforce 
    qed
    from 1 2 show ?thesis
      by auto
  qed
qed

end

lemma strongly_commute_rstep_mstep_imp_strongly_commute_mstep: 
  assumes SC: "strongly_commute (rstep S) (mstep R)" 
  shows "strongly_commute (mstep S) (mstep R)" 
  unfolding strongly_commute_def
proof (intro allI impI, elim conjE)
  fix s t u
  assume st: "(s,t) ∈ mstep S" and su: "(s,u) ∈ mstep R" 
  from st have "(s,t) ∈ (rstep S)⇧*" 
    using mstep_imp_rsteps by blast
  from this su
  show "∃ v. (t,v) ∈ (mstep R)⇧= ∧ (u,v) ∈ (mstep S)⇧*" 
  proof (induction arbitrary: u rule: converse_rtrancl_induct)
    case (base u)
    thus ?case by (intro exI[of _ u], insert st, auto)
  next
    case (step s v u)
    from SC[unfolded strongly_commute_def] ‹(s, u) ∈ mstep R› ‹(s, v) ∈ rstep S›
    obtain w where "(v,w) ∈ (mstep R)⇧=" and uw: "(u,w) ∈ (rstep S)⇧*" by blast
    hence "(v,w) ∈ mstep R" by auto
    from step.IH[OF this] obtain x where "(w, x) ∈ (mstep S)⇧*" "(t, x) ∈ (mstep R)⇧=" by auto
    thus ?case using step uw 
      by (metis mstep_rsteps_subset rstep_mstep_subset rtrancl_subset rtrancl_trans)
  qed
qed  

lemma rtrancl_mstep_rtrancl_rstep: "(mstep R)^* = (rstep R)^*"
  by (metis mstep_rsteps_subset rstep_mstep_subset rtrancl_subset)

lemma strongly_commute_rstep_mstep_iff: 
  "strongly_commute (rstep S) (mstep R) = strongly_commute (mstep S) (mstep R)" (is "?L = ?R")
proof
  show "?L ⟹ ?R" by (rule strongly_commute_rstep_mstep_imp_strongly_commute_mstep)
  assume ?R
  show ?L
  proof 
    fix s t u
    assume "(s, t) ∈ rstep S" 
      and "(s, u) ∈ mstep R"
    hence "(s,t) ∈ mstep S" by (metis rstep_imp_mstep)
    from strongly_commute_E11[OF ‹?R› this ‹(s,u) ∈ mstep R›]
    show "∃z. (t, z) ∈ (mstep R)⇧= ∧ (u, z) ∈ (rstep S)⇧*" 
      unfolding rtrancl_mstep_rtrancl_rstep by blast
  qed
qed
      
section"Main Theorems"

theorem okui_imp_commutation:
  assumes R_wf:"left_lin_wf_trs R" and S_wf: "left_lin_wf_trs S" 
  and closed:"⋀A B. (A, B) ∈ ren.sim_cp ren R S ⟹ ∃v. (target A, v) ∈ (rstep S)⇧* ∧ (target B, v) ∈ mstep R"
shows okui_imp_commute: "commute (rstep R) (rstep S)"
  and okui_imp_strongly_commute_rstep_mstep: "strongly_commute (rstep S) (mstep R)" 
  and okui_imp_strongly_commute: "strongly_commute (mstep S) (mstep R)" 
proof -
  interpret ren_wf_trs ren R S
    using R_wf S_wf unfolding ren_wf_trs_def by auto
  show SC: "strongly_commute (rstep S) (mstep R)" 
    unfolding strongly_commute_def
    using okui_strongly_confluent[OF closed]
    by (metis Un_iff mstep_rsteps_subset rstep_mstep_subset rtrancl_subset)
  show "strongly_commute (mstep S) (mstep R)" 
    by (rule strongly_commute_rstep_mstep_imp_strongly_commute_mstep[OF SC])
  from SC have "commute (rstep S) (mstep R)" 
    by (rule strongly_commute_imp_commute)
  hence "commute (rstep S) (rstep R)" 
    unfolding commute_def rtrancl_mstep_rtrancl_rstep by auto
  thus "commute (rstep R) (rstep S)" by (simp add: commuteE commuteI)
qed

corollary strongly_commute_iff_sim_cps_joinable:
  assumes R_wf:"left_lin_wf_trs R" and S_wf: "left_lin_wf_trs S" 
  shows "strongly_commute (mstep S) (mstep R) ⟷ 
    (∀ A B. (A,B) ∈ ren.sim_cp ren R S ⟶ (∃v. (target A, v) ∈ (rstep S)⇧* ∧ (target B, v) ∈ mstep R))"
   (is "?L = ?R")
proof 
  interpret ren_wf_trs ren R S using R_wf S_wf
    by (metis R_wf S_wf ren_wf_trs.intro)
  show "?R ⟹ ?L" using okui_imp_strongly_commute[OF R_wf S_wf] by auto
  assume ?L
  show ?R
  proof (intro allI impI)
    fix A B
    assume sim_cp: "(A,B) ∈ ren.sim_cp ren R S" 
    from sim_cp_co_init[OF sim_cp] have src:"source A = source B" .
    from sim_cp have "A ∈ wf_pterm R" and "B ∈ wf_pterm S" 
      unfolding ren.sim_cp_def by fastforce+
    then have "(source A, target A) ∈ mstep R" and "(source B, target B) ∈ mstep S"
      by (simp add: pterm_to_mstep)+
    with ‹?L› src obtain v where 1:"(target A, v) ∈ (mstep S)⇧*" and 2:"(target B, v) ∈ (mstep R)⇧=" 
      unfolding strongly_commute_def by metis  
    from 1 have "(target A, v) ∈ (rstep S)⇧*" unfolding rtrancl_mstep_rtrancl_rstep . 
    with 2 show "∃v. (target A, v) ∈ (rstep S)⇧* ∧ (target B, v) ∈ mstep R"
      by force
  qed
qed

corollary strongly_confluent_iff_sim_cps_joinable:
  assumes wf:"left_lin_wf_trs R"  
  shows "strongly_confluent (mstep R)  ⟷ 
    (∀ A B. (A,B) ∈ ren.sim_cp ren R R ⟶ (∃v. (target A, v) ∈ (rstep R)⇧* ∧ (target B, v) ∈ mstep R))"
    (is "_ ⟷ ?joinable")
proof -
  have "?joinable ⟷ strongly_commute (mstep R) (mstep R)" 
    using strongly_commute_iff_sim_cps_joinable[OF wf wf, of ren] by simp
  also have "… ⟷ strongly_confluent (mstep R)"
    by (meson iso_tuple_UNIV_I strongly_commute_def strongly_confluentI strongly_confluent_on_E11)
  finally show ?thesis ..
qed


theorem okui_imp_CR:
  assumes R_wf:"left_lin_wf_trs R"
  and closed:"⋀A B. (A, B) ∈ ren.sim_cp ren R R ⟹ ∃v. (target A, v) ∈ (rstep R)⇧* ∧ (target B, v) ∈ mstep R"
  shows "CR (rstep R)"
proof-
  from okui_imp_commute[OF R_wf R_wf closed]
  have "commute (rstep R) (rstep R)" by auto
  thus "CR (rstep R)"
    by (simp add: CR_iff_self_commute)
qed

declare ren.rename_list_def[code]

end