Theory Redex_Patterns

section‹Redex Patterns›

theory Redex_Patterns
imports
  Labels_and_Overlaps    
begin

text‹Collect all rule symbols of a proof term together with the position in its source where they 
appear. This is used to split a proof term into a set of single steps, whose union 
(@{const join_list}) is the whole proof term again. 

The redex patterns are collected in leftmost outermost order.›

fun redex_patterns :: "('f, 'v) pterm ⇒ (('f, 'v) prule × pos) list"
  where
  "redex_patterns (Var x) = []" 
| "redex_patterns (Pfun f ss) = concat (map (λ (i, rps). map (λ (α, p). (α, i#p)) rps)
    (zip [0 ..< length ss] (map redex_patterns ss)))"
| "redex_patterns (Prule α ss) = (α, []) # concat (map (λ (p1, rps). map (λ (α, p2). (α, p1@p2)) rps)
    (zip (var_poss_list (lhs α)) (map redex_patterns ss)))"

interpretation lexord_linorder: 
  linorder "ord.lexordp_eq ((<) :: nat ⇒ nat ⇒ bool)" 
           "ord.lexordp ((<) :: nat ⇒ nat ⇒ bool)"
  using linorder.lexordp_linorder[OF linorder_class.linorder_axioms] by simp

lemma lexord_prefix_diff:
  assumes "(ord.lexordp ((<) :: nat ⇒ nat ⇒ bool)) xs ys" and "¬ prefix xs ys" 
  shows "(ord.lexordp (<)) (xs@us) (ys@vs)" 
using assms proof(induct xs arbitrary:ys)
  case (Cons x xs')
  from Cons(2) obtain y ys' where ys:"ys = y#ys'"
    by (metis list.exhaust_sel ord.lexordp_simps(2)) 
  consider "x < y" | "x = y ∧ ord.lexordp (<) xs' ys'" 
    using Cons(2) ord.lexordp_eq.simps unfolding Cons ys by force 
  then show ?case proof(cases)
    case 1
    then show ?thesis unfolding ys by simp
  next
    case 2
    with Cons(3) have "¬ prefix xs' ys'" 
      unfolding ys by simp 
    with Cons(1) 2 have "(ord.lexordp (<)) (xs'@us) (ys'@vs)"
      by auto 
    then show ?thesis unfolding ys using 2 by simp
  qed
qed simp

lemma var_poss_list_sorted: "sorted_wrt (ord.lexordp ((<) :: nat ⇒ nat ⇒ bool)) (var_poss_list t)"
proof(induct t)
  case (Fun f ts)
  let ?poss="(map2 (λi. map ((#) i)) [0..<length ts] (map var_poss_list ts))"
  {fix i j assume i:"i < length (var_poss_list (Fun f ts))" and j:"j < i"
    let ?p="concat ?poss ! i" 
    let ?q="concat ?poss ! j"
    from i obtain i' i'' where p:"?p = ?poss!i'!i''" and i':"i' < length ts" and i'':"i'' < length (?poss!i')"
        and i_sum:"i = sum_list (map length (take i' ?poss)) + i''"
      using less_length_concat[OF i[unfolded var_poss_list.simps]] unfolding length_map by auto
    from p have p2:"?p = i'# (var_poss_list (ts!i') ! i'')" 
      using i' i'' by simp
    from j obtain j' j'' where q:"?q = ?poss!j'!j''" and j':"j' < length ts" and j'':"j'' < length (?poss!j')"
        and j_sum:"j = sum_list (map length (take j' ?poss)) + j''"
      using less_length_concat i j length_map unfolding var_poss_list.simps
      by (smt (verit, ccfv_threshold) diff_le_self length_take length_upt length_zip map_upt_len_conv order.strict_trans take_all) 
    from q have q2:"?q = j'# (var_poss_list (ts!j') ! j'')" 
      using j' j'' by simp
    have "(ord.lexordp (<)) (var_poss_list (Fun f ts) ! j) (var_poss_list (Fun f ts) ! i)" proof(cases "i' = j'")
      case True
      have l:"length (map2 (λx. map ((#) x)) [0..<length ts] (map var_poss_list ts) ! j') = length (var_poss_list (ts!j'))" 
        using j' by auto
      from True j j_sum i_sum have "j'' < i''"
        using nat_add_left_cancel_less by blast 
      with Fun(1)[of "ts!j'"] i' i'' j'' have "(ord.lexordp (<)) (var_poss_list (ts!j') ! j'') (var_poss_list (ts!i') ! i'')"
        unfolding True l by (simp add: sorted_wrt_iff_nth_less)  
      then have "(ord.lexordp (<)) ?q ?p" 
        unfolding p2 q2 True by simp
      then show ?thesis unfolding var_poss_list.simps by fastforce
    next
      case False
      then have "j' < i'"
        using  i'' i' j' i_sum j_sum sum_list_less[OF j]
        by (smt (verit, best) i j le_neq_implies_less length_concat linorder_le_less_linear not_add_less1 order.strict_trans take_all var_poss_list.simps(2))
      then have "(ord.lexordp (<)) ?q ?p" 
        unfolding p2 q2 by simp
      then show ?thesis unfolding var_poss_list.simps by fastforce
    qed
  }
  then show ?case
    using sorted_wrt_iff_nth_less by blast
qed simp
  
context left_lin_no_var_lhs
begin

lemma redex_patterns_sorted:
  assumes  "A ∈ wf_pterm R"
  shows "sorted_wrt (ord.lexordp (<)) (map snd (redex_patterns A))"
proof-
  {fix i j assume "i < j" "j < length (redex_patterns A)" 
    with assms have "(ord.lexordp (<)) (snd (redex_patterns A ! i)) (snd (redex_patterns A ! j))"
    proof(induct A arbitrary: i j)
      case (2 As f)
      let ?poss="map2 (λi. map (λ(α, p). (α, i # p))) [0..<length As] (map redex_patterns As)"
      from 2(2,3) obtain α p1 where ap:"redex_patterns (Pfun f As) ! i = (α, p1)"
        by (metis surj_pair) 
      from 2(3) obtain β p2 where bp:"redex_patterns (Pfun f As) ! j = (β, p2)"
        by (metis surj_pair) 
      have l:"length (zip [0..<length As] (map redex_patterns As)) = length As" by simp
      from 2(2,3) have *:"i < length (concat ?poss)" by simp
      from ap obtain i' i'' where ap1:"(α, p1) = ?poss!i'!i''" and i':"i' < length As" and i'':"i'' < length (?poss!i')"
        and i:"i = sum_list (map length (take i' ?poss)) + i''"
        unfolding redex_patterns.simps using less_length_concat[OF *] by (metis l length_map)
      have poss_i':"?poss!i' = map (λ(α, p). (α, i' # p)) (redex_patterns (As!i'))"
        using i' nth_zip[of i'] by fastforce  
      from ap1 i'' obtain p1' where p1':"p1 = i'#p1'" "(α, p1') = redex_patterns (As!i') ! i''"  
        unfolding poss_i' by (smt (z3) case_prod_conv length_map nth_map old.prod.inject surj_pair) 
      from bp obtain j' j'' where ap2:"(β, p2) = ?poss!j'!j''" and j':"j' < length As" and j'':"j'' < length (?poss!j')"
        and j:"j = sum_list (map length (take j' ?poss)) + j''"
        unfolding redex_patterns.simps using less_length_concat[OF 2(3)[unfolded redex_patterns.simps]] by (metis l length_map)
      have poss_j':"?poss!j' = map (λ(α, p). (α, j' # p)) (redex_patterns (As!j'))"
        using j' nth_zip[of j'] by fastforce  
      from ap2 j'' obtain p2' where p2':"p2 = j'#p2'" "(β, p2') = redex_patterns (As!j') ! j''"  
        unfolding poss_j' by (smt (z3) case_prod_conv length_map nth_map old.prod.inject surj_pair) 
      show ?case proof(cases "i' = j'")
        case True
        from i j 2 have "i'' < j''" unfolding True by linarith
        moreover from j'' have "j'' < length (redex_patterns (As!j'))" unfolding poss_j' by auto    
        ultimately have "ord.lexordp (<) p1' p2'" using  2(1) j' True p1'(2) p2'(2) by (metis nth_mem snd_eqD)
        then show ?thesis unfolding ap bp p1' p2' True by auto
      next
        case False
        with 2(2) i j have "i' < j'" using sum_list_less[OF 2(2)] i' j' j''
          by (smt (verit, best) "*" "2.prems"(2) le_neq_implies_less length_concat linorder_le_less_linear not_add_less1 redex_patterns.simps(2) take_all)
        then show ?thesis unfolding ap bp p1' p2' by fastforce 
      qed
    next
      case (3 γ As)
      from 3(2,3) obtain α p1 where ap:"redex_patterns (Prule γ As) ! i = (α, p1)"
        by (metis surj_pair) 
      from 3(3) obtain β p2 where bp:"redex_patterns (Prule γ As) ! j = (β, p2)"
        by (metis surj_pair) 
      show ?case proof(cases "i")
        case 0
        from 3(1) no_var_lhs obtain f ts where lhs:"lhs γ = Fun f ts"
          by fastforce 
        from bp 3(4) 0 obtain j' where "concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As)) ! j' = (β, p2)" 
          "j' < length (concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As)))" 
          unfolding redex_patterns.simps using "3.prems"(2) by force
        then obtain j1 j2 where j1:"j1 < length (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As))" 
            and j2:"j2 < length (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As) ! j1)"
            and j1j2:"(map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As) ! j1) ! j2 = (β, p2)" 
          using nth_concat_split by metis 
        let ?p'="var_poss_list (lhs γ)!j1" 
        let ?rdp="(map redex_patterns As ! j1)" 
        from j1 have zip:"zip (var_poss_list (lhs γ)) (map redex_patterns As) ! j1 = (?p', ?rdp)" 
          unfolding length_map length_zip using nth_zip by force
        with j1j2 have "(β, p2) = map (λ(α, p2). (α, ?p' @ p2)) ?rdp !j2" 
          using nth_map j1 unfolding length_map by force
        moreover from j2 have "j2 < length (map (λ(α, p2). (α, ?p' @ p2)) ?rdp)" 
          unfolding nth_map[OF j1[unfolded length_map]] zip by force
        ultimately have "(β, p2) ∈ set (map (λ(α, p2). (α, ?p' @ p2)) ?rdp)" 
          by simp
        moreover have "?p' ≠ []" proof-
          from j1 have "?p' ∈ var_poss (lhs γ)"  
            unfolding length_map length_zip using nth_mem by fastforce
          then show ?thesis unfolding lhs var_poss.simps by force 
        qed
        ultimately have "p2 ≠ []"
          by auto 
        moreover from 0 ap have "p1 = []" by simp
        ultimately show ?thesis unfolding ap bp by simp
      next
        case (Suc n)
        let ?poss="(map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As))"
        from 3(1,2) have l:"length (var_poss_list (lhs γ)) = length As" 
          using linear_term_var_vars_term_list left_lin unfolding left_linear_trs_def using length_var_poss_list length_var_rule by auto  
        from 3(4,5) have *:"n < length (concat ?poss)" unfolding Suc by simp
        from ap have "concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As)) ! n = (α, p1)" 
          unfolding Suc by simp
        then obtain i' i'' where ap1:"(α, p1) = ?poss!i'!i''" and i':"i' < length ?poss" and i'':"i'' < length (?poss!i')"
          and n:"n = sum_list (map length (take i' ?poss)) + i''"
          using less_length_concat[OF *] by metis
        from i' have i'2:"i' < length (var_poss_list (lhs γ))" by simp
        obtain p11 where p11:"?poss!i' = map (λ(α, p). (α, p11 @ p)) (redex_patterns (As!i'))" "var_poss_list (lhs γ) !i' = p11" 
          using i' nth_zip[of i'] by fastforce  
        from ap1 i'' obtain p12 where p12:"p1 = p11@p12" "(α, p12) = redex_patterns (As!i') ! i''"  
          unfolding p11 by (smt (z3) case_prod_conv length_map nth_map old.prod.inject surj_pair) 
        from 3(4,5) Suc obtain n' where j:"j = Suc n'" by (meson Suc_lessE) 
        from 3(5) have *:"n' < length (concat ?poss)" unfolding j by simp
        from bp have "concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs γ)) (map redex_patterns As)) ! n' = (β, p2)" 
          unfolding j by simp
        then obtain j' j'' where ap2:"(β, p2) = ?poss!j'!j''" and j':"j' < length ?poss" and j'':"j'' < length (?poss!j')"
          and n':"n' = sum_list (map length (take j' ?poss)) + j''"
          using less_length_concat[OF *] by metis
        from j' have j'2:"j' < length (var_poss_list (lhs γ))" by simp
        obtain p21 where p21:"?poss!j' = map (λ(α, p). (α, p21 @ p)) (redex_patterns (As!j'))" "var_poss_list (lhs γ) !j' = p21" 
          using j' nth_zip[of j'] by fastforce  
        from ap2 j'' obtain p22 where p22:"p2 = p21@p22" "(β, p22) = redex_patterns (As!j') ! j''"  
         unfolding p21 by (smt (z3) case_prod_conv length_map nth_map old.prod.inject surj_pair) 
        show ?thesis proof(cases "i' = j'")
          case True
          from n n' 3(4) have ij:"i'' < j''" unfolding True Suc j by linarith
          moreover from j'' have "j'' < length (redex_patterns (As!j'))" unfolding p21 by auto 
          moreover from j' l have "j' < length As" unfolding length_map by simp
          ultimately have "ord.lexordp (<) p12 p22" using 3(3) p22 p12 j' unfolding True by (metis nth_mem snd_conv)
          with p21(2) p11(2) show ?thesis unfolding ap bp p22 p12 True by (simp add: ord.lexordp_append_leftI)  
        next
          case False
          then have "i' < j'"
            using  sum_list_less[OF 3(4), where i'=i' and j'=j']
            by (smt (verit) "3.prems"(1) Suc Suc_less_SucD i' j j' j'' le_neq_implies_less n n' sum_list_less)
          then have "ord.lexordp (<) p11 p21" 
            using p11(2) p21(2) var_poss_list_sorted[of "lhs γ"] i'2 j'2 using sorted_wrt_nth_less by blast 
          moreover have "¬ prefix p11 p21" proof-
            from False j' i' have "parallel_pos (var_poss_list (lhs γ) !i') (var_poss_list (lhs γ) !j')"
              unfolding length_map length_zip using var_poss_parallel var_poss_list_sound distinct_var_poss_list 
              by (metis l min.idem nth_eq_iff_index_eq nth_mem)
            then show ?thesis using p11(2) p21(2)
              by (metis less_eq_pos_simps(1) parallel_pos prefix_def)
          qed
          ultimately show ?thesis unfolding ap bp p12 p22 using lexord_prefix_diff by simp
        qed
      qed
    qed simp
  }
  then show ?thesis
    by (metis (mono_tags, lifting) sorted_wrt_iff_nth_less sorted_wrt_map) 
qed

corollary distinct_snd_rdp:
  assumes "A ∈ wf_pterm R"
  shows "distinct (map snd (redex_patterns A))" 
  using redex_patterns_sorted[OF assms] lexord_linorder.strict_sorted_iff by simp

lemma redex_patterns_equal:
  assumes wf:"A ∈ wf_pterm R" 
    and sorted:"sorted_wrt (ord.lexordp (<)) (map snd xs)" and eq:"set xs = set (redex_patterns A)"
  shows "xs = redex_patterns A" 
proof-
  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 xs = map snd (redex_patterns A)" 
    using linorder.strict_sorted_equal[OF linord redex_patterns_sorted[OF wf] sorted] eq by simp
  with eq distinct_snd_rdp[OF wf] show ?thesis 
    using distinct_map by (metis (mono_tags, opaque_lifting) inj_onD list.inj_map_strong) 
qed

lemma redex_patterns_order:
  assumes "A ∈ wf_pterm R" and "i < j" and "j < length (redex_patterns A)" 
    and "redex_patterns A ! i = (α, p1)" and "redex_patterns A ! j = (β, p2)"
  shows "¬ p2 ≤⇩_p p1" 
proof-
  have "(ord.lexordp (<)) p1 p2 " 
    using redex_patterns_sorted[OF assms(1)] assms sorted_wrt_nth_less by fastforce 
  then show ?thesis
    by (metis less_eq_pos_def lexord_linorder.less_le_not_le ord.lexordp_eq_pref) 
qed

end

context left_lin_no_var_lhs
begin 
lemma redex_patterns_label:
  assumes "A ∈ wf_pterm R"
  shows "(α, p) ∈ set (redex_patterns A) ⟷ p ∈ poss (source A) ∧ get_label (labeled_source A |_ p) = Some (α, 0)"
proof
  {assume "(α, p) ∈ set (redex_patterns A)"
    with assms show "p ∈ poss (source A) ∧ get_label (labeled_source A |_ p) = Some (α, 0)" proof(induct arbitrary:p)
      case (2 ts f)
      have l:"length (map2 (λi. map (λ(α, p). (α, i # p))) [0..<length ts] (map redex_patterns ts)) = length ts" 
        unfolding length_map length_zip by simp
      with 2(2) obtain i where i:"i < length ts" and ap:"(α, p) ∈ set ((map2 (λi. map (λ(α, p). (α, i # p))) [0..<length ts] (map redex_patterns ts))!i)" 
        unfolding redex_patterns.simps using in_set_idx by (metis nth_concat_split nth_mem) 
      have "(map2 (λi. map (λ(α, p). (α, i # p))) [0..<length ts] (map redex_patterns ts))!i = map (λ(α, p). (α, i # p)) (redex_patterns (ts!i))" 
        using nth_zip i by fastforce
      with ap obtain p' where p':"p = i#p'" and "(α, p') ∈ set (redex_patterns (ts !i))" by auto 
      with 2(1) i have "p' ∈ poss (source (ts!i))" and "get_label (labeled_source (ts!i)|_p') = Some (α, 0)"
        using nth_mem by blast+
      with i show ?case unfolding p' by simp
    next
      case (3 β As)
      from no_var_lhs 3(1) obtain f ts where lhs:"lhs β = Fun f ts" by fastforce 
      from 3(2) have l:"length (var_poss_list (lhs β)) = length As" 
        using left_lin.length_var_rule[OF left_lin_axioms 3(1)] by (simp add: length_var_poss_list) 
      from 3(4) consider (root) "(α, p) = (β, [])" | (arg) "(α, p) ∈ set (concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs β)) (map redex_patterns As)))" 
        unfolding redex_patterns.simps by (meson set_ConsD) 
      then show ?case proof(cases)
        case root
        then have "α = β" and "p = []" by simp+
        then show ?thesis by (simp add: lhs) 
      next
        case arg
        then obtain i where i:"i < length As" and ap:"(α, p) ∈ set ((map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs β)) (map redex_patterns As))!i)" 
          using in_set_idx l by (metis (no_types, lifting) length_map map_snd_zip nth_concat_split nth_mem)
        let ?p1="(var_poss_list (lhs β))!i" 
        have "(map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs β)) (map redex_patterns As))!i = map (λ(α, p). (α, ?p1 @ p)) (redex_patterns (As!i))" 
          using nth_zip i l by fastforce
        with ap obtain p2 where p2:"p = ?p1@p2" and ap2:"(α, p2) ∈ set (redex_patterns (As !i))" by auto 
        with 3(3) i have poss:"p2 ∈ poss (source (As!i))" and label:"get_label (labeled_source (As!i)|_p2) = Some (α, 0)"
          using nth_mem by blast+
        have p1_poss:"?p1 ∈ poss (lhs β)" using i l
          by (metis nth_mem var_poss_imp_poss var_poss_list_sound) 
        then have 1:"p ∈ poss (source (Prule β As))" 
          using poss 3(2) i l unfolding source.simps p2 
          by (smt (verit, ccfv_SIG)  append_eq_append_conv2 comp_apply length_map length_remdups_eq length_rev length_var_poss_list nth_map poss_append_poss poss_imp_subst_poss rev_swap var_rule_pos_subst vars_term_list_var_poss_list)
        have "labeled_source (Prule β As) |_p = labeled_source (As!i) |_p2" proof-
          have "(⟨map labeled_source As⟩⇩β) (var_rule β ! i) = labeled_source (As!i)" 
            using i 3(2) by (metis length_map lhs_subst_var_i nth_map) 
          moreover have "labeled_lhs β |_ ?p1 = Var (var_rule β ! i)"
            using 3(1) i l by (metis case_prodD left_lin left_linear_trs_def length_var_poss_list linear_term_var_vars_term_list p1_poss var_label_term vars_term_list_var_poss_list) 
          ultimately show ?thesis unfolding p2 labeled_source.simps
            by (smt (verit, best) eval_term.simps(1) label_term_to_term p1_poss poss_imp_subst_poss poss_term_lab_to_term subt_at_append subt_at_subst)
        qed
        with label have 2:"get_label (labeled_source (Prule β As)|_p) = Some (α, 0)"
          by presburger
        from 1 2 show ?thesis by simp
      qed 
    qed simp
  }
  {assume "p ∈ poss (source A) ∧ get_label (labeled_source A |_ p) = Some (α, 0)"
    with assms show "(α, p) ∈ set (redex_patterns A)" proof(induct arbitrary:p)
      case (2 ts f)
      from 2(2) have "p ≠ []" unfolding labeled_source.simps by auto 
      with 2(2) obtain i p' where p':"p = i#p'" "p' ∈ poss (source (ts!i))" and i:"i < length ts"
        unfolding source.simps by fastforce
      with 2(2) have "get_label (labeled_source (ts!i) |_ p') = Some (α, 0)" 
        unfolding p' labeled_source.simps by auto 
      with 2(1) i p' have IH:"(α, p') ∈ set (redex_patterns (ts!i))"
        using nth_mem by blast 
      from i have i_zip:"i < length (zip [0..<length ts] (map redex_patterns ts))" by simp 
      from i have "zip [0..<length ts] (map redex_patterns ts) ! i = (i, redex_patterns (ts!i))" 
        using nth_zip by simp
      then have "(map2 (λx. map (λ(α, p). (α, x # p))) [0..<length ts] (map redex_patterns ts)) ! i = map (λ(α, p). (α, i # p)) (redex_patterns (ts!i))"
        unfolding nth_map[OF i_zip] by simp
      with p'(2) IH have "(α, p) ∈ set ((map2 (λi. map (λ(α, p). (α, i # p))) [0..<length ts] (map redex_patterns ts))!i)"
        unfolding p' by auto 
      with i_zip show ?case using i unfolding redex_patterns.simps set_concat by (metis (no_types, lifting) UN_I length_map nth_mem)  
    next
      case (3 β As)
      with get_label_Prule consider (1)"p = [] ∧ α = β" | "(∃p1 p2 i. p = p1 @ p2 ∧ i < length As ∧ var_poss_list (lhs β) ! i = p1 
          ∧ p2 ∈ poss (source (As ! i)) ∧ get_label (labeled_source (As ! i) |_ p2) = Some (α, 0))"
        by (metis wf_pterm.intros(3))
      then show ?case proof(cases)
        case 1
        then show ?thesis unfolding redex_patterns.simps by simp
      next
        case 2
        from 3(1,2) left_lin have l:"length (var_poss_list (lhs β)) = length As"
          using length_var_poss_list length_var_rule by auto 
        from 2 obtain p1 p2 i where p:"p = p1 @ p2" and i:"i < length As" and p1:"var_poss_list (lhs β) ! i = p1" 
          and p2:"p2 ∈ poss (source (As ! i))" and lab:"get_label (labeled_source (As ! i) |_ p2) = Some (α, 0)"
          by blast
        from i l have i':"i < length (zip (var_poss_list (lhs β)) (map redex_patterns As))" by simp
        from i p2 lab 3(3) have "(α, p2) ∈ set (redex_patterns (As!i))" using nth_mem by blast  
        then have "(α, p) ∈ set (map (λ(α, p2). (α, p1 @ p2)) (redex_patterns (As!i)))" using p by force  
        then have "(α, p) ∈ set ((map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs β)) (map redex_patterns As))!i)" 
          unfolding nth_map[OF i'] p using p1 by (simp add: i l) 
        then have "(α, p) ∈ set (concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs β)) (map redex_patterns As)))"
          unfolding set_concat by (metis (no_types, lifting) UN_I i' length_map nth_mem) 
        then show ?thesis unfolding redex_patterns.simps by (meson list.set_intros(2))
      qed
    qed simp
   }
 qed

lemma redex_pattern_rule_symbol:
  assumes "A ∈ wf_pterm R" "(α, p) ∈ set (redex_patterns A)" 
  shows "to_rule α ∈ R" 
proof-
  from redex_patterns_label[OF assms(1)] have "p ∈ poss (source A)" and "get_label (labeled_source A |_ p) = Some (α, 0)" 
    using assms(2) by simp+
  then show ?thesis
    using assms(1) labeled_wf_pterm_rule_in_TRS by fastforce 
qed

lemma redex_patterns_subset_possL:
  assumes "A ∈ wf_pterm R"
  shows "set (map snd (redex_patterns A)) ⊆ possL A"
  using redex_patterns_label[OF assms]
  by (smt (verit) get_label_imp_labelposs imageE labeled_source_to_term list.set_map option.simps(3) poss_term_lab_to_term prod.collapse subsetI)  
end

lemma redex_poss_empty_imp_empty_step:
  assumes "redex_patterns A = []"
  shows "is_empty_step A" 
  using assms proof(induct A)
  case (Pfun f As)
  {fix i assume i:"i < length As" 
    then have i_zip:"i < length (zip [0..<length As] (map redex_patterns As))" by simp  
    {fix x xs assume "redex_patterns (As!i) = x#xs"
      with i have "zip [0..<length As] (map redex_patterns As) ! i = (i, x#xs)" by simp
      then have "(map2 (λi. map (λ(α, p). (α, i # p))) [0..<length As] (map redex_patterns As))!i ≠ []" 
        using nth_map i_zip by simp
      with Pfun(2) have False unfolding redex_patterns.simps using i_zip concat_nth_length
        by (metis (no_types, lifting) length_0_conv length_greater_0_conv length_map less_nat_zero_code)
    }
    then have "redex_patterns (As!i) = []"
      by (meson list.exhaust) 
    with Pfun(1) i have "is_empty_step (As!i)"
      by simp
  }
  then show ?case 
    by (simp add: list_all_length) 
qed simp_all

lemma overlap_imp_redex_poss:
  assumes "A ∈ wf_pterm R" "B ∈ wf_pterm R" 
    and "measure_ov A B ≠ 0"
  shows "redex_patterns A ≠ []"
proof
  assume "redex_patterns A = []"
  then have "is_empty_step A"
    by (simp add: redex_poss_empty_imp_empty_step) 
  with assms(3) show False
    by (simp add: empty_step_imp_measure_zero) 
qed

lemma redex_patterns_to_pterm:
  shows "redex_patterns (to_pterm s) = []" 
proof(induct s)
  case (Fun f ts)
  have l:"length (map2 (λi. map (λ(α, p). (α, i # p))) [0..<length (map to_pterm ts)] (map redex_patterns (map to_pterm ts))) = length ts"
    by simp
  {fix i assume "i < length ts"
    with Fun have "(map2 (λi. map (λ(α, p). (α, i # p))) [0..<length (map to_pterm ts)] (map redex_patterns (map to_pterm ts)))!i = []" 
      by simp
  }
  with l show ?case unfolding to_pterm.simps redex_patterns.simps
    by (metis length_greater_0_conv length_nth_simps(1) less_nat_zero_code nth_concat_split)
qed simp

(*some of this might make older lemmas about labeled_pos/Possl redundant*)
lemma redex_patterns_elem_fun:
  assumes "(α, p) ∈ set (redex_patterns (Pfun f As))"
  shows "∃i p'. i < length As ∧ p = i#p' ∧ (α, p') ∈ set (redex_patterns (As!i))" 
proof-
  let ?xs="map2 (λi. map (λ(α, p). (α, i # p))) [0..<length As] (map redex_patterns As)"
  from assms obtain k where k:"k < length (redex_patterns (Pfun f As))" "redex_patterns (Pfun f As) ! k = (α, p)"
    by (metis in_set_idx)
  then obtain i j where "i < length ?xs" and j:"j < length (?xs!i)" "?xs ! i ! j = (α, p)" 
    using nth_concat_split[OF k(1)[unfolded redex_patterns.simps]] by force  
  then have i:"i < length As" by auto 
  then have "zip [0..<length As] (map redex_patterns As) !i = (i, redex_patterns (As!i))" 
    using nth_zip by auto
  then have "?xs!i = map (λ(α, p). (α, i#p)) (redex_patterns (As!i))" using nth_map i by auto
  with j obtain p' where "p = i#p'" and "(α, p') ∈ set (redex_patterns (As!i))"
    by (smt (verit, ccfv_threshold) case_prod_beta fst_conv imageE list.set_map nth_mem prod.collapse snd_conv) 
  with i show ?thesis by simp
qed

lemma redex_patterns_elem_rule:
  assumes "(α, p) ∈ set (redex_patterns (Prule β As))"
  shows "p = [] ∨ (∃i p'. i < length As ∧ i < length (var_poss_list (lhs β)) 
       ∧ p = (var_poss_list (lhs β)!i)@p' ∧ (α, p') ∈ set (redex_patterns (As!i)))" 
proof-
  let ?xs="map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs β)) (map redex_patterns As)"
  from assms obtain k where k:"k < length (redex_patterns (Prule β As))" "redex_patterns (Prule β As) ! k = (α, p)"
    by (metis in_set_idx)
  show ?thesis proof(cases "p = []")
    case False 
    with k have "k ≠ 0" 
      unfolding redex_patterns.simps by (metis nth_Cons_0 prod.inject) 
    with k obtain i j where "i < length ?xs" and j:"j < length (?xs!i)" "?xs ! i ! j = (α, p)" 
      using nth_concat_split less_Suc_eq_0_disj unfolding redex_patterns.simps by force
    then have i:"i < length As" "i < length (var_poss_list (lhs β))" by auto 
    let ?p="(var_poss_list (lhs β))!i"
    from i have "zip (var_poss_list (lhs β)) (map redex_patterns As) !i = (?p, redex_patterns (As!i))" 
      using nth_zip by auto
    then have "?xs!i = map (λ(α, p). (α, ?p@p)) (redex_patterns (As!i))" using nth_map i by auto
    with j obtain p' where "p = ?p@p'" and "(α, p') ∈ set (redex_patterns (As!i))"
      by (smt (verit, ccfv_threshold) case_prod_beta fst_conv imageE list.set_map nth_mem prod.collapse snd_conv) 
    with i show ?thesis by blast
  qed simp
qed

lemma redex_patterns_elem_fun':
  assumes "(α, p) ∈ set (redex_patterns (As!i))" and i:"i < length As"
  shows "(α, i#p) ∈ set (redex_patterns (Pfun f As))" 
proof-
  let ?xs="map2 (λi. map (λ(α, p). (α, i # p))) [0..<length As] (map redex_patterns As)"
  from i have "zip [0..<length As] (map redex_patterns As) !i = (i, redex_patterns (As!i))" 
    using nth_zip by auto
  then have "?xs!i = map (λ(α, p). (α, i#p)) (redex_patterns (As!i))" using nth_map i by auto
  with assms have "(α, i#p) ∈ set (?xs!i)" by fastforce 
  moreover from i have "i < length ?xs" by simp
  ultimately have *:"(α, i#p) ∈ set (concat ?xs)" 
    unfolding set_concat by (meson UN_iff nth_mem) 
  then show ?thesis by simp
qed

lemma redex_patterns_elem_rule':
  assumes "(β, p) ∈ set (redex_patterns (As!i))" and i:"i < length As" "i < length (var_poss_list (lhs α))"
  shows "(β, (var_poss_list (lhs α) ! i)@p) ∈ set (redex_patterns (Prule α As))" 
proof-
  let ?xs="map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs α)) (map redex_patterns As)"
  let ?p="var_poss_list (lhs α) ! i"
  from i have "zip (var_poss_list (lhs α)) (map redex_patterns As) !i = (?p, redex_patterns (As!i))" 
    using nth_zip by auto
  then have "?xs!i = map (λ(α, p). (α, ?p@p)) (redex_patterns (As!i))" using nth_map i by auto
  with assms have "(β, ?p@p) ∈ set (?xs!i)" by fastforce 
  moreover from i have "i < length ?xs" by simp
  ultimately have *:"(β, ?p@p) ∈ set (concat ?xs)" 
    unfolding set_concat by (meson UN_iff nth_mem) 
  then show ?thesis by simp
qed

lemma redex_patterns_elem_subst: 
  assumes "(α, p) ∈ set (redex_patterns ((to_pterm t) ⋅ σ))" 
  shows "∃p1 p2 x. p = p1@p2 ∧ (α, p2) ∈ set (redex_patterns (σ x)) ∧ p1 ∈ var_poss t ∧ t|_p1 = Var x" 
  using assms proof(induct t arbitrary: p)
  case (Var x)
  then show ?case unfolding to_pterm.simps eval_term.simps by force
next
  case (Fun f ts)
  from Fun(2) obtain j where j:"j < length (redex_patterns (to_pterm (Fun f ts) ⋅ σ))" "(redex_patterns (to_pterm (Fun f ts) ⋅ σ))!j = (α, p)" 
    by (metis in_set_idx) 
  from j obtain i k where i:"i < length ts" 
    and k:"k < length (map (λ(α, p). (α, i # p)) (redex_patterns (to_pterm (ts!i) ⋅ σ)))"
    and rdp:"(map (λ(α, p). (α, i # p)) (redex_patterns (to_pterm (ts!i) ⋅ σ)))!k = (α, p)"
    using nth_concat_split unfolding length_map to_pterm.simps eval_term.simps redex_patterns.simps by force 
  from rdp k obtain p' where p:"p = i#p'" 
    by (smt (verit, del_insts) case_prod_conv list.sel(3) map_eq_imp_length_eq map_ident nth_map prod.inject surj_pair) 
  from k rdp have "(α, p') ∈ set (redex_patterns (to_pterm (ts!i) ⋅ σ))" 
    unfolding p by (smt (verit, del_insts) case_prod_conv list.sel(3) map_eq_imp_length_eq map_ident nth_map nth_mem prod.inject surj_pair) 
  with Fun(1) i obtain p1 p2 x where p':"p' = p1@p2" and rdp2:"(α, p2) ∈ set (redex_patterns (σ x))" and "p1 ∈ var_poss (ts!i)" and "(ts!i)|_p1 = Var x"
    by (meson nth_mem) 
  with i have "i#p1 ∈ var_poss (Fun f ts)" "Fun f ts |_ (i#p1) = Var x" 
    by auto 
  with p' rdp2 show ?case 
    unfolding p by (meson Cons_eq_appendI)
qed

context left_lin_no_var_lhs
begin

lemma redex_patterns_rule'':
  assumes rdp:"(β, p @ q) ∈ set (redex_patterns (Prule α As))" 
    and wf:"Prule α As ∈ wf_pterm R" 
    and p:"p = var_poss_list (lhs α)!i" 
    and i:"i < length As" 
  shows "(β, q) ∈ set (redex_patterns (As!i))" 
proof-
  from wf obtain f ts where lhs:"lhs α = Fun f ts"
    by (metis Inl_inject case_prodD is_FunE is_Prule.simps(1) is_Prule.simps(3) no_var_lhs term.distinct(1) term.inject(2) wf_pterm.simps) 
  from wf i have l:"length As = length (var_poss_list (lhs α))"
    by (metis Inl_inject is_Prule.simps(1) is_Prule.simps(3) length_var_poss_list length_var_rule term.distinct(1) term.inject(2) wf_pterm.simps) 
  with i p have "p ∈ var_poss (Fun f ts)"
    by (metis lhs nth_mem var_poss_list_sound) 
  then have "p ≠ []" by force
  then obtain j p' where j:"j < length As" and p':"p@q = var_poss_list (lhs α) ! j @ p'" "(β, p') ∈ set (redex_patterns (As!j))" 
    using redex_patterns_elem_rule[OF rdp] by blast  
  {assume "j ≠ i" 
    then have "p ⊥ var_poss_list (lhs α) ! j" 
      unfolding p using i j by (metis distinct_var_poss_list l nth_eq_iff_index_eq nth_mem var_poss_list_sound var_poss_parallel) 
    with p'(1) have False
      by (metis less_eq_pos_simps(1) pos_less_eq_append_not_parallel) 
  }
  with p'(1) p have "j = i" and "p' = q" by fastforce+
  with p'(2) show ?thesis by simp
qed

lemma redex_patterns_elem_subst': 
  assumes "(α, p2) ∈ set (redex_patterns (σ x))" and p1:"p1 ∈ poss t" "t|_p1 = Var x"
  shows "(α, p1@p2) ∈ set (redex_patterns ((to_pterm t) ⋅ σ))" 
using assms proof(induct t arbitrary: p1)
  case (Var x)
  then show ?case unfolding to_pterm.simps eval_term.simps by force
next
  case (Fun f ts)
  from Fun(3,4) obtain i p1' where i:"i < length ts" and p1:"p1 = i#p1'" and p1':"p1' ∈ poss (ts!i)" "(ts!i)|_p1' = Var x"
    by auto 
  with Fun(1,2) have "(α, p1' @ p2) ∈ set (redex_patterns (to_pterm (ts!i) ⋅ σ))"
    using nth_mem by blast
  then obtain j where j:"j < length (redex_patterns (to_pterm (ts!i) ⋅ σ))" "redex_patterns (to_pterm (ts!i) ⋅ σ)!j = (α, p1' @ p2)"
    by (metis in_set_idx) 
  let ?xs="map2 (λi. map (λ(α, p). (α, i # p))) [0..<length (map (λs. s ⋅ σ) (map to_pterm ts))] (map redex_patterns (map (λs. s ⋅ σ) (map to_pterm ts)))"
  from i j have rdp:"?xs!i!j = (α, p1@p2)"
    unfolding p1 by auto
  let ?i="sum_list (map length (take i ?xs)) + j"
  from rdp i j(1) have "(redex_patterns ((to_pterm (Fun f ts)) ⋅ σ)) ! ?i = (α, p1@p2)" 
    using concat_nth[of i ?xs j] unfolding length_map by force
  moreover from i j(1) have "?i < length (redex_patterns (to_pterm (Fun f ts) ⋅ σ))" 
    using concat_nth_length[of i ?xs j] unfolding length_map by force
  ultimately show ?case
    using nth_mem by fastforce 
qed
 
lemma redex_patterns_join: 
  assumes "A ∈ wf_pterm R" "B ∈ wf_pterm R" "A ⊔ B = Some C"
  shows "set (redex_patterns C) = set (redex_patterns A) ∪ set (redex_patterns B)"  
  using assms proof(induct A arbitrary: B C rule:subterm_induct)
  case (subterm A)
  from subterm(2) show ?case proof(cases A)
    case (1 x)
    from subterm(2,3,4) var_join show ?thesis 
      unfolding 1 by auto
  next
    case (2 As f)
    with subterm(4) consider (Pfun) "∃g Bs. B = Pfun g Bs" | (Prule) "∃α Bs. B = Prule α Bs" by (meson fun_join) 
    then show ?thesis proof(cases)
      case Pfun
      then obtain g Bs where B:"B = Pfun g Bs" by blast
      from subterm(4) join_fun_fun obtain Cs where fg:"f = g" and l_As_Bs:"length As = length Bs" and  
        C:"C = Pfun f Cs" and l_Cs_As:"length Cs = length As" and Cs:"(∀i<length As. As ! i ⊔ Bs ! i = Some (Cs ! i))"
        unfolding 2 B by force 
      {fix i assume i:"i < length As" 
        with subterm(3) have "Bs!i ∈ wf_pterm R"
          using B l_As_Bs by auto 
        with subterm(1) i 2 Cs have "set (redex_patterns (Cs!i)) = set (redex_patterns (As!i)) ∪ set (redex_patterns (Bs!i))"
          by (meson nth_mem supt.arg)
      }note IH=this
      {fix α p assume "(α, p) ∈ set (redex_patterns C)" 
        then obtain i p' where i:"i < length Cs" and p:"p = i#p'" and "(α, p') ∈ set (redex_patterns (Cs!i))" 
          unfolding C by (meson redex_patterns_elem_fun)
        with IH consider "(α, p') ∈ set (redex_patterns (As!i))" | "(α, p') ∈ set (redex_patterns (Bs!i))"
          using l_Cs_As by fastforce
        then have "(α, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)" proof(cases)
          case 1
          with i have "(α, p) ∈ set (redex_patterns A)" 
            unfolding 2 p l_Cs_As by (meson redex_patterns_elem_fun')
          then show ?thesis by simp
        next
          case 2
          with i have "(α, p) ∈ set (redex_patterns B)" 
            unfolding B l_Cs_As l_As_Bs p by (meson redex_patterns_elem_fun')
          then show ?thesis by simp
        qed
      }
      moreover 
      {fix α p assume "(α, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)"
        then consider "(α, p) ∈ set (redex_patterns A)" | "(α, p) ∈ set (redex_patterns B)" by force
        then have "(α, p) ∈ set (redex_patterns C)" proof(cases)
          case 1
          then obtain i p' where i:"i < length As" and p:"p = i#p'" and "(α, p') ∈ set (redex_patterns (As!i))" 
            unfolding 2 by (meson redex_patterns_elem_fun)
          with IH have "(α, p') ∈ set (redex_patterns (Cs!i))" by blast 
          with i l_Cs_As show ?thesis unfolding C p
            by (metis redex_patterns_elem_fun')
        next
          case 2
          then obtain i p' where i:"i < length Bs" and p:"p = i#p'" and "(α, p') ∈ set (redex_patterns (Bs!i))" 
            unfolding B by (meson redex_patterns_elem_fun)
          with IH l_As_Bs have "(α, p') ∈ set (redex_patterns (Cs!i))" by simp 
          with i l_Cs_As l_As_Bs show ?thesis unfolding C p
            by (metis redex_patterns_elem_fun')
        qed
      }
      ultimately show ?thesis by auto
    next
      case Prule
      then obtain α Bs where B:"B = Prule α Bs" by blast
      from B subterm(3) have alpha:"to_rule α ∈ R"
        using wf_pterm.simps by fastforce 
      then obtain f' ts where lhs:"lhs α = Fun f' ts" 
        using no_var_lhs by fastforce 
      from alpha have lin:"linear_term (lhs α)"
        using left_lin left_linear_trs_def by fastforce 
      from B subterm(3,4) obtain σ Cs where sigma:"match A (to_pterm (lhs α)) = Some σ"
        and C:"C = Prule α Cs" and l_Cs_Bs:"length Cs = length Bs" and Cs:"(∀i<length Bs. σ (var_rule α ! i) ⊔ (Bs ! i) = Some (Cs ! i))"
        unfolding 2 using join_rule_fun join_sym by (smt (verit, best)) 
      from B subterm(3) have l_Bs:"length Bs = length (var_rule α)"
        using wf_pterm.simps by fastforce 
      from sigma have A:"A = (to_pterm (lhs α) ⋅ σ)"
        by (simp add: match_matches)
      {fix i assume i:"i < length Bs" 
        with sigma lhs l_Bs have "σ (var_rule α ! i) ⊲ A"
          by (smt (verit, best) comp_def match_lhs_subst nth_mem set_remdups set_rev set_vars_term_list subst_image_subterm to_pterm.simps(2) vars_to_pterm) 
        moreover have "σ (var_rule α ! i) ∈ wf_pterm R" 
          using subterm(2) by (metis i l_Bs match_well_def sigma vars_to_pterm) 
        moreover from i subterm(3) have "Bs!i ∈ wf_pterm R"
          using B nth_mem by blast 
        ultimately have "set (redex_patterns (Cs!i)) = set (redex_patterns (σ (var_rule α ! i))) ∪ set (redex_patterns (Bs!i))"
          using subterm(1) Cs l_Cs_Bs i by presburger
      }note IH=this
      {fix β p assume rdp:"(β, p) ∈ set (redex_patterns C)" 
        then have "(β, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)" proof(cases "p=[]")
          case True
          with rdp have "α = β"  
            unfolding C using lhs by (metis (no_types, lifting) C join_wf_pterm list.set_intros(1) option.sel 
                prod.inject redex_patterns.simps(3) redex_patterns_label subterm.prems(1) subterm.prems(2) subterm.prems(3)) 
          then show ?thesis unfolding B redex_patterns.simps True by simp
        next
          case False
          with rdp obtain i p' where i:"i < length Cs" "i < length (var_poss_list (lhs α))" 
            and p:"p = (var_poss_list (lhs α) ! i)@p'" and *:"(β, p') ∈ set (redex_patterns (Cs!i))" 
            unfolding C by (meson redex_patterns_elem_rule)
          let ?p="var_poss_list (lhs α) ! i"
          from * i IH consider "(β, p') ∈ set (redex_patterns (σ (var_rule α ! i)))" | "(β, p') ∈ set (redex_patterns (Bs!i))"
            using l_Cs_Bs by fastforce
          then show ?thesis proof(cases)
            case 1
            let ?x="var_rule α ! i"
            from i(2) have p_pos:"?p ∈ poss (lhs α)"
              by (metis nth_mem var_poss_iff var_poss_list_sound) 
            from i(2) have p_x:"(lhs α)|_?p = Var ?x"
              by (metis ‹to_rule α ∈ R› case_prodD left_lin left_linear_trs_def length_var_poss_list linear_term_var_vars_term_list vars_term_list_var_poss_list) 
            from i(2) have "(β, p) ∈ set (redex_patterns A)" 
              unfolding p A using redex_patterns_elem_subst'[of β p' σ ?x, OF 1 p_pos p_x] by simp
            then show ?thesis by simp
          next
            case 2
            from i have "(β, p) ∈ set (redex_patterns B)" 
              unfolding B p l_Cs_Bs using redex_patterns_elem_rule'[OF 2] by presburger
            then show ?thesis by simp
        qed
        qed
      }
      moreover 
      {fix β p assume "(β, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)"
        then consider "(β, p) ∈ set (redex_patterns A)" | "(β, p) ∈ set (redex_patterns B)" by force
        then have "(β, p) ∈ set (redex_patterns C)" proof(cases)
          case 1
          then obtain p1 p2 x where p:"p = p1@p2" and rdp2:"(β, p2) ∈ set (redex_patterns (σ x))" 
            and p1:"p1 ∈ var_poss (lhs α)" "lhs α|_p1 = Var x" 
            unfolding A using redex_patterns_elem_subst by metis 
          then obtain i where i:"i < length (var_rule α)" "(var_rule α)!i = x" 
            using lin by (metis in_set_conv_nth length_var_poss_list linear_term_var_vars_term_list term.inject(1) var_poss_list_sound vars_term_list_var_poss_list) 
          with p1 lin have p1:"p1 = var_poss_list (lhs α) ! i"
            by (metis length_var_poss_list linear_term_unique_vars linear_term_var_vars_term_list nth_mem var_poss_imp_poss var_poss_list_sound vars_term_list_var_poss_list) 
          from i IH rdp2 have "(β, p2) ∈ set (redex_patterns (Cs!i))"
            by (simp add: l_Bs) 
          with i(1) show ?thesis unfolding C p
            using redex_patterns_elem_rule' p1 by (metis alpha l_Bs l_Cs_Bs length_var_poss_list length_var_rule) 
        next
          case 2 
          show ?thesis proof(cases "p=[]")
            case True
            from 2 have "α = β"  
            unfolding B True using lhs by (metis (no_types, lifting) B list.set_intros(1) option.sel 
                prod.inject redex_patterns.simps(3) redex_patterns_label subterm.prems(2)) 
            then show ?thesis unfolding C redex_patterns.simps True by simp
          next
            case False
            with 2 obtain i p' where i:"i < length Bs" "i < length (var_poss_list (lhs α))" 
              and p:"p = (var_poss_list (lhs α) ! i)@p'" and *:"(β, p') ∈ set (redex_patterns (Bs!i))" 
              unfolding B by (meson redex_patterns_elem_rule)
            with IH l_Cs_Bs have "(β, p') ∈ set (redex_patterns (Cs!i))" by simp 
            with i l_Cs_Bs show ?thesis unfolding C p
              by (metis redex_patterns_elem_rule')
          qed
        qed
      }
      ultimately show ?thesis by auto
    qed
  next
    case (3 α As)
    from 3(2) obtain f' ts where lhs:"lhs α = Fun f' ts" 
      using no_var_lhs by fastforce 
    from 3(2) have lin:"linear_term (lhs α)"
      using left_lin left_linear_trs_def by fastforce 
    from 3 subterm(2,4) consider (Pfun) "∃g Bs. B = Pfun g Bs" | (Prule) "∃β Bs. B = Prule β Bs" by (meson rule_join) 
    then show ?thesis proof(cases)
      case Pfun
      then obtain f Bs where B:"B = Pfun f Bs" by blast
      from subterm(2,4) obtain σ Cs where sigma:"match B (to_pterm (lhs α)) = Some σ"
        and C:"C = Prule α Cs" and l_Cs_As:"length Cs = length As" and As:"(∀i<length As. (As ! i) ⊔ σ (var_rule α ! i) = Some (Cs ! i))"
        unfolding 3 B using 3(3) join_rule_fun by metis
      {fix i assume i:"i < length As" 
        have "σ (var_rule α ! i) ∈ wf_pterm R" 
          using subterm(3) by (metis "3"(3) i match_well_def sigma vars_to_pterm)
        then have "set (redex_patterns (Cs!i)) = set (redex_patterns (As!i)) ∪ set (redex_patterns (σ (var_rule α ! i)))"
          using subterm(1) 3 by (meson As i nth_mem supt.arg) 
      }note IH=this
      {fix β p assume rdp:"(β, p) ∈ set (redex_patterns C)" 
        then have "(β, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)" proof(cases "p=[]")
          case True
          with rdp have "α = β"  
            unfolding C using lhs by (metis (no_types, lifting) C join_wf_pterm list.set_intros(1) option.sel 
                prod.inject redex_patterns.simps(3) redex_patterns_label subterm.prems(1) subterm.prems(2) subterm.prems(3)) 
          then show ?thesis unfolding 3 redex_patterns.simps True by simp
        next
          case False
          with rdp obtain i p' where i:"i < length Cs" "i < length (var_poss_list (lhs α))" 
            and p:"p = (var_poss_list (lhs α) ! i)@p'" and *:"(β, p') ∈ set (redex_patterns (Cs!i))" 
            unfolding C by (meson redex_patterns_elem_rule)
          let ?p="var_poss_list (lhs α) ! i"
          from * i IH consider "(β, p') ∈ set (redex_patterns (σ (var_rule α ! i)))" | "(β, p') ∈ set (redex_patterns (As!i))"
            using l_Cs_As by auto
          then show ?thesis proof(cases)
            case 1
            let ?x="var_rule α ! i"
            from i(2) have p_pos:"?p ∈ poss (lhs α)"
              by (metis nth_mem var_poss_iff var_poss_list_sound) 
            from i(2) have p_x:"(lhs α)|_?p = Var ?x"
              by (metis 3(2) case_prodD left_lin left_linear_trs_def length_var_poss_list linear_term_var_vars_term_list vars_term_list_var_poss_list) 
            from sigma have "(β, p) ∈ set (redex_patterns B)" 
              unfolding p using redex_patterns_elem_subst'[of β p' σ ?x, OF 1 p_pos p_x] by (simp add: match_matches)
            then show ?thesis by simp
          next
            case 2
            from i have "(β, p) ∈ set (redex_patterns A)" 
              unfolding 3(1) p l_Cs_As using redex_patterns_elem_rule'[OF 2] by presburger
            then show ?thesis by simp
          qed
        qed
      }
      moreover 
      {fix β p assume "(β, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)"
        then consider "(β, p) ∈ set (redex_patterns B)" | "(β, p) ∈ set (redex_patterns A)"  by force
        then have "(β, p) ∈ set (redex_patterns C)" proof(cases)
          case 1
          then obtain p1 p2 x where p:"p = p1@p2" and rdp2:"(β, p2) ∈ set (redex_patterns (σ x))" 
            and p1:"p1 ∈ var_poss (lhs α)" "lhs α|_p1 = Var x" 
            using sigma redex_patterns_elem_subst using match_matches by blast
          then obtain i where i:"i < length (var_rule α)" "(var_rule α)!i = x" 
            using lin by (metis in_set_conv_nth length_var_poss_list linear_term_var_vars_term_list term.inject(1) var_poss_list_sound vars_term_list_var_poss_list) 
          with p1 lin have p1:"p1 = var_poss_list (lhs α) ! i"
            by (metis length_var_poss_list linear_term_unique_vars linear_term_var_vars_term_list nth_mem var_poss_imp_poss var_poss_list_sound vars_term_list_var_poss_list) 
          from i IH rdp2 have "(β, p2) ∈ set (redex_patterns (Cs!i))"
            by (simp add: "3"(3))
          with i(1) show ?thesis unfolding C p
            using redex_patterns_elem_rule' p1 by (metis "3"(2) "3"(3) l_Cs_As length_var_poss_list length_var_rule)
        next
          case 2 
          show ?thesis proof(cases "p=[]")
            case True
            from 2 have "α = β"  
              unfolding True using lhs by (metis "3"(1) list.set_intros(1) option.sel prod.sel(1) redex_patterns.simps(3) redex_patterns_label subterm.prems(1))
            then show ?thesis unfolding C redex_patterns.simps True by simp
          next
            case False
            with 2 obtain i p' where i:"i < length As" "i < length (var_poss_list (lhs α))" 
              and p:"p = (var_poss_list (lhs α) ! i)@p'" and *:"(β, p') ∈ set (redex_patterns (As!i))"
              using "3"(1) redex_patterns_elem_rule by blast 
            with IH l_Cs_As have "(β, p') ∈ set (redex_patterns (Cs!i))" by simp 
            with i l_Cs_As show ?thesis unfolding C p
              by (metis redex_patterns_elem_rule')
          qed
        qed
      }
      ultimately show ?thesis by auto
    next
      case Prule
      then obtain β Bs where B:"B = Prule β Bs" by blast
      obtain Cs where alpha_beta:"α = β" and l_As_Bs:"length As = length Bs" 
        and C:"C = Prule α Cs" and l_Cs_As:"length Cs = length As" and args:"∀i < length As. As ! i ⊔ Bs ! i = Some (Cs ! i)" 
        using join_rule_rule[OF subterm(4,2,3)[unfolded B 3]] using "3"(3) by fastforce 
      {fix i assume "i < length As" 
        from subterm(1) have "set (redex_patterns (Cs!i)) = set (redex_patterns (As!i)) ∪ set (redex_patterns (Bs!i))"
          by (metis "3"(1) "3"(4) B ‹i < length As› fun_well_arg l_As_Bs local.args nth_mem subterm.prems(2) supt.arg)
      }note IH=this
      {fix γ p assume rdp:"(γ, p) ∈ set (redex_patterns C)" 
        have "(γ, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)" proof(cases "p = []")
          case True
          from rdp have "α = γ" unfolding C True using lhs
            by (metis (no_types, lifting) C join_wf_pterm list.set_intros(1) option.sel prod.inject redex_patterns.simps(3) redex_patterns_label subterm(2,3,4)) 
          then show ?thesis unfolding 3 True by simp
        next
          case False
          then obtain p2 i where i:"i < length Cs" "i < length (var_poss_list (lhs α))" 
            and p:"p = var_poss_list (lhs α) ! i @p2" and "(γ, p2) ∈ set (redex_patterns (Cs!i))" 
            using C rdp redex_patterns_elem_rule by blast
          with IH consider "(γ, p2) ∈ set (redex_patterns (As!i))" | "(γ, p2) ∈ set (redex_patterns (Bs!i))"
            using l_Cs_As by fastforce
          then show ?thesis proof(cases)
            case 1
            with i have "(γ, p) ∈ set (redex_patterns A)" 
              unfolding 3 p l_Cs_As by (metis "3"(3) redex_patterns_elem_rule')
            then show ?thesis by simp
          next
            case 2
            with i have "(γ, p) ∈ set (redex_patterns B)" 
              unfolding B l_Cs_As l_As_Bs p alpha_beta using redex_patterns_elem_rule' by blast
            then show ?thesis by simp
          qed
        qed
      }
      moreover 
      {fix γ p assume rdp:"(γ, p) ∈ set (redex_patterns A) ∪ set (redex_patterns B)"
        have "(γ, p) ∈ set (redex_patterns C)" proof(cases "p = []")
          case True
          from rdp lhs have "γ = α" 
            unfolding 3 B alpha_beta True
            by (metis "3"(1) B Un_iff alpha_beta list.set_intros(1) option.inject prod.inject redex_patterns.simps(3) redex_patterns_label subterm.prems(1) subterm.prems(2)) 
          then show ?thesis unfolding C True by simp 
        next
          case False
          from rdp consider "(γ, p) ∈ set (redex_patterns A)" | "(γ, p) ∈ set (redex_patterns B)" by force
          then show ?thesis proof(cases) 
            case 1
            then obtain p2 i where i:"i < length As" "i < length (var_poss_list (lhs α))" 
              and p:"p = var_poss_list (lhs α) ! i @p2" and "(γ, p2) ∈ set (redex_patterns (As!i))" 
              using 3 redex_patterns_elem_rule False by blast
            with IH have "(γ, p2) ∈ set (redex_patterns (Cs!i))" by blast 
            with i l_Cs_As show ?thesis unfolding C p
              by (metis redex_patterns_elem_rule')
          next
            case 2
            then obtain p2 i where i:"i < length Bs" "i < length (var_poss_list (lhs α))" 
              and p:"p = var_poss_list (lhs α) ! i @p2" and "(γ, p2) ∈ set (redex_patterns (Bs!i))" 
              using B alpha_beta redex_patterns_elem_rule False by blast
            with IH have "(γ, p2) ∈ set (redex_patterns (Cs!i))" using l_As_Bs by simp 
            with i l_Cs_As l_As_Bs show ?thesis unfolding C p
              by (metis redex_patterns_elem_rule')
          qed
        qed 
      }
      ultimately show ?thesis by auto
    qed
  qed
qed

lemma redex_patterns_join_list: 
  assumes "join_list As = Some A" and "∀a ∈ set As. a ∈ wf_pterm R"
  shows "set (redex_patterns A) = ⋃ (set (map (set ∘ redex_patterns) As))"  
  using assms proof(induct As arbitrary:A)
  case (Cons a As)
  show ?case proof(cases "As = []")
    case True
    from Cons(2,3) have "a = A" 
      unfolding True join_list.simps by (simp add: join_with_source) 
    then show ?thesis unfolding True by simp
  next
    case False
    then have *:"join_list (a#As) = join_opt a (join_list As)"
      using join_list.elims by blast 
    with Cons(2) obtain A' where A':"join_list As = Some A'" by fastforce
    with Cons(1,3) have "set (redex_patterns A') = ⋃ (set (map (set ∘ redex_patterns) As))"  
      by simp
    then show ?thesis using redex_patterns_join * Cons(2,3) unfolding A' join_opt.simps
      by (metis (no_types, opaque_lifting) A' Sup_insert insert_iff join_list_wf_pterm list.set(2) list.simps(9) o_apply) 
  qed
qed simp

lemma redex_patterns_context:
  assumes "p ∈ poss s"
  shows "redex_patterns ((ctxt_of_pos_term p (to_pterm s)) ⟨A⟩) = map (λ(α, q). (α,p@q)) (redex_patterns A)" 
  using assms proof(induct p arbitrary:s)
  case (Cons i p')
  from Cons(2) obtain f ss where s:"s = Fun f ss"
    by (meson args_poss)
  from Cons(2) have i:"i < length ss" and p':"p' ∈ poss (ss!i)" 
    unfolding s by auto
  with Cons(1) have IH:"redex_patterns (ctxt_of_pos_term p' (to_pterm (ss!i)))⟨A⟩ =
    map (λ(α, q). (α,p'@q)) (redex_patterns A)" by simp
  from i have l:"length (take i (map to_pterm ss) @ (ctxt_of_pos_term p' (map to_pterm ss ! i))⟨A⟩ # drop (Suc i) (map to_pterm ss)) = length ss" 
    by simp
  let ?take_i="take i (map to_pterm ss)"
  let ?ith="(ctxt_of_pos_term p' (map to_pterm ss ! i))⟨A⟩"
  let ?drop_i="drop (Suc i) (map to_pterm ss)"
  let ?xs="take i (map to_pterm ss) @ (ctxt_of_pos_term p' (map to_pterm ss ! i))⟨A⟩ # drop (Suc i) (map to_pterm ss)"
  let ?zip="zip [0..<length ss] (map redex_patterns ?xs)" 
  from i have l_zip:"length ?zip = length ss" by auto
  let ?zip1="zip [0..<i] (map redex_patterns ?take_i)" 
  let ?zip2="zip [Suc i..<length ss] (map redex_patterns ?drop_i)"
  have zip:"?zip = ?zip1 @ ((i, redex_patterns ?ith) # ?zip2)"
    unfolding map_append zip_append2 using i by (simp add: upt_conv_Cons)  
  {fix j assume j:"j < length (map (λ(x, y). map (λ(α, p). (α, x # p)) y) ?zip1)" 
    with i have "(map redex_patterns ?take_i)!j = []"
      by (simp add: redex_patterns_to_pterm) 
    with j have "?zip1 ! j = (j, [])" 
      by simp
    with j have "map (λ(x, y). map (λ(α, p). (α, x # p)) y) ?zip1 ! j = []" 
      by simp 
  }
  then have 1:"concat (map (λ(x, y). map (λ(α, p). (α, x # p)) y) ?zip1) = []"
    by (metis length_0_conv length_greater_0_conv less_nat_zero_code nth_concat_split) 
  {fix j assume j:"j < length (map (λ(x, y). map (λ(α, p). (α, x # p)) y) ?zip2)" 
    with i have "(map redex_patterns ?drop_i)!j = []"
      by (simp add: redex_patterns_to_pterm) 
    with j have "?zip2 ! j = (j+Suc i, [])" 
      by simp
    with j have "map (λ(x, y). map (λ(α, p). (α, x # p)) y) ?zip2 ! j = []" 
      by simp 
  }
  then have 2:"concat (map (λ(x, y). map (λ(α, p). (α, x # p)) y) ?zip2) = []"
    by (metis length_0_conv length_greater_0_conv less_nat_zero_code nth_concat_split) 
  show ?case unfolding s to_pterm.simps ctxt_of_pos_term.simps intp_actxt.simps redex_patterns.simps l zip 
    unfolding map_append concat_append 1 list.map(2) concat.simps 2 using IH i by simp
qed simp

lemma redex_patterns_prule:
  assumes l:"length ts = length (var_poss_list (lhs α))" 
  shows "redex_patterns (Prule α (map to_pterm ts)) = [(α, [])]"
proof-
  {fix x assume x:"x ∈ set (map2 (λx. map (λ(α, p2). (α, x @ p2))) (var_poss_list (lhs α)) (map redex_patterns (map to_pterm ts)))"
    from l have "length (map2 (λx. map (λ(α, p2). (α, x @ p2))) (var_poss_list (lhs α)) (map redex_patterns (map to_pterm ts))) = length (var_poss_list (lhs α))" 
      by simp
    with x obtain i where i:"i < length (var_poss_list (lhs α))" "x = (map2 (λx. map (λ(α, p2). (α, x @ p2))) (var_poss_list (lhs α)) (map redex_patterns (map to_pterm ts)))!i"
      by (metis in_set_idx) 
    from i l have "x = []" 
      using redex_patterns_to_pterm by simp
  }
  then show ?thesis
    unfolding redex_patterns.simps using concat_eq_Nil_conv by blast
qed

lemma redex_patterns_single:
  assumes "p ∈ poss s" and "to_rule α ∈ R"
  shows "redex_patterns (ll_single_redex s p α) = [(α, p)]"
proof-
  let ?As="map (to_pterm ∘ (λpi. s |_ (p @ pi))) (var_poss_list (lhs α))"
  let ?A="Prule α ?As" 
  have "redex_patterns ?A = [(α, [])]" 
    using redex_patterns_prule using length_map by fastforce 
  moreover have "set (redex_patterns (ll_single_redex s p α)) = set (map (λ (α, q). (α,p@q)) (redex_patterns ?A))"
    using redex_patterns_context assms redex_patterns_to_pterm[of s] unfolding ll_single_redex_def using p_in_poss_to_pterm by fastforce
  ultimately have set:"set (redex_patterns (ll_single_redex s p α)) = {(α, p)}" 
    by simp
  have wf:"ll_single_redex s p α ∈ wf_pterm R"
    using assms left_lin left_linear_trs_def single_redex_wf_pterm by fastforce 
  have sorted:"sorted_wrt (ord.lexordp (<)) (map snd [(α, p)])" by simp
  show ?thesis using redex_patterns_equal[OF wf sorted] set by simp
qed  

lemma get_label_imp_rdp:
  assumes "get_label (labeled_source A |_ p) = Some (α, 0)"
    and "A ∈ wf_pterm R"
    and "p ∈ poss (labeled_source A)"
  shows "(α, p) ∈ set (redex_patterns A)" 
  using assms proof(induct A arbitrary:p)
  case (Pfun f As)
  then show ?case proof(cases p)
    case (Cons i p')
    from Pfun(4) have i:"i < length As" 
      unfolding Cons by simp
    moreover from Pfun(2,4) have "get_label (labeled_source (As!i) |_ p') = Some (α, 0)" 
      unfolding Cons by simp
    moreover from Pfun(4) have "p' ∈ poss (labeled_source (As!i))" 
      unfolding Cons using i by simp
    ultimately have "(α, p') ∈ set (redex_patterns (As!i))"
      using Pfun(1,3) using nth_mem by blast 
    then show ?thesis 
      unfolding Cons redex_patterns.simps using i by (metis redex_patterns.simps(2) redex_patterns_elem_fun')
  qed simp
next
  case (Prule β As)
  from Prule(3) obtain f ts where lhs:"lhs β = Fun f ts"
    by (metis Inl_inject Term.term.simps(4) case_prodD is_Prule.simps(1) is_Prule.simps(3) no_var_lhs term.collapse(2) term.sel(2) wf_pterm.simps) 
  then show ?case proof(cases p)
    case Nil
    from Prule(2,3,4) show ?thesis 
      unfolding Nil labeled_source.simps lhs label_term.simps eval_term.simps subt_at.simps get_label.simps by simp
  next
    case (Cons i' p')
    from Prule(3) have l:"length As = length (var_poss_list (lhs β))"
      by (metis Inl_inject is_Prule.simps(1) is_Prule.simps(3) length_var_poss_list length_var_rule term.distinct(1) term.inject(2) wf_pterm.simps) 
    from Prule obtain i p2 where p:"p = var_poss_list (lhs β)!i @ p2" and i:"i < length As" and p2:"p2 ∈ poss (labeled_source (As!i))"
      by (smt (verit) labeled_source_to_term left_lin_no_var_lhs.get_label_Prule left_lin_no_var_lhs_axioms list.distinct(1) local.Cons poss_term_lab_to_term)
    let ?x="vars_term_list (lhs β) ! i" 
    let ?p1="var_poss_list (lhs β) ! i" 
    have p1:"?p1 ∈ poss (labeled_lhs β)"
      by (metis i l label_term_to_term nth_mem poss_term_lab_to_term var_poss_imp_poss var_poss_list_sound) 
    have "labeled_lhs β |_ ?p1 = Var ?x" 
      using i l by (metis length_var_poss_list var_poss_list_labeled_lhs vars_term_list_labeled_lhs vars_term_list_var_poss_list)
    then have "labeled_source (Prule β As) |_ ?p1 = labeled_source (As!i)" 
      unfolding labeled_source.simps subt_at_subst[OF p1]
      by (smt (verit) Inl_inject Prule.prems(2) apply_lhs_subst_var_rule comp_eq_dest_lhs eval_term.simps(1) i is_Prule.simps(1) is_Prule.simps(3) 
          l length_map length_remdups_eq length_rev length_var_poss_list map_nth_conv rev_rev_ident term.distinct(1) term.inject(2) wf_pterm.simps) 
    with Prule(2,4) have "get_label (labeled_source (As!i)|_p2) = Some (α, 0)" 
      unfolding p labeled_source.simps by auto
    then have "(α, p2) ∈ set (redex_patterns (As!i))"
      using Prule(1)[of "As!i" p2] p2 Prule(3) i by (meson fun_well_arg nth_mem)   
    then show ?thesis unfolding p redex_patterns.simps using i
      by (metis l redex_patterns.simps(3) redex_patterns_elem_rule')
  qed
qed simp

lemma redex_pattern_proof_term_equality:
  assumes "A ∈ wf_pterm R" "B ∈ wf_pterm R" 
    and "set (redex_patterns A) = set (redex_patterns B)" 
    and "source A = source B"
  shows "A = B" 
  using assms proof(induct A arbitrary:B)
  case (1 x)
  then show ?case
    using redex_poss_empty_imp_empty_step source_empty_step by force
next
  case (2 As f)
  then show ?case proof(cases B)
    case (Pfun g Bs)
    from 2(4) have f:"f = g" 
      unfolding Pfun by fastforce
    from 2(4) have len:"length As = length Bs"
      unfolding Pfun f by (metis length_map source.simps(2) term.inject(2))
    {fix i assume i:"i < length As" 
      have "set (redex_patterns (As!i)) = set (redex_patterns (Bs!i))" proof(rule ccontr)
        assume "set (redex_patterns (As!i)) ≠ set (redex_patterns (Bs!i))" 
        then consider "∃r. r ∈ set (redex_patterns (As!i)) ∧ r ∉ set (redex_patterns (Bs!i))" | 
                      "∃r. r ∈ set (redex_patterns (Bs!i)) ∧ r ∉ set (redex_patterns (As!i))"
          by blast
        then show False proof(cases)
          case 1
          then obtain p α where "(α, p) ∈ set (redex_patterns (As!i))" and B:"(α, p) ∉ set (redex_patterns (Bs!i))"
            by force
          then have "(α, i#p) ∈ set (redex_patterns (Pfun f As))"
            by (meson i redex_patterns_elem_fun') 
          moreover from B have "(α, i#p) ∉ set (redex_patterns (Pfun f Bs))"
            by (metis list.inject redex_patterns_elem_fun) 
          ultimately show ?thesis
            using "2.prems"(2) Pfun f by blast
        next
          case 2
           then obtain p α where "(α, p) ∈ set (redex_patterns (Bs!i))" and A:"(α, p) ∉ set (redex_patterns (As!i))"
            by force
          then have "(α, i#p) ∈ set (redex_patterns (Pfun f Bs))"
            by (metis i len redex_patterns_elem_fun')
          moreover from A have "(α, i#p) ∉ set (redex_patterns (Pfun f As))"
            by (metis list.inject redex_patterns_elem_fun) 
          ultimately show ?thesis
            using "2.prems"(2) Pfun f by blast
        qed
      qed
      moreover have "(Bs!i) ∈ wf_pterm R"
        using 2(2) Pfun i len by auto
      ultimately have "As!i = Bs!i" 
        using 2(1,4) by (metis Pfun i len nth_map nth_mem source.simps(2) term.inject(2)) 
    }
    then show ?thesis 
      unfolding Pfun f using len using nth_equalityI by blast
  next
    case (Prule α Bs)
    with 2(3) show ?thesis
      by (metis list.distinct(1) list.set_intros(1) redex_patterns.simps(3) redex_patterns_elem_fun) 
  qed simp
next
  case (3 α As)
  then show ?case proof(cases B)
    case (Pfun g Bs)
    with 3(5) show ?thesis
      by (metis list.distinct(1) list.set_intros(1) redex_patterns.simps(3) redex_patterns_elem_fun)
  next
    case (Prule β Bs)
    from 3(5) have α:"α = β" 
      unfolding Prule using distinct_snd_rdp
      by (metis "3.prems"(1) Pair_inject Prule left_lin_no_var_lhs.redex_patterns_label 
          left_lin_no_var_lhs_axioms list.set_intros(1) option.inject redex_patterns.simps(3))
    from 3 have len:"length As = length Bs"
      using Prule α by (metis length_args_well_Prule wf_pterm.intros(3)) 
    have len2:"length (var_poss_list (lhs β)) = length Bs"
      by (metis "3.hyps"(1) "3.hyps"(2) α len length_var_poss_list length_var_rule)
    {fix i assume i:"i < length As" 
      obtain pi where pi:"var_poss_list (lhs β) ! i = pi"
        by auto 
      have "set (redex_patterns (As!i)) = set (redex_patterns (Bs!i))" proof(rule ccontr)
        assume "set (redex_patterns (As!i)) ≠ set (redex_patterns (Bs!i))" 
        then consider "∃r. r ∈ set (redex_patterns (As!i)) ∧ r ∉ set (redex_patterns (Bs!i))" | 
                      "∃r. r ∈ set (redex_patterns (Bs!i)) ∧ r ∉ set (redex_patterns (As!i))"
          by blast
        then show False proof(cases)
          case 1
          then obtain p β where "(β, p) ∈ set (redex_patterns (As!i))" and B:"(β, p) ∉ set (redex_patterns (Bs!i))"
            by force
          then show False
            using 3(4,5) by (metis Prule α i len len2 redex_patterns_elem_rule' redex_patterns_rule'') 
        next
          case 2
           then obtain p β where "(β, p) ∈ set (redex_patterns (Bs!i))" and A:"(β, p) ∉ set (redex_patterns (As!i))"
            by force
          then show False
            using 3 by (metis Prule α i len len2 redex_patterns_elem_rule' redex_patterns_rule'' wf_pterm.intros(3)) 
        qed
      qed
      moreover have "(Bs!i) ∈ wf_pterm R"
        using "3.prems"(1) Prule i len by auto
      moreover have "co_initial (As!i) (Bs!i)"
        using 3 by (metis Prule α co_init_prule i wf_pterm.intros(3))
      ultimately have "As!i = Bs!i" 
        using 3(3) by (simp add: i)
    }
    then show ?thesis 
      unfolding Prule α using len using nth_equalityI by blast
  qed simp
qed


end

abbreviation single_steps :: "('f, 'v) pterm ⇒ ('f, 'v) pterm list" 
  where "single_steps A ≡ map (λ (α, p). ll_single_redex (source A) p α) (redex_patterns A)"

context left_lin_wf_trs
begin

lemma ll_no_var_lhs: "left_lin_no_var_lhs R"
  by (simp add: left_lin_axioms left_lin_no_var_lhs_def no_var_lhs_axioms)

lemma single_step_redex_patterns:
  assumes "A ∈ wf_pterm R" "Δ ∈ set (single_steps A)" 
  shows "∃p α. Δ = ll_single_redex (source A) p α ∧ (α, p) ∈ set (redex_patterns A) ∧ redex_patterns Δ = [(α, p)]"
proof-
  from assms obtain p α where Δ:"Δ = ll_single_redex (source A) p α" and rdp:"(α, p) ∈ set (redex_patterns A)"
    by auto
  moreover have "to_rule α ∈ R"
    using rdp assms(1) labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs by fastforce 
  moreover have "p ∈ poss (source A)"
    using assms rdp left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs by blast 
  ultimately show ?thesis 
    using Δ left_lin_no_var_lhs.redex_patterns_single[OF ll_no_var_lhs] by blast
qed

lemma single_step_wf:
  assumes "A ∈ wf_pterm R" and "Δ ∈ set (single_steps A)"
  shows "Δ ∈ wf_pterm R" 
proof-
  from assms obtain p α where p:"p ∈ poss (source A)" "Δ = ll_single_redex (source A) p α" and "get_label ((labeled_source A)|_p) = Some (α, 0)" 
    using left_lin_no_var_lhs.redex_patterns_label left_lin_no_var_lhs.redex_patterns_subset_possL possL_subset_poss_source ll_no_var_lhs by fastforce
  then have "to_rule α ∈ R"
    using assms(1) labeled_wf_pterm_rule_in_TRS by fastforce   
  with p show ?thesis using single_redex_wf_pterm
    using left_lin left_linear_trs_def by fastforce
qed

lemma source_single_step:
  assumes Δ:"Δ ∈ set (single_steps A)" and wf:"A ∈ wf_pterm R"
  shows "source Δ = source A" 
proof-
  let ?s="source A"
  from Δ obtain p α where pa:"Δ = ll_single_redex ?s p α" "(α, p) ∈ set (redex_patterns A)"
    by auto 
  from pa have lab_p:"get_label (labeled_source A |_p) = Some (α, 0)" and p:"p ∈ poss ?s" 
    using left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs wf by blast+
  from lab_p p obtain p' where p':"p'∈poss A" and ctxt:"ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p' A)" 
    and Ap':"A |_ p' = Prule α (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)])"
    using poss_labeled_source wf by force
  have l:"length (var_rule α) = length (var_poss_list (lhs α))"
    using wf by (metis Ap' Inl_inject Term.term.simps(4) is_Prule.simps(1) is_Prule.simps(3) length_var_poss_list length_var_rule p' subt_at_is_wf_pterm term.inject(2) wf_pterm.simps)
  {fix i assume i:"i < length (var_rule α)" 
    let ?pi="var_poss_list (lhs α)!i" 
    obtain x where x:"lhs α |_ ?pi = Var x" "var_rule α!i = x"
      by (metis comp_apply i l length_remdups_eq length_rev length_var_poss_list rev_rev_ident vars_term_list_var_poss_list) 
    have "?s|_p = lhs α ⋅ ⟨map source (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)])⟩⇩α" 
      using Ap' ctxt by (metis ctxt_of_pos_term_well ctxt_supt_id local.wf p p' replace_at_subt_at source.simps(3) source_ctxt_apply_term) 
    moreover have "lhs α ⋅ ⟨map source (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)])⟩⇩α |_ ?pi = map source (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)])!i" 
      using x by (smt (verit, ccfv_SIG) diff_zero eval_term.simps(1) i l length_upt lhs_subst_var_i map_eq_imp_length_eq map_nth nth_mem subt_at_subst var_poss_imp_poss var_poss_list_sound) 
    ultimately have "?s|_(p@?pi) = source (A |_ (p' @ [i]))" using i p by auto 
    then have "map source (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)]) !i = map (λpi. source A |_ (p @ pi)) (var_poss_list (lhs α)) ! i" 
      using l i by auto
  }
  with l have "map source (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)]) = map (λpi. source A |_ (p @ pi)) (var_poss_list (lhs α))"
    by (simp add: map_equality_iff) 
  then have "source (A|_p') = lhs α ⋅ ⟨map (λpi. ?s |_ (p @ pi)) (var_poss_list (lhs α))⟩⇩α" 
    unfolding Ap' source.simps by simp
  with ctxt show ?thesis unfolding pa(1) source_single_redex[OF p] using p'
    by (metis ctxt_of_pos_term_well ctxt_supt_id wf source_ctxt_apply_term) 
qed

lemma single_redex_single_step:
  assumes Δ:"Δ = ll_single_redex s p α" 
    and p:"p ∈ poss s" and α:"to_rule α ∈ R"
    and src:"source Δ = s"
  shows "single_steps Δ = [Δ]" 
  using src unfolding Δ left_lin_no_var_lhs.redex_patterns_single[OF ll_no_var_lhs p α] by simp 

lemma single_step_label_imp_label:
  assumes Δ:"Δ ∈ set (single_steps A)" and q:"q ∈ poss (labeled_source Δ)" and wf:"A ∈ wf_pterm R"
    and lab:"get_label (labeled_source Δ|_q) = Some l"
  shows "get_label (labeled_source A |_q) = Some l"
proof-
  let ?s="source A"
  from Δ obtain p α where pa:"Δ = ll_single_redex ?s p α" "(α, p) ∈ set (redex_patterns A)"
    by auto 
  from pa have lab_p:"get_label (labeled_source A |_p) = Some (α, 0)" and p:"p ∈ poss (source A)" 
    using left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs wf by blast+
  from pa lab obtain q' where l:"l = (α, size q')" and q':"q = p@q'" "q' ∈ fun_poss (lhs α)" 
    using single_redex_label[OF pa(1) p] q pa(2) wf
    by (metis labeled_source_to_term labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs poss_term_lab_to_term prod.collapse)   
  from lab_p p obtain p' where "p'∈poss A" and "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p' A)" and "A |_ p' = Prule α (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)])"
    using poss_labeled_source wf by force
  then have "labeled_source A = (ctxt_of_pos_term p (labeled_source A))⟨labeled_source (Prule α (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)]))⟩" 
    using label_source_ctxt p wf by (metis ctxt_supt_id) 
  then have "labeled_source A|_q = labeled_lhs α ⋅ ⟨map labeled_source (map (λi. A |_ (p' @ [i])) [0..<length (var_rule α)])⟩⇩α |_q'"
    unfolding q' labeled_source.simps by (metis labeled_source.simps(3) labeled_source_to_term p poss_term_lab_to_term subt_at_append subt_at_ctxt_of_pos_term) 
  then have "get_label (labeled_source A|_q) = Some (α, size q')" 
    using q'(2) by (simp add: label_term_increase) 
  with l show ?thesis by simp
qed

lemma single_steps_measure:
  assumes Δ1 :"Δ1 ∈ set (single_steps A)" and Δ2:"Δ2 ∈ set (single_steps A)" 
    and wf:"A ∈ wf_pterm R" and neq:"Δ1 ≠ Δ2" 
  shows "measure_ov Δ1 Δ2 = 0" 
proof-
  let ?s="source A"
  from Δ1 obtain p α where pa:"Δ1 = ll_single_redex ?s p α" "(α, p) ∈ set (redex_patterns A)"
    by auto 
  from Δ2 obtain q β where qb:"Δ2 = ll_single_redex ?s q β" "(β, q) ∈ set (redex_patterns A)"
    by auto  
  from neq have pq:"p ≠ q ∨ α ≠ β"
    using pa(1) qb(1) by force 
  {assume "measure_ov Δ1 Δ2 ≠ 0" 
    then obtain r where r1:"r ∈ possL Δ1" and r2:"r ∈ possL Δ2"
      by (metis card.empty disjoint_iff) 
    from r1 obtain p' where p':"r = p@p'" and l1:"get_label (labeled_source Δ1 |_r) = Some (α, size p')" 
      using single_redex_label[OF pa(1)] wf
      by (smt (verit, ccfv_SIG) labeled_source_to_term labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs pa(2) possL_obtain_label possL_subset_poss_source poss_term_lab_to_term subsetD)  
    from r2 obtain q' where q':"r = q@q'" and l2:"get_label (labeled_source Δ2 |_r) = Some (β, size q')" 
      using single_redex_label[OF qb(1)] wf
      by (smt (verit, ccfv_SIG) labeled_source_to_term labeled_wf_pterm_rule_in_TRS left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs qb(2) possL_obtain_label possL_subset_poss_source poss_term_lab_to_term subsetD)  
    from l1 have "get_label (labeled_source A |_r) = Some (α, size p')"
      using Δ1 labelposs_subs_poss wf r1 single_step_label_imp_label by blast
    moreover from l2 have "get_label (labeled_source A |_r) = Some (β, size q')"
      using Δ2 labelposs_subs_poss wf r2 single_step_label_imp_label by blast 
    moreover from pq have "p' ≠ q' ∨ α ≠ β" 
      using p' q' by blast
    ultimately have False using p' q' by auto
  }
  then show ?thesis by auto
qed

lemma single_steps_orth:
  assumes Δ1:"Δ1 ∈ set (single_steps A)" and Δ2:"Δ2 ∈ set (single_steps A)" and wf:"A ∈ wf_pterm R"
  shows "Δ1 ⊥⇩_p Δ2" 
  using single_steps_measure[OF Δ1 Δ2 wf] equal_imp_orthogonal
  by (metis Δ1 Δ2 ll_no_var_lhs local.wf measure_zero_imp_orthogonal single_step_wf source_single_step) 

lemma redex_patterns_below:
  assumes wf:"A ∈ wf_pterm R" 
  and "(α, p) ∈ set (redex_patterns A)" 
  and "(β, p@q) ∈ set (redex_patterns A)" and "q ≠ []"
shows "q ∉ fun_poss (lhs α)" 
proof-
  let ?Δ1="ll_single_redex (source A) p α" 
  let ?Δ2="ll_single_redex (source A) (p@q) β"
  from assms have Δ1:"?Δ1 ∈ set (single_steps A)"
    by force  
  from assms have Δ2:"?Δ2 ∈ set (single_steps A)"
    by force  
  from assms(1,2) have possL1:"possL ?Δ1 = {p@p' | p'. p' ∈ fun_poss (lhs α)}"
    by (metis (no_types, lifting) left_lin_no_var_lhs.redex_pattern_rule_symbol left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs single_redex_possL) 
  from assms(1,3) have possL2:"possL ?Δ2 = {(p@q)@p' | p'. p' ∈ fun_poss (lhs β)}"
    using left_lin.single_redex_possL left_lin_axioms left_lin_no_var_lhs.redex_pattern_rule_symbol left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs by blast 
  from assms have neq:"?Δ1 ≠ ?Δ2"
    by (metis Pair_inject left_lin_no_var_lhs.redex_patterns_label ll_no_var_lhs self_append_conv single_redex_neq) 
  from single_steps_measure[OF Δ1 Δ2 wf neq] have "possL ?Δ1 ∩ possL ?Δ2 = {}"
    by (simp add: finite_possL) 
  moreover have "[] ∈ fun_poss (lhs β)" proof-
    have "to_rule β ∈ R"
      using assms(1) assms(3) left_lin_no_var_lhs.redex_pattern_rule_symbol ll_no_var_lhs by blast
    then show ?thesis
      using wf_trs_alt wf_trs_imp_lhs_Fun by fastforce 
  qed
  ultimately show ?thesis 
    unfolding possL1 possL2 by auto
qed

lemma single_steps_singleton:
  assumes A_wf:"A ∈ wf_pterm R" and Δ:"single_steps A = [Δ]" 
  shows "A = Δ" 
proof-
  obtain p α where rdp_Δ:"Δ = ll_single_redex (source A) p α" "(α, p) ∈ set (redex_patterns A)" "redex_patterns Δ = [(α, p)]"
    using single_step_redex_patterns[OF A_wf] Δ by auto
  then have rdp_A:"redex_patterns A = [(α, p)]"
    by (smt (verit) Δ in_set_simps(2) list.map_disc_iff map_eq_Cons_D) 
  then show ?thesis 
    using left_lin_no_var_lhs.redex_pattern_proof_term_equality[OF ll_no_var_lhs A_wf]
    by (metis A_wf Δ list.set_intros(1) rdp_Δ(3) single_step_wf source_single_step) 
qed
end

context left_lin_no_var_lhs
begin
lemma measure_ov_imp_single_step_ov: 
  assumes "measure_ov A B ≠ 0" and wf:"A ∈ wf_pterm R"
  shows "∃Δ ∈ set (single_steps A). measure_ov Δ B ≠ 0" 
proof-
  from assms obtain r where r1:"r ∈ possL A" and r2:"r ∈ possL B"
    by (metis card.empty disjoint_iff) 
  then obtain α n where lab:"get_label (labeled_source A |_ r) = Some (α, n)"
    using possL_obtain_label by blast 
  with wf r1 obtain r1 r2 where r:"r = r1@r2" and lab_r1:"get_label (labeled_source A |_r1) = Some (α, 0)" and n:"length r2 = n"
    by (metis (no_types, lifting) append_take_drop_id diff_diff_cancel label_term_max_value labelposs_subs_poss length_drop obtain_label_root subsetD) 
  from r r1 have r1_pos:"r1 ∈ poss (labeled_source A)"
    using labelposs_subs_poss poss_append_poss by blast 
  then obtain q where q:"q∈poss A" and ctxt:"ctxt_of_pos_term r1 (source A) = source_ctxt (ctxt_of_pos_term q A)"  
    and Aq:"A |_ q = Prule α (map (λi. A |_ (q @ [i])) [0..<length (var_rule α)])" 
    using poss_labeled_source wf lab_r1 by blast
  with r r1 have r2_pos:"r2 ∈ poss (source (Prule α (map (λi. A |_ (q @ [i])) [0..<length (var_rule α)])))"
    by (metis (no_types, lifting) ctxt_supt_id fun_poss_imp_poss label_source_ctxt labeled_source_to_term labelposs_subs_fun_poss_source local.wf poss_term_lab_to_term r1_pos replace_at_subt_at subterm_poss_conv) 
  from Aq q wf have "Prule α (map (λi. A |_ (q @ [i])) [0..<length (var_rule α)]) ∈ wf_pterm R"
    using subt_at_is_wf_pterm by auto 
  moreover then have "is_Fun (lhs α)" using no_var_lhs
    using wf_pterm.cases by fastforce 
  moreover from lab ctxt have "get_label (labeled_source (Prule α (map (λi. A |_ (q @ [i])) [0..<length (var_rule α)])) |_r2) = Some (α, n)"
    by (metis (no_types, lifting) Aq ctxt_supt_id label_source_ctxt labeled_source_to_term local.wf poss_term_lab_to_term q r r1_pos replace_at_subt_at subt_at_append) 
  ultimately have r2_funposs:"r2 ∈ fun_poss (lhs α)"
    using labeled_poss_in_lhs[OF r2_pos] n by blast
  let ?Δ="ll_single_redex (source A) r1 α"
  from lab_r1 r1_pos have rdp:"(α, r1) ∈ set (redex_patterns A)" 
    using redex_patterns_label wf by auto
  then have Δ:"?Δ ∈ set (single_steps A)" by force 
  from r2 have "measure_ov ?Δ B ≠ 0"
    by (smt (verit, ccfv_threshold) rdp labeled_sources_imp_measure_not_zero labeled_wf_pterm_rule_in_TRS labelposs_subs_poss wf mem_Collect_eq option.simps(3) possL_obtain_label r r1_pos r2_funposs redex_patterns_label rel_simps(70) single_redex_possL subsetD) 
  with Δ show ?thesis by blast 
qed
end

context left_lin_no_var_lhs
begin
lemma label_single_step: 
  assumes "p ∈ poss (labeled_source A)" "A ∈ wf_pterm R" 
    and "get_label (labeled_source A |_ p) = Some (α, n)"
  shows "∃Ai. Ai ∈ set (single_steps A) ∧ get_label (labeled_source Ai |_ p) = Some (α, n)" 
proof- 
  let ?p1="take (length p - n) p"
  let ?p2="drop (length p - n) p"
  let ?xs="map (to_pterm ∘ (λpi. (source A)|_(p@pi))) (var_poss_list (lhs α))"
  from assms(1) have p1_pos:"?p1 ∈ poss (labeled_source A)"
    by (metis append_take_drop_id poss_append_poss) 
  have lab:"get_label (labeled_source A |_ ?p1) = Some (α, 0)"
    using obtain_label_root[OF assms(1) assms(3) assms(2)] by simp
  with assms have rdp:"(α, ?p1) ∈ set (redex_patterns A)"
    using redex_patterns_label[OF assms(2)] by (metis labeled_source_to_term obtain_label_root poss_term_lab_to_term) 
  then have "ll_single_redex (source A) ?p1 α ∈ set (single_steps A)" by force
  then obtain Ai where Ai:"Ai ∈ set (single_steps A)" "Ai = ll_single_redex (source A) ?p1 α" 
    by presburger
  from rdp obtain p' As where p':"A|_p' = Prule α As" "p' ∈ poss A" "ctxt_of_pos_term ?p1 (source A) = source_ctxt (ctxt_of_pos_term p' A)"
    using poss_labeled_source[OF p1_pos] lab assms(2) by blast
  from p' assms(2) have "A|_p' ∈ wf_pterm R"
    using subt_at_is_wf_pterm by blast 
  moreover from p' assms have "get_label (labeled_source (A|_p') |_ ?p2) = Some (α, n)"
    by (smt (verit, ccfv_SIG) append_take_drop_id ctxt_supt_id label_source_ctxt p1_pos rdp redex_patterns_label replace_at_subt_at subterm_poss_conv) 
  ultimately have p2_pos:"?p2 ∈ fun_poss (lhs α)"
    using labeled_poss_in_lhs no_var_lhs assms p'
    by (smt (verit, ccfv_threshold) append_take_drop_id case_prod_conv ctxt_of_pos_term_well ctxt_supt_id diff_diff_cancel label_term_max_value 
        labeled_source_to_term labeled_wf_pterm_rule_in_TRS length_drop  poss_append_poss poss_term_lab_to_term replace_at_subt_at source_ctxt_apply_term)
  then have l:"get_label (labeled_source (Prule α ?xs) |_ ?p2) = Some (α, n)"
    using label_term_increase assms by (metis (no_types, lifting) add_0  diff_diff_cancel label_term_max_value labeled_source.simps(3) length_drop)
  from p1_pos have "?p1 ∈ poss (source A)" by simp
  then have "get_label (labeled_source Ai |_ p) = Some (α, n)" 
    unfolding Ai(2) by (metis p2_pos append_take_drop_id l label_ctxt_apply_term label_term_increase labeled_source.simps(3) ll_single_redex_def)
  with Ai show ?thesis
    by blast 
qed

lemma proof_term_matches:
  assumes "A ∈ wf_pterm R" "B ∈ wf_pterm R" "linear_term A" 
    and "⋀α r. (α, r) ∈ set (redex_patterns A) = ((α, r) ∈ set (redex_patterns B) ∧ r ∈ fun_poss (source A))"  
    and "source A ⋅ σ = source B"
  shows "A ⋅ (mk_subst Var (match_substs A B)) = B" 
proof-
  {fix p g ts assume "p ∈ poss A" "A|_p = Fun g ts" 
    with assms have "∃ Bs. length ts = length Bs ∧ B|_p = Fun g Bs" 
      using assms proof(induct A arbitrary: B p rule:pterm_induct)
      case (Pfun f As)
      then have "⋀α. (α, []) ∉ set (redex_patterns (Pfun f As))"
        by (meson list.distinct(1) redex_patterns_elem_fun) 
      with Pfun(5) have "¬ (is_Prule B)"
        by (metis empty_pos_in_poss is_FunI is_Prule.elims(2) list.set_intros(1) poss_is_Fun_fun_poss redex_patterns.simps(3) source.simps(2) subt_at.simps(1)) 
      with Pfun(6) obtain Bs where B:"B = Pfun f Bs" and l:"length Bs = length As"
        by (smt (verit, del_insts) eval_term.simps(2) is_Prule.elims(3) length_map source.simps(1) source.simps(2) term.distinct(1) term.inject(2))
      then show ?case proof(cases p)
        case Nil
        from Pfun(8) show ?thesis unfolding Nil B using l by simp
      next
        case (Cons i p')
        from Pfun(7) have i:"i < length As" and p':"p' ∈ poss (As!i)" and a:"As!i ∈ set As"
          unfolding Cons by simp_all
        from Pfun(8) have at_p':"(As!i)|_p' = Fun g ts" 
          unfolding Cons by simp
        from Pfun(2) have a_wf:"As!i ∈ wf_pterm R"
          using i nth_mem by blast 
        from Pfun(3) have b_wf:"Bs!i ∈ wf_pterm R" 
          unfolding B using i l by auto
        from Pfun(4) have a_lin:"linear_term (As!i)" 
          using i by simp
        {fix α r assume "(α, r) ∈ set (redex_patterns (As!i))" 
          then have "(α, i#r) ∈ set (redex_patterns (Pfun f As))"
            by (meson i redex_patterns_elem_fun') 
          with Pfun(5) have "(α, r) ∈ set (redex_patterns (Bs!i)) ∧ i#r ∈ fun_poss (source (Pfun f As))" 
            unfolding B by (metis list.inject redex_patterns_elem_fun) 
          then have "(α, r) ∈ set (redex_patterns (Bs!i)) ∧ r ∈ fun_poss (source (As!i))" 
            using i by simp
        } moreover {fix α r assume "(α, r) ∈ set (redex_patterns (Bs!i))" and r:"r ∈ fun_poss (source (As!i))" 
          then have "(α, i#r) ∈ set (redex_patterns B)"
            unfolding B using i l by (metis redex_patterns_elem_fun') 
          moreover from r have "i#r ∈ fun_poss (source (Pfun f As))" 
            using i unfolding source.simps fun_poss.simps length_map by simp
          ultimately have "(α, r) ∈ set (redex_patterns (As!i))" 
            using Pfun(5) i by (metis list.inject redex_patterns_elem_fun) 
        }
        ultimately have rdp:"⋀α r. ((α, r) ∈ set (redex_patterns (As ! i))) = ((α, r) ∈ set (redex_patterns (Bs ! i)) ∧ r ∈ fun_poss (source (As ! i)))" 
          by blast
        from Pfun(6) have sigma:"source (As!i) ⋅ σ = source (Bs!i)"
          unfolding B source.simps eval_term.simps using i l using map_nth_conv by fastforce 
        from Pfun(1)[OF a a_wf b_wf a_lin rdp sigma p' at_p' a_wf b_wf a_lin rdp sigma] 
          obtain ss where "length ts = length ss" and "Bs!i |_ p' = Fun g ss" by blast
        then show ?thesis unfolding B Cons using i l by simp
      qed
    next
      case (Prule α As)
      from Prule(5) have "(α, []) ∈ set (redex_patterns B)" 
        by auto 
      then obtain Bs where B:"B = Prule α Bs"
        by (smt (verit, ccfv_threshold) Prule.prems(2) in_set_idx in_set_simps(3) redex_patterns_elem_fun less_nat_zero_code list.distinct(1) 
            nat_neq_iff nth_Cons_0 order_pos.dual_order.refl prod.inject redex_patterns.simps(1) redex_patterns.simps(3) redex_patterns_order wf_pterm.simps) 
      with Prule(2,3) have l:"length As = length Bs"
        using length_args_well_Prule by blast 
      show ?case proof(cases p)
        case Nil
        from Prule(8) show ?thesis unfolding Nil B using l by simp
      next
        case (Cons i p')
        from Prule(7) have i:"i < length As" and p':"p' ∈ poss (As!i)" and a:"As!i ∈ set As"
          unfolding Cons by simp_all
        from Prule(8) have at_p':"(As!i)|_p' = Fun g ts" 
          unfolding Cons by simp
        from Prule(2) have a_wf:"As!i ∈ wf_pterm R"
          using i nth_mem by blast 
        from Prule(3) have b_wf:"Bs!i ∈ wf_pterm R" 
          unfolding B using i l by auto
        from Prule(4) have a_lin:"linear_term (As!i)" 
          using i by simp
        let ?pi="var_poss_list (lhs α) ! i" 
        let ?xi="vars_term_list (lhs α) ! i"
        have i':"i < length (var_poss_list (lhs α))" 
          using i Prule(2) by (metis Inl_inject is_Prule.simps(1) is_Prule.simps(3) length_var_poss_list length_var_rule term.distinct(1) term.inject(2) wf_pterm.simps) 
        have eval_lhs':"⋀σ. lhs α ⋅ σ |_ ?pi = σ ?xi"
          by (metis eval_term.simps(1) i' length_var_poss_list nth_mem subt_at_subst var_poss_imp_poss var_poss_list_sound vars_term_list_var_poss_list)
        then have eval_lhs:"⋀σ q. lhs α ⋅ σ |_ (?pi@q) = σ ?xi |_ q"
          by (smt (verit) i' nth_mem poss_imp_subst_poss subt_at_append var_poss_imp_poss var_poss_list_sound) 
        have "i < length (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs α)) (map redex_patterns Bs))" 
          unfolding length_map length_zip using i l i' by simp
        moreover have "zip (var_poss_list (lhs α)) (map redex_patterns Bs) ! i = (?pi, redex_patterns (Bs!i))"
          using i i' l by force  
        ultimately have map_rdp:"(map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs α)) (map redex_patterns Bs))!i =  map (λ(α, p2). (α, ?pi @ p2)) (redex_patterns (Bs!i))"
          by simp
        have l':"length (var_rule α) = length (vars_term_list (lhs α))"
          using B Prule.prems(2) left_lin.length_var_rule left_lin_axioms wf_pterm.simps by fastforce 
        {fix β r assume βr:"(β, r) ∈ set (redex_patterns (As!i))" 
          from i' have "(β, ?pi@r) ∈ set (redex_patterns (Prule α As))"
            using redex_patterns_elem_rule'[OF βr i] by simp
          with Prule(5) have 1:"(β, ?pi@r) ∈ set (redex_patterns B)" and 2:"?pi@r ∈ fun_poss (source (Prule α As))"
            by presburger+  
          from 1 have "(β, r) ∈ set (redex_patterns (Bs!i))"
            using redex_patterns_rule'' by (metis B Prule.prems(2) i l) 
          moreover have "r ∈ fun_poss (source (As!i))"
            by (metis βr a_wf get_label_imp_labelposs labeled_source_to_term labelposs_subs_fun_poss_source left_lin_no_var_lhs.redex_patterns_label left_lin_no_var_lhs_axioms option.distinct(1) poss_term_lab_to_term) 
          ultimately have "(β, r) ∈ set (redex_patterns (Bs!i)) ∧ r ∈ fun_poss (source (As!i))" 
            by simp
        } moreover {fix β r assume βr:"(β, r) ∈ set (redex_patterns (Bs!i))" and r:"r ∈ fun_poss (source (As!i))" 
          let ?x="var_rule α ! i" 
          from l' have x:"lhs α |_ ?pi = Var ?x" 
            using i by (metis comp_apply eval_lhs' length_remdups_eq length_rev rev_rev_ident subst_apply_term_empty) 
          with r have r:"r ∈ fun_poss (lhs α |_ ?pi ⋅ ⟨map source As⟩⇩α)"
            using lhs_subst_var_i l' i i' by (metis (mono_tags, lifting) eval_term.simps(1) length_map length_var_poss_list nth_map) 
          from βr have "(β, ?pi@r) ∈ set (redex_patterns B)"
            unfolding B using i l using redex_patterns_elem_rule'[OF βr i[unfolded l] i'] by simp
          moreover from r x have "?pi@r ∈ fun_poss (source (Prule α As))" 
            using i unfolding source.simps fun_poss.simps
            by (metis (no_types, lifting) eval_lhs eval_lhs' fun_poss_fun_conv fun_poss_imp_poss i' is_FunI nth_mem 
                pos_append_poss poss_imp_subst_poss poss_is_Fun_fun_poss subt_at_subst var_poss_imp_poss var_poss_list_sound)
          ultimately have "(β, ?pi @ r) ∈ set (redex_patterns (Prule α As))" 
            using Prule(5) by presburger
          then have "(β, r) ∈ set (redex_patterns (As!i))" 
            using i redex_patterns_rule'' Prule.prems(1) by blast 
        }
        ultimately have rdp:"⋀α r. ((α, r) ∈ set (redex_patterns (As ! i))) = ((α, r) ∈ set (redex_patterns (Bs ! i)) ∧ r ∈ fun_poss (source (As ! i)))" 
          by blast
        from Prule(6) have sigma:"source (As!i) ⋅ σ = source (Bs!i)"
          unfolding B source.simps eval_term.simps using i l map_nth_conv
          by (smt (verit, best) B Inl_inject Prule.prems(2) apply_lhs_subst_var_rule comp_apply eval_lhs' i' is_Prule.simps(1) is_Prule.simps(3) length_map length_remdups_eq length_rev length_var_rule nth_mem poss_imp_subst_poss rev_swap subt_at_subst term.distinct(1) term.inject(2) var_poss_imp_poss var_poss_list_sound wf_pterm.simps)
        from Prule(1)[OF a a_wf b_wf a_lin rdp sigma p' at_p' a_wf b_wf a_lin rdp sigma] 
          obtain ss where "length ts = length ss" and "Bs!i |_ p' = Fun g ss" by blast
        then show ?thesis unfolding B Cons using i l by simp
      qed
    qed simp
  }
  then show ?thesis using fun_poss_eq_imp_matches[OF assms(3)] by simp
qed 
end

context left_lin_wf_trs
begin
lemma join_single_steps_wf:
  assumes "A ∈ wf_pterm R"
  and "As = filter f (single_steps A)" and "As ≠ []"
  shows "∃D. join_list As = Some D ∧ D ∈ wf_pterm R"
proof-
  {fix a1 a2 assume a1:"a1 ∈ set (single_steps A)" and a2:"a2 ∈ set (single_steps A)"
    with assms(1,2) have "a1 ⊥⇩_p a2 ∨ a1 = a2" 
      using single_steps_orth by presburger
    moreover from a1 have "a1 ∈ wf_pterm R" 
      using single_step_wf[OF assms(1)] assms(2) by presburger
    moreover from a2 have "a2 ∈ wf_pterm R" 
      using single_step_wf[OF assms(1)] assms(2) by presburger
    ultimately have "a1 ⊔ a2 ≠ None" 
      using join_same orth_imp_join_defined no_var_lhs by fastforce
  } 
  then show ?thesis using left_lin_no_var_lhs.join_list_defined[OF ll_no_var_lhs] assms(2,3) single_step_wf[OF assms(1)] by simp
qed

lemma single_steps_join_list:
  assumes "join_list As = Some A" and "∀a ∈ set As. a ∈ wf_pterm R"
  shows "set (single_steps A) = ⋃ (set (map (set ∘ single_steps) As))"  
proof-
  have rdp:"set (redex_patterns A) = ⋃ (set (map (set ∘ redex_patterns) As))" 
    using left_lin_no_var_lhs.redex_patterns_join_list assms ll_no_var_lhs by blast 
  {fix a assume "a ∈ set (single_steps A)" 
    then obtain α p where a:"a = ll_single_redex (source A) p α" and "(α, p) ∈ set (redex_patterns A)" by auto
    with rdp obtain Ai where Ai:"Ai ∈ set As" and "(α, p) ∈ set (redex_patterns Ai)" by auto
    then have "a ∈ set (single_steps Ai)" 
      unfolding a using left_lin_no_var_lhs.source_join_list[OF ll_no_var_lhs assms] by force
    with Ai have "a ∈ ⋃ (set (map (set ∘ single_steps) As))" by auto
  } moreover 
  {fix a assume "a ∈ ⋃ (set (map (set ∘ single_steps) As))"
    then obtain Ai where Ai:"Ai ∈ set As" "a ∈ set (single_steps Ai)"
      by (smt (verit, best) UnionE comp_def in_set_idx length_map map_nth_eq_conv nth_mem)
    then obtain α p where a:"a = ll_single_redex (source Ai) p α" and "(α, p) ∈ set (redex_patterns Ai)" by auto
    with rdp Ai have "(α, p) ∈ set (redex_patterns A)" by auto
    then have "a ∈ set (single_steps A)" 
      unfolding a using left_lin_no_var_lhs.source_join_list[OF ll_no_var_lhs assms] Ai by force
  }
  ultimately show ?thesis by fastforce
qed
end

end