Theory CP

theory CP
imports Renaming_Interpretations
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014, 2015, 2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Critical Pairs›

theory CP
imports
  QTRS.Unification_More
  QTRS.Renaming_Interpretations
begin

definition
  overlap ::
    "('f, 'v :: infinite) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) rule ⇒ bool"
where
  "overlap R R' r p r' ⟷
    (∃p. p ∙ r ∈ R) ∧
    (∃p. p ∙ r' ∈ R') ∧
    vars_rule r ∩ vars_rule r' = {} ∧
    p ∈ funposs (fst r') ∧
    (∃σ :: ('f, 'v) subst. fst r ⋅ σ = (fst r' |_  p) ⋅ σ) ∧
    (p = ε ⟶ ¬ (∃p. p ∙ r = r'))"

lemma overlap_right:
  fixes R1 R2 :: "('f, 'v::infinite) trs"
  assumes "overlap R1 R2 r1 p r2"
  obtains π where "overlap R1 R2 (π ∙ r1) p (π ∙ r2)" and "(π ∙ r2) ∈ R2"
proof -
  obtain π1 and π2
    where 1 ∙ r1 ∈ R1" and 2 ∙ r2 ∈ R2"
    and "vars_rule r1 ∩ vars_rule r2 = {}"
    and "p ∈ funposs (fst r2)"
    and "∃σ::('f, 'v) subst. fst r1 ⋅ σ = (fst r2 |_ p) ⋅ σ"
    and "p = ε ⟶ ¬ (∃p. p ∙ r1 = r2)"
    using assms unfolding overlap_def by blast
  then have "(π1 + -π2) ∙ (π2 ∙ r1) ∈ R1" and "0 ∙ (π2 ∙ r2) ∈ R2"
    and "vars_rule (π2 ∙ r1) ∩ vars_rule (π2 ∙ r2) = {}"
    and "p ∈ funposs (fst (π2 ∙ r2))"
    and "∃σ::('f, 'v) subst. fst (π2 ∙ r1) ⋅ σ = (fst (π2 ∙ r2) |_ p) ⋅ σ"
    and "p = ε ⟶ ¬ (∃p. p ∙ (π2 ∙ r1) = π2 ∙ r2)"
         apply (auto simp: eqvt [symmetric])
      apply (rule_tac x = "sop (-π2) ∘s σ" in exI)
      apply (simp add: funposs_imp_poss subt_at_eqvt)
     apply (rule_tac x = "sop (-π2) ∘s σ" in exI)
     apply (simp add: funposs_imp_poss subt_at_eqvt)
    by (metis rule_pt.permute_minus_cancel(2) rule_pt.permute_plus)
  then show thesis
    apply (intro that [of π2])
     apply (unfold overlap_def)
     apply blast
    apply auto
    done
qed

text ‹Critical peaks are single-step rewrite peaks originating from overlaps.›
definition
  cpeaks2 ::
    "('f, 'v :: infinite) trs ⇒ ('f, 'v) trs ⇒
    (('f, 'v) term × pos × ('f, 'v) term × ('f, 'v) term) set"
where
  "cpeaks2 R R' = {(replace_at (fst r') p (snd r) ⋅ σ, p, fst r' ⋅ σ, snd r' ⋅ σ) |
    r p r' σ. overlap R R' r p r' ∧ σ = the_mgu (fst r) (fst r' |_ p)}"

abbreviation "cpeaks R ≡ cpeaks2 R R"

lemma cpeaks2_I:
  assumes "overlap R R' r p r'" and "σ = the_mgu (fst r) (fst r' |_ p)"
  shows "(replace_at (fst r') p (snd r) ⋅ σ, p, fst r' ⋅ σ, snd r' ⋅ σ) ∈ cpeaks2 R R'"
  using assms by (force simp: cpeaks2_def)

inductive_set S3 for A
where
  subst: "(t, p, s, u) ∈ A ⟹ (t ⋅ σ, p, s ⋅ σ, u ⋅ σ) ∈ S3 A"

lemma peak_above_imp_join_or_cpeaks:
  fixes R :: "('f, 'v :: infinite) trs"
    and σ1 σ2 :: "('f, 'v) subst"
  assumes rule_variants: "∃π. π ∙ (l1, r1) ∈ R" "∃π. π ∙ (l2, r2) ∈ R"
    and disj: "vars_rule (l1, r1) ∩ vars_rule (l2, r2) = {}"
    and "p2 ≤ p1"

    and "vars_term r1 ⊆ vars_term l1"
    and p1: "p1 ∈ poss s"
    and sp1: "s |_ p1 = l1 ⋅ σ1"
    and t: "t = replace_at s p1 (r1 ⋅ σ1)"

    and p2: "p2 ∈ poss s"
    and sp2: "s |_ p2 = l2 ⋅ σ2"
    and u: "u = replace_at s p2 (r2 ⋅ σ2)"

  shows "(t, u) ∈ (rstep R) ∨
    (p2 ∈ poss s ∧
    (ctxt_of_pos_term p2 s)⟨t |_ p2⟩ = t ∧
    (ctxt_of_pos_term p2 s)⟨u |_ p2⟩ = u ∧
    (t |_ p2, pos_diff p1 p2, s |_ p2, u |_ p2) ∈ S3 (cpeaks R))"
proof -
  define p where "p = pos_diff p1 p2"
  have p1_eq: "p1 = p2 <#> p" using ‹p2 ≤ p1 by (simp add: p_def)
  then have t: "t = replace_at s p2 (replace_at (l2 ⋅ σ2) p (r1 ⋅ σ1))"
    by (simp add: t ctxt_of_pos_term_append p2 sp2)
  show ?thesis
  proof (cases "p ∈ funposs l2 ∧ (p = ε ⟶ ¬ (∃π. π ∙ (l1, r1) = (l2, r2)))")
    case True
    define σ' where "σ' x = (if x ∈ vars_rule (l1, r1) then σ1 x else σ2 x)" for x

    have p: "p ∈ funposs l2" and "p = ε ⟹ ¬ (∃π. π ∙ (l1, r1) = (l2, r2))" using True by auto
    moreover
    have unif: "l1 ⋅ σ' = (l2 |_ p) ⋅ σ'"
    proof -
      note coinc = coincidence_lemma' [of l1 "vars_rule (l1, r1)"]
      have disj: "vars_rule (l1, r1) ∩ vars_term (l2 |_ p) = {}"
        using vars_term_subt_at [OF funposs_imp_poss [OF p]] and disj
        by (auto simp: vars_rule_def)
      have "l1 ⋅ σ' = l1 ⋅ (σ' |s vars_rule (l1, r1))"
        using coinc by (simp add: vars_rule_def)
      also have "… = l1 ⋅ (σ1 |s vars_rule (l1, r1))" by (simp add: σ'_def [abs_def])
      also have "… = l1 ⋅ σ1" using coinc by (simp add: vars_rule_def)
      also have "… = (l2 ⋅ σ2) |_ p" using subt_at_append [OF p2] and sp1 by (simp add: p1_eq sp2)
      also have "… = (l2 |_ p) ⋅ σ2" using funposs_imp_poss [OF p] by simp
      also have "… = (l2 |_ p) ⋅ (σ2 |s vars_term (l2 |_ p))"
        by (simp add: coincidence_lemma [symmetric])
      also have "… = (l2 |_ p) ⋅ (σ' |s vars_term (l2 |_ p))" using disj by (simp add: σ'_def [abs_def])
      finally show ?thesis by (simp add: coincidence_lemma [symmetric])
    qed
    ultimately
    have overlap: "overlap R R (l1, r1) p (l2, r2)"
      using disj and rule_variants by (auto simp: overlap_def)

    define σ where "σ = the_mgu l1 (l2 |_ p)"
    have cpeaks: "(replace_at l2 p r1 ⋅ σ, p, l2 ⋅ σ, r2 ⋅ σ) ∈ cpeaks R"
      using cpeaks2_I [OF overlap refl] by (simp add: σ_def)

    have "is_mgu σ {(l1, l2 |_ p)}" by (rule is_mguI) (insert unif the_mgu, auto simp: σ_def)
    with unif obtain τ where σ': "σ' = σ ∘s τ" by (auto simp: is_mgu_def unifiers_def)
    have "(replace_at (l2 ⋅ σ2) p (r1 ⋅ σ1), p, l2 ⋅ σ2, r2 ⋅ σ2) ∈ S3 (cpeaks R)"
    proof -
      have "l2 ⋅ σ2 = l2 ⋅ σ'"
      proof -
        have disj: "vars_rule (l1, r1) ∩ vars_term l2 = {}" using disj by (auto simp: vars_rule_def)
        have "l2 ⋅ σ' = l2 ⋅ (σ' |s vars_term l2)" by (rule coincidence_lemma)
        also have "… = l2 ⋅ (σ2 |s vars_term l2)" using disj by (simp add: σ'_def [abs_def])
        also have "… = l2 ⋅ σ2" by (simp add: coincidence_lemma [symmetric])
        finally show ?thesis ..
      qed
      moreover
      have "r1 ⋅ σ1 = r1 ⋅ σ'"
      proof -
        note coinc = coincidence_lemma' [of r1 "vars_rule (l1, r1)"]
        have "r1 ⋅ σ' = r1 ⋅ (σ' |s vars_rule (l1, r1))"
          using coinc by (simp add: vars_rule_def)
        also have "… = r1 ⋅ (σ1 |s vars_rule (l1, r1))" by (simp add: σ'_def [abs_def])
        also have "… = r1 ⋅ σ1" using coinc by (simp add: vars_rule_def)
        finally show ?thesis ..
      qed
      moreover
      have "r2 ⋅ σ2 = r2 ⋅ σ'"
      proof -
        have disj: "vars_rule (l1, r1) ∩ vars_term r2 = {}" using disj by (auto simp: vars_rule_def)
        have "r2 ⋅ σ' = r2 ⋅ (σ' |s vars_term r2)" by (rule coincidence_lemma)
        also have "… = r2 ⋅ (σ2 |s vars_term r2)" using disj by (simp add: σ'_def [abs_def])
        also have "… = r2 ⋅ σ2" by (simp add: coincidence_lemma [symmetric])
        finally show ?thesis ..
      qed
      ultimately
      show ?thesis using cpeaks
        using S3.intros [OF cpeaks, of τ]
        and funposs_imp_poss [OF p]
        by (simp add: σ' ctxt_of_pos_term_subst)
    qed
    moreover have "p2 ∈ poss s" by fact
    ultimately show ?thesis using p2 and sp2 by (auto simp: t u p_def replace_at_subt_at)
  next
    case False
    then have "(p = ε ∧ (∃π. π ∙ (l1, r1) = (l2, r2))) ∨ p ∉ funposs l2" by blast
    then show ?thesis
    proof (elim disjE conjE exE)
      txt ‹The variable condition is only needed here.›
      fix π
      assume [simp]: "p = ε" and "π ∙ (l1, r1) = (l2, r2)"
      then have "p2 = p1" and "l2 = π ∙ l1" and [simp]: "r2 = π ∙ r1" by (simp_all add: p1_eq eqvt)
      then have "l1 ⋅ σ1 = l1 ⋅ (σ2 ∘ Rep_perm π)"
        using sp1 and sp2 by (simp add: permute_term_subst_apply_term)
      moreover
      have "vars_term r1 ⊆ vars_term l1" by fact
      ultimately
      have "r1 ⋅ σ1 = r1 ⋅ (σ2 ∘ Rep_perm π)" using vars_term_subset_subst_eq by blast
      then have "r1 ⋅ σ1 = π ∙ r1 ⋅ σ2" by (simp add: permute_term_subst_apply_term)
      then show ?thesis by (auto simp: t u)
    next
      txt ‹Variable overlap.›
      have step1: "(l1, r1) ∈ rstep R" and step2: "(l2, r2) ∈ rstep R"
        using rule_variants by (auto simp: eqvt) (metis rstep.rule rstep_permute_iff)+
      have "p ∈ poss (l2 ⋅ σ2)" by (metis p1_eq p1 poss_append_poss sp2)
      moreover
      assume "p ∉ funposs l2"
      ultimately
      obtain q1 q2 x
        where [simp]: "p = q1 <#> q2" and q1: "q1 ∈ poss l2"
        and l2q1: "l2 |_ q1 = Var x" and q2: "q2 ∈ poss (σ2 x)"
        by (rule poss_subst_apply_term)
      moreover
      have [simp]: "l2 ⋅ σ2 |_ p = l1 ⋅ σ1" by (metis p1_eq p2 sp1 sp2 subt_at_append)
      ultimately
      have [simp]: 2 x |_ q2 = l1 ⋅ σ1" by simp

      define σ2' where 2' y = (if y = x then replace_at (σ2 x) q2 (r1 ⋅ σ1) else σ2 y)" for y

      have "(σ2 x, σ2' x) ∈ rstep R"
      proof -
        let ?C = "ctxt_of_pos_term q22 x)"
        have "(?C⟨l1 ⋅ σ1⟩, ?C⟨r1 ⋅ σ1⟩) ∈ rstep R" using step1 by blast
        then show ?thesis using q2 by (simp add: σ2'_def replace_at_ident)
      qed
      then have *: "⋀x. (σ2 x, σ2' x) ∈ (rstep R)*" by (auto simp: σ2'_def)
      then have "(r2 ⋅ σ2, r2 ⋅ σ2') ∈ (rstep R)*" by (rule substs_rsteps)
      then have "(u, replace_at s p2 (r2 ⋅ σ2')) ∈ (rstep R)*" by (auto simp: u rsteps_closed_ctxt)
      moreover
      have "(t, replace_at s p2 (r2 ⋅ σ2')) ∈ (rstep R)*"
      proof -
        have "replace_at (l2 ⋅ σ2) p (r1 ⋅ σ1) = replace_at (l2 ⋅ σ2) q12' x)"
          using q1 and q2 by (simp add: σ2'_def ctxt_of_pos_term_append l2q1)
        moreover
        have "(replace_at (l2 ⋅ σ2) q12' x), l2 ⋅ σ2') ∈ (rstep R)*"
          by (rule replace_at_subst_rsteps [OF * q1 l2q1])
        moreover
        have "(l2 ⋅ σ2', r2 ⋅ σ2') ∈ rstep R" using step2 by blast
        ultimately
        have "(replace_at (l2 ⋅ σ2) p (r1 ⋅ σ1), r2 ⋅ σ2') ∈ (rstep R)*" by auto
        then show ?thesis by (auto simp: p2 t rsteps_closed_ctxt)
      qed
      ultimately show ?thesis by blast
    qed
  qed
qed

lemma parallel_peak_imp_join:
  fixes p1 p2 :: "pos"
  assumes parallel: "p1 ⊥ p2"
    and peak: "(s, t) ∈ rstep_pos R p1" "(s, u) ∈ rstep_pos R p2"
  shows "(t, u) ∈ (rstep R)"
  using parallel_steps [OF _ _ parallel, of s t R _ _ _ u] and peak
  apply (auto simp: join_def rstep_pos_rstep_r_p_s_conv simp del: reverseTrs)
  apply (intro relcompI r_into_rtrancl)
  by (fastforce simp add: rstep_iff_rstep_r_p_s)+

text ‹Peaks are either joinable or contain an instance of a critical peak.›
(*Lemma 5.1.9*)
lemma peak_imp_join_or_S3_cpeaks:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes variable_condition: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and peak: "(s, t) ∈ rstep_pos R p1" "(s, u) ∈ rstep_pos R p2"
  shows "(t, u) ∈ (rstep R) ∨ (
    (p2 ≤ p1 ∧ (ctxt_of_pos_term p2 s)⟨t |_ p2⟩ = t ∧ (ctxt_of_pos_term p2 s)⟨u |_ p2⟩ = u ∧
      (t |_ p2, pos_diff p1 p2, s |_ p2, u |_ p2) ∈ S3 (cpeaks R)) ∨
    (p1 ≤ p2 ∧ (ctxt_of_pos_term p1 s)⟨t |_ p1⟩ = t ∧ (ctxt_of_pos_term p1 s)⟨u |_ p1⟩ = u ∧
      (u |_ p1, pos_diff p2 p1, s |_ p1, t |_ p1) ∈ S3 (cpeaks R)))"
proof -
  obtain l1' r1' σ1' l2 r2 σ2
    where rule1': "(l1', r1') ∈ R" and rule2: "(l2, r2) ∈ R"
    and p1: "p1 ∈ poss s" and p2: "p2 ∈ poss s"
    and s1': "replace_at s p1 (l1' ⋅ σ1') = s" and t': "t = replace_at s p1 (r1' ⋅ σ1')"
    and s2: "replace_at s p2 (l2 ⋅ σ2) = s" and u: "u = replace_at s p2 (r2 ⋅ σ2)"
    using rstep_pos.cases [OF peak(1)]
      and rstep_pos.cases [OF peak(2)]
      by (metis ctxt_supt_id)

  from vars_rule_disjoint obtain π1
    where π1: "vars_rule (π1 ∙ (l1', r1')) ∩ vars_rule (l2, r2) = {}" ..
  define l1 and r1 and σ1
    where "l1 = π1 ∙ l1'" and "r1 = π1 ∙ r1'" and 1 = (Var ∘ Rep_perm (-π1)) ∘s σ1'"
  note rename = l1_def r1_def σ1_def

  have disj: "vars_rule (l1, r1) ∩ vars_rule (l2, r2) = {}" using π1 by (auto simp: eqvt rename)
  have s1: "replace_at s p1 (l1 ⋅ σ1) = s" and t: "t = replace_at s p1 (r1 ⋅ σ1)"
    by (simp_all add: s1' t' rename)

  have "-π1 ∙ (l1, r1) ∈ R" and "0 ∙ (l2, r2) ∈ R"
    using rule1' and rule2 by (simp_all add: rename)
  then have rule_variants: "∃π. π ∙ (l1, r1) ∈ R" "∃π. π ∙ (l2, r2) ∈ R" by blast+

  show ?thesis
  proof (cases "p1 ⊥ p2")
    assume "p1 ⊥ p2"
    moreover
    have "(s, t) ∈ rstep_r_p_s R (l1', r1') p1 σ1'"
      by (simp add: p1 rstep_r_p_s_def s1' t' rule1')
    moreover
    have "(s, u) ∈ rstep_r_p_s R (l2, r2) p2 σ2"
      by (simp add: p2 rstep_r_p_s_def s2 u rule2)
    ultimately
    obtain v where "(t, v) ∈ rstep R" and "(u, v) ∈ rstep R"
      by (blast dest: parallel_steps rstep_r_p_s_imp_rstep)
    then show ?thesis by blast
  next
    have sp1: "s |_ p1 = l1 ⋅ σ1" using s1 and p1 by (metis replace_at_subt_at)
    have sp2: "s |_ p2 = l2 ⋅ σ2" using s2 and p2 by (metis replace_at_subt_at)

    assume "¬ (p1 ⊥ p2)"
    then have "p1 ≤ p2 ∨ p2 ≤ p1" by (metis parallel_pos)
    then show ?thesis
    proof
      have vars: "vars_term r1 ⊆ vars_term l1"
        using variable_condition [THEN bspec, OF rule1']
        and atom_set_pt.permute_set_subset [of "vars_term r1'" "vars_term l1'"]
        by (auto simp add: rename supp_vars_term_eq [symmetric] term_fs.supp_eqvt [symmetric])
      assume "p2 ≤ p1"
      with peak_above_imp_join_or_cpeaks [OF rule_variants disj this vars p1 sp1 t p2 sp2 u]
        show ?thesis by (auto simp: s2)
    next
      have vars: "vars_term r2 ⊆ vars_term l2"
        using variable_condition [THEN bspec, OF rule2] by blast
      have disj: "vars_rule (l2, r2) ∩ vars_rule (l1, r1) = {}" using disj by blast
      assume "p1 ≤ p2"
      with peak_above_imp_join_or_cpeaks [OF rule_variants(2, 1) disj this vars p2 sp2 u p1 sp1 t]
        show ?thesis by (auto simp: s1)
    qed
  qed
qed

inductive_set CS3 for A
where
  "(t, p, s, u) ∈ A ⟹ (C⟨t ⋅ σ⟩, hole_pos C <#> p, C⟨s ⋅ σ⟩, C⟨u ⋅ σ⟩) ∈ CS3 A"

lemma CS3_imp_rstep:
  assumes "(t, p, s, u) ∈ CS3 A"
  shows "(t, u) ∈ rstep ((λ(w, x, y, z). (w, z)) ` A)"
  using assms by (cases) force

lemma S3_imp_CS3:
  assumes "p ∈ poss s"
    and S3: "(v, q, s |_ p, w) ∈ S3 A"
  shows "((ctxt_of_pos_term p s)⟨v⟩, p <#> q, s, (ctxt_of_pos_term p s)⟨w⟩) ∈ CS3 A"
using S3
proof (cases)
  case (subst t' s' u' σ)
  with CS3.intros [OF subst(4), of "ctxt_of_pos_term p s" σ]
    show ?thesis by (simp add: assms replace_at_ident)
qed

lemma peak_imp_join_or_CS3_cpeaks:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes vc: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and peak: "(s, t) ∈ rstep R" "(s, u) ∈ rstep R"
  shows "(t, u) ∈ (rstep R) ∨ (∃p. (t, p, s, u) ∈ CS3 (cpeaks R) ∨ (u, p, s, t) ∈ CS3 (cpeaks R))"
proof -
  from peak obtain p q
    where peak: "(s, t) ∈ rstep_pos R p" "(s, u) ∈ rstep_pos R q"
    by (auto simp: rstep_rstep_pos_conv)
  then have "p ∈ poss s" and "q ∈ poss s" by (auto elim: rstep_pos.cases)
  with peak_imp_join_or_S3_cpeaks [OF vc peak]
    show ?thesis by (auto dest: S3_imp_CS3)
qed

definition
  CP2 :: "('f, 'v::infinite) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule set"
where
  "CP2 R R' = {(replace_at (fst r') p (snd r) ⋅ σ, snd r' ⋅ σ) |
    r p r' σ. overlap R R' r p r' ∧ σ = the_mgu (fst r) (fst r' |_ p)}"

abbreviation "CP R ≡ CP2 R R"

lemma CP2_I:
  assumes "overlap R R' r p r'" and "σ = the_mgu (fst r) (fst r' |_ p)"
  shows "(replace_at (fst r') p (snd r) ⋅ σ, snd r' ⋅ σ) ∈ CP2 R R'"
  using assms by (force simp: CP2_def)

lemma CP2_cpeaks2_conv:
  "CP2 R R' = (λ(t, p, s, u). (t, u)) ` cpeaks2 R R'"
  by (force simp: CP2_def cpeaks2_def)

lemma peak_imp_join_or_CP:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and "(s, t) ∈ rstep R" "(s, u) ∈ rstep R"
  shows "(t, u) ∈ (rstep R) ∨ (t, u) ∈ (rstep (CP R))"
  using peak_imp_join_or_CS3_cpeaks [OF assms]
  by (auto simp: CP2_cpeaks2_conv dest: CS3_imp_rstep simp del: reverseTrs)

lemma CP_join_imp_peak_join:
  assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and *: "∀(s, t)∈CP R. (s, t) ∈ (rstep R)"
  shows "(rstep R)¯ O (rstep R) ⊆ (rstep R)"
proof -
  have "(rstep (CP R)) ⊆ (rstep R)"
  proof (intro subrelI)
    fix s t
    assume "(s, t) ∈ (rstep (CP R))"
    then have "(s, t) ∈ rstep (CP R) ∨ (t, s) ∈ rstep (CP R)" by auto
    then show "(s, t) ∈ (rstep R)"
    proof
      assume "(s, t) ∈ rstep (CP R)"
      then obtain C σ u v where cp: "(u, v) ∈ CP R"
        and [simp]: "s = C⟨u ⋅ σ⟩" "t = C⟨v ⋅ σ⟩" by auto
      from * [THEN bspec, OF cp] show ?thesis by auto
    next
      assume "(t, s) ∈ rstep (CP R)"
      then obtain C σ u v where cp: "(u, v) ∈ CP R"
        and [simp]: "t = C⟨u ⋅ σ⟩" "s = C⟨v ⋅ σ⟩" by auto
      show ?thesis by (rule join_sym) (insert * [THEN bspec, OF cp], auto)
    qed
  qed
  with peak_imp_join_or_CP [OF assms(1)] show ?thesis by blast
qed

lemma CP2_imp_peak:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "(s, t) ∈ CP2 R S"
  shows "(s, t) ∈ (rstep R)¯ O (rstep S)"
proof -
  from assms obtain r p r' σ
    where overlap: "overlap R S r p r'"
    and σ: "σ = the_mgu (fst r) (fst r' |_ p)"
    and s: "s = replace_at (fst r') p (snd r) ⋅ σ"
    and t: "t = snd r' ⋅ σ"
    by (auto simp: CP2_def)
  obtain l1 r1 l2 r2
    where [simp]: "r = (l1, r1)" "r' = (l2, r2)" by (cases r, cases r') auto
  from overlap obtain π1 π2 and τ :: "('f, 'v) subst"
    where 1 ∙ (l1, r1) ∈ R" and 2 ∙ (l2, r2) ∈ S"
    and p: "p ∈ funposs l2"
    and unif: "l1 ⋅ τ = l2 |_ p ⋅ τ"
    by (auto simp: overlap_def)
  then have 1 ∙ (l1, r1) ∈ rstep R" and 2 ∙ (l2, r2) ∈ rstep S"
    by (metis rstep.rule surjective_pairing)+
  then have "(l1, r1) ∈ rstep R" and "(l2, r2) ∈ rstep S"
    by (metis perm_rstep_imp_rstep rule_pt.permute_prod.simps)+
  then have "((ctxt_of_pos_term p l2)⟨l1⟩ ⋅ σ, s) ∈ rstep R"
    and "(l2 ⋅ σ, t) ∈ rstep S" by (auto simp: s t)
  moreover
  have "replace_at (l2) p (l1) ⋅ σ = l2 ⋅ σ"
    using the_mgu [OF unif] and funposs_imp_poss [OF p]
    by (auto simp: σ) (metis replace_at_ident subst_apply_term_ctxt_apply_distrib)
  ultimately
  show ?thesis by (auto) blast
qed

lemma WCR_imp_CP_join:
  assumes "(rstep R)¯ O (rstep R) ⊆ (rstep R)"
   and "(s, t) ∈ CP R"
  shows "(s, t) ∈ (rstep R)"
  using CP2_imp_peak [OF assms(2)] and assms(1) by blast

text ‹The Critical Pair Lemma›
lemma CP:
  assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
  shows "(rstep R)¯ O (rstep R) ⊆ (rstep R) ⟷ (∀(s, t)∈CP R. (s, t) ∈ (rstep R))"
  using CP_join_imp_peak_join [OF assms] and WCR_imp_CP_join [of R] by auto

text ‹A terminating TRS is confluent iff all critical pairs are joinable.›
corollary SN_imp_CR_iff_CP_join:
  assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and "SN (rstep R)"
  shows "CR (rstep R) ⟷ (∀(s, t)∈CP R. (s, t) ∈ (rstep R))"
  using Newman [OF assms(2)] and CP [OF assms(1)]
  unfolding WCR_alt_def [symmetric]
  by (simp) (metis CR_on_def WCR_onI r_into_rtrancl)

definition
  "CP2_rules_pos R R' r p r' =
    {(replace_at (fst (π2 ∙ r')) p (snd (π1 ∙ r)) ⋅ σ, snd (π2 ∙ r') ⋅ σ) | π1 π2 σ.
    mgu (fst (π1 ∙ r)) (fst (π2 ∙ r') |_ p) = Some σ ∧
    overlap R R' (π1 ∙ r) p (π2 ∙ r')}"

(*Auxiliary definition to obtain the result that only finitely many CPs have to be
considered.*)
definition
  CP2' :: "('f, 'v::infinite) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule set set"
where
  "CP2' R R' = {CP2_rules_pos R R' r p r' | r p r'. r ∈ R ∧ r' ∈ R' ∧ p ∈ funposs (fst r')}"

lemma finite_CP2':
  assumes "finite R" and "finite R'"
  shows "finite (CP2' R R')"
proof -
  let ?R = "{(r, p, r'). r ∈ R ∧ r' ∈ R' ∧ p ∈ funposs (fst r')}"
  have *: "CP2' R R' = (λ(r, p, r'). {(replace_at (fst (π2 ∙ r')) p (snd (π1 ∙ r)) ⋅ σ, snd (π2 ∙ r') ⋅ σ) |
    π1 π2 σ. mgu (fst (π1 ∙ r)) (fst (π2 ∙ r') |_ p) = Some σ ∧
    overlap R R' (π1 ∙ r) p (π2 ∙ r')}) ` ?R"
    by (fastforce simp: CP2'_def CP2_rules_pos_def)
  have "{(r, p, r'). r ∈ R ∧ r' ∈ R' ∧ p ∈ funposs (fst r')} ⊆ R × ⋃(funposs ` lhss R') × R'"
    by auto
  moreover have "finite (R × ⋃(funposs ` lhss R') × R')"
    using assms and finite_funposs by auto
  ultimately have "finite ?R" by (rule finite_subset)
  then show ?thesis unfolding * by (rule finite_imageI)
qed

lemma overlap_permute_rules:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "overlap R R' r p r'"
  shows "overlap R R' (π ∙ r) p (π ∙ r')"
  (is "overlap R R' ?r p ?r'")
proof -
  obtain π1' π2' and σ :: "('f, 'v) subst"
    where rules: 1' ∙ r ∈ R" 2' ∙ r' ∈ R'"
    and disj: "vars_rule r ∩ vars_rule r' = {}"
    and pos: "p ∈ funposs (fst r')"
    and unif: "fst r ⋅ σ = fst r' |_ p ⋅ σ"
    and triv: "p = ε ⟹ ¬ (∃π. π ∙ r = r')"
    using assms by (auto simp: overlap_def)
  have "(π1' + -π) ∙ ?r ∈ R" and "(π2' + -π) ∙ ?r' ∈ R'"
    using rules by auto
  then have "∃π. π ∙ ?r ∈ R" and "∃π. π ∙ ?r' ∈ R'" by blast+
  moreover have "vars_rule ?r ∩ vars_rule ?r' = {}"
    unfolding vars_rule_eqvt [symmetric] using disj
    unfolding atom_set_pt.inter_eqvt [symmetric] by (simp)
  moreover have pos': "p ∈ funposs (fst ?r')" using pos by (simp add: rule_pt.fst_eqvt [symmetric])
  moreover have "fst ?r ⋅ conjugate_subst π σ = fst ?r' |_ p ⋅ conjugate_subst π σ"
    using unif and funposs_imp_poss [OF pos'] and funposs_imp_poss [OF pos]
    by (simp add: eqvt [symmetric])
  moreover have "p = ε ⟹ ¬ (∃π. π ∙ ?r = ?r')"
    using triv by (auto) (metis left_minus rule_pt.permute_plus rule_pt.permute_zero)
  ultimately show ?thesis
    by (auto simp: overlap_def)
qed

lemma overlap_permuted_rules:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "overlap R R' (π ∙ r) p (π ∙ r')" (is "overlap R R' ?r p ?r'")
  shows "overlap R R' r p r'"
proof -
  obtain π1' π2' and σ :: "('f, 'v) subst"
    where rules: 1' ∙ ?r ∈ R" 2' ∙ ?r' ∈ R'"
    and disj: "vars_rule ?r ∩ vars_rule ?r' = {}"
    and pos: "p ∈ funposs (fst ?r')"
    and unif: "fst ?r ⋅ σ = fst ?r' |_ p ⋅ σ"
    and triv: "p = ε ⟹ ¬ (∃π. π ∙ ?r = ?r')"
    using assms by (auto simp: overlap_def)
  have "(π1' + π) ∙ r ∈ R" and "(π2' + π) ∙ r' ∈ R'"
    using rules by auto
  then have "∃π. π ∙ r ∈ R" and "∃π. π ∙ r' ∈ R'" by blast+
  moreover have "vars_rule r ∩ vars_rule r' = {}"
    using disj unfolding eqvt [symmetric]
    by (metis atom_set_pt.empty_eqvt atom_set_pt.permute_eq_iff)
  moreover have pos': "p ∈ funposs (fst r')" using pos by (simp add: rule_pt.fst_eqvt [symmetric])
  moreover have "fst r ⋅ ((Var ∘ Rep_perm π) ∘s σ) = fst r' |_ p ⋅ ((Var ∘ Rep_perm π) ∘s σ)"
    using unif and funposs_imp_poss [OF pos'] by (simp add: eqvt [symmetric])
  moreover have "p = ε ⟹ ¬ (∃π. π ∙ r = r')"
    using triv by (auto) (metis diff_add_cancel rule_pt.permute_plus)
  ultimately show ?thesis
    unfolding overlap_def by blast
qed

lemma overlap_perm_simp [simp]:
  "overlap R R' (π ∙ r) p (π ∙ r') = overlap R R' r p r'"
  by (metis overlap_permute_rules overlap_permuted_rules)

text ‹Overlaps that origin from the same rules at the same position are variants.›
lemma same_rule_pos_overlap_imp_perm:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "overlap R R' (π1 ∙ r) p (π2 ∙ r')"
    and "overlap R R' (π3 ∙ r) p (π4 ∙ r')"
  shows "∃π. π ∙ (π1 ∙ r) = π3 ∙ r ∧ π ∙ (π2 ∙ r') = π4 ∙ r'"
proof -
  from assms obtain τ τ' :: "('f, 'v) subst"
    where "vars_rule (π1 ∙ r) ∩ vars_rule (π2 ∙ r') = {}"
      and "vars_rule (π3 ∙ r) ∩ vars_rule (π4 ∙ r') = {}"
    by (auto simp: overlap_def dest!: funposs_imp_poss)
  from rule_variants_imp_perm [OF this(2, 1)] show ?thesis .
qed

text ‹Critical pairs that origin from overlaps which are variants are also variants
of each other.›
lemma overlap_variants_imp_CP_variants:
  fixes R R' :: "('f, 'v :: infinite) trs"
  assumes ol: "overlap R R' (π1 ∙ r) p (π2 ∙ r')"
              "overlap R R' (π3 ∙ r) p (π4 ∙ r')"
    and mgu: "mgu (fst (π1 ∙ r)) (fst (π2 ∙ r') |_ p) = Some σ" (is "mgu ?s ?t = _")
             "mgu (fst (π3 ∙ r)) (fst (π4 ∙ r') |_ p) = Some σ'" (is "mgu ?u ?v = _")
  shows "∃π.
    replace_at (fst (π2 ∙ r')) p (snd (π1 ∙ r)) ⋅ σ =
    π ∙ (replace_at (fst (π4 ∙ r')) p (snd (π3 ∙ r)) ⋅ σ') ∧
    snd (π2 ∙ r') ⋅ σ = π ∙ (snd (π4 ∙ r') ⋅ σ')"
proof -
  have "p ∈ poss (fst (π2 ∙ r'))" using ol(1) by (auto simp: overlap_def dest: funposs_imp_poss)
  then have p: "p ∈ poss (fst r')" by (simp add: eqvt [symmetric])
  have mgu': "is_mgu σ {(?s, ?t)}" "is_mgu σ' {(?u, ?v)}"
    using mgu_sound [THEN is_imgu_imp_is_mgu] and mgu by auto
  have unif: "?s ⋅ σ = ?t ⋅ σ" "?u ⋅ σ' = ?v ⋅ σ'"
    using mgu' by (auto simp: is_mgu_def)
  define s and t where "s = fst r" and "t = fst r' |_ p"
  have unif: "(π1 ∙ s) ⋅ σ = (π2 ∙ t) ⋅ σ" "(π3 ∙ s) ⋅ σ' = (π4 ∙ t) ⋅ σ'"
    using unif and p by (simp add: s_def t_def eqvt)+
  have mgu': "is_mgu σ {(π1 ∙ s, π2 ∙ t)}" "is_mgu σ' {(π3 ∙ s, π4 ∙ t)}"
    using mgu' and p by (simp add: s_def t_def eqvt)+
  from same_rule_pos_overlap_imp_perm [OF ol(2, 1)] obtain π :: "'v perm"
    where 0: 1 ∙ r = π ∙ π3 ∙ r" 2 ∙ r' = π ∙ π4 ∙ r'" by metis
  then have *: 1 ∙ s = π ∙ π3 ∙ s" 2 ∙ t = π ∙ π4 ∙ t"
    using p by (simp_all add: s_def t_def eqvt)
  then have **: 3 ∙ s = (-π) ∙ π1 ∙ s" 4 ∙ t = (-π) ∙ π2 ∙ t" by auto

  have "is_mgu (sop π ∘s σ) {(π3 ∙ s, π4 ∙ t)}"
  proof (unfold is_mgu_def, intro conjI ballI)
    fix τ :: "('f, 'v) subst"
    assume "τ ∈ unifiers {(π3 ∙ s, π4 ∙ t)}"
    then have 3 ∙ s ⋅ τ = π4 ∙ t ⋅ τ" by (simp add: unifiers_def)
    then have "(-π) ∙ π1 ∙ s ⋅ τ = (-π) ∙ π2 ∙ t ⋅ τ" by (simp add: ** )
    then have 1 ∙ s ⋅ sop (-π) ∘s τ = π2 ∙ t ⋅ sop (-π) ∘s τ" by simp
    with mgu'(1) obtain μ :: "('f, 'v) subst"
      where "sop (-π) ∘s τ = σ ∘s μ"
      unfolding is_mgu_def and unifiers_def by force
    then have "sop π ∘s sop (-π) ∘s τ = sop π ∘s σ ∘s μ" by (simp add: ac_simps)
    then have "τ = sop π ∘s σ ∘s μ" by (simp add: subst_compose_def)
    then show "∃μ. τ = sop π ∘s σ ∘s μ" by blast
  qed (simp add: unif ** unifiers_def)
  moreover have "finite (subst_domain (sop π ∘s σ))"
  proof -
    have "subst_domain (sop π ∘s σ) ⊆ subst_domain (sop π :: ('f, 'v) subst) ∪ subst_domain σ"
      using subst_domain_compose [of "sop π" σ] using [[show_sorts]] .
    moreover have "finite (subst_domain (sop π))" by (metis finite_subst_domain_sop)
    moreover have "finite (subst_domain σ)" using mgu_finite_subst_domain [OF mgu(1)] .
    ultimately show ?thesis by (metis infinite_Un infinite_super)
  qed
  moreover have "finite (subst_domain σ')" using mgu_finite_subst_domain [OF mgu(2)] .
  ultimately obtain π' where 1: "π' ∙ σ' = sop π ∘s σ"
    using is_mgu_imp_perm [OF mgu'(2)] by blast

  have "replace_at (fst (π2 ∙ r') ⋅ σ) p (snd (π1 ∙ r) ⋅ σ) =
    π' ∙ (replace_at (fst (π4 ∙ r')) p (snd (π3 ∙ r)) ⋅ σ')"
  proof -
    have "replace_at (fst (π2 ∙ r') ⋅ σ) p (snd (π1 ∙ r) ⋅ σ) =
      π ∙ replace_at (fst (π4 ∙ r')) p (snd (π3 ∙ r)) ⋅ σ"
      using p by (simp add: 0 eqvt ctxt_of_pos_term_subst)
    also have "… = π' ∙ (replace_at (fst (π4 ∙ r')) p (snd (π3 ∙ r)) ⋅ σ')"
      using 1 apply auto
      by (metis permute_subst_subst_compose subst_apply_term_ctxt_apply_distrib subst_subst term_apply_subst_Var_Rep_perm)
    finally show ?thesis .
  qed
  moreover
  have "snd (π2 ∙ r') ⋅ σ = π' ∙ (snd (π4 ∙ r') ⋅ σ')"
  proof -
    have "snd (π2 ∙ r') ⋅ σ = π ∙ snd (π4 ∙ r') ⋅ σ" by (simp add: 0 eqvt)
    also have "… = π' ∙ (snd (π4 ∙ r') ⋅ σ')"
      using 1 by (metis permute_subst_subst_compose subst_subst term_apply_subst_Var_Rep_perm)
    finally show ?thesis .
  qed
  ultimately show ?thesis
    by (metis ctxt_of_pos_term_subst p poss_perm_prod_simps(1) subst_apply_term_ctxt_apply_distrib)
qed

lemma CP2_Union_CP2':
  "CP2 R R' = ⋃(CP2' R R')"
proof
  show "⋃(CP2' R R') ⊆ CP2 R R'"
  proof
    fix s t
    assume "(s, t) ∈ ⋃(CP2' R R')"
    then obtain r p r' π1 π2 σ
      where "r ∈ R" and "r' ∈ R'" and p: "p ∈ funposs (fst (π2 ∙ r'))"
      and "mgu (π1 ∙ fst r) (π2 ∙ fst r' |_ p) = Some σ"
      and ol: "overlap R R' (π1 ∙ r) p (π2 ∙ r')"
      and s: "s = replace_at (fst (π2 ∙ r')) p (snd (π1 ∙ r)) ⋅ σ"
      and t: "t = snd (π2 ∙ r') ⋅ σ"
      by (auto simp: CP2'_def CP2_rules_pos_def eqvt)
    then have "σ = the_mgu (π1 ∙ fst r) (π2 ∙ fst r' |_ p)" by (simp add: the_mgu_def)
    with ol show "(s, t) ∈ CP2 R R'"
      using funposs_imp_poss [OF p]
      unfolding CP2_def s t by (force simp add: eqvt ctxt_of_pos_term_subst)
  qed
next
  show "CP2 R R' ⊆ ⋃(CP2' R R')"
  proof
    fix s t
    assume "(s, t) ∈ CP2 R R'"
    then obtain r p r' σ
      where ol: "overlap R R' r p r'"
      and "σ = the_mgu (fst r) (fst r' |_ p)"
      and s: "s = replace_at (fst r') p (snd r) ⋅ σ"
      and t: "t = snd r' ⋅ σ"
      by (auto simp: CP2_def)
    then have mgu: "mgu (fst r) (fst r' |_ p) = Some σ"
      unfolding overlap_def the_mgu_def
      using unify_complete and unify_sound by (force split: option.splits simp: is_imgu_def unifiers_def)
    from ol obtain π1 π2
      where 1 ∙ r ∈ R" (is "?r ∈ R")
      and 2 ∙ r' ∈ R'" (is "?r' ∈ R'")
      and p: "p ∈ funposs (fst r')" by (auto simp: overlap_def)
    moreover
    have "overlap R R' (-π1 ∙ ?r) p (-π2 ∙ ?r')" using ol by simp
    moreover
    have "s = (ctxt_of_pos_term p (fst (-π2 ∙ ?r')))⟨snd (-π1 ∙ ?r)⟩ ⋅ σ"
      and "t = snd (-π2 ∙ ?r') ⋅ σ"
      using funposs_imp_poss [OF p] by (simp_all add: s t ctxt_of_pos_term_subst)
    moreover
    have "mgu (fst (-π1 ∙ ?r)) (fst (-π2 ∙ ?r') |_ p) = Some σ" using mgu by simp
    moreover have "p ∈ funposs (fst ?r')" using p by (simp add: eqvt [symmetric])
    ultimately show "(s, t) ∈ ⋃(CP2' R R')"
      unfolding CP2'_def CP2_rules_pos_def by blast
  qed
qed

lemma CP2_rules_pos_perm:
  fixes R R' :: "('f, 'v :: infinite) trs"
  assumes "x ∈ CP2_rules_pos R R' r p r'"
    and "y ∈ CP2_rules_pos R R' r p r'"
  shows "∃π. π ∙ x = y"
proof -
  from assms [unfolded CP2_rules_pos_def] obtain π1 π2 π3 π4 and σ σ' :: "('f, 'v) subst"
  where mgu: "mgu (fst (π1 ∙ r)) (fst (π2 ∙ r') |_ p) = Some σ"
             "mgu (fst (π3 ∙ r)) (fst (π4 ∙ r') |_ p) = Some σ'"
    and ol: "overlap R R' (π1 ∙ r) p (π2 ∙ r')"
            "overlap R R' (π3 ∙ r) p (π4 ∙ r')"
    and x: "x = (replace_at (fst (π2 ∙ r')) p (snd (π1 ∙ r)) ⋅ σ, snd (π2 ∙ r') ⋅ σ)"
    and y: "y = (replace_at (fst (π4 ∙ r')) p (snd (π3 ∙ r)) ⋅ σ', snd (π4 ∙ r') ⋅ σ')"
    by blast
  show ?thesis
    using overlap_variants_imp_CP_variants [OF ol(2, 1) mgu(2, 1)]
    by (auto simp: x y eqvt)
qed

lemma CP2_rules_pos_join:
  assumes "x ∈ CP2_rules_pos R R' r p r'"
    and "y ∈ CP2_rules_pos R R' r p r'"
  shows "x ∈ (rstep S) ⟷ y ∈ (rstep S)"
  using CP2_rules_pos_perm [OF assms] by auto

abbreviation "CP' R ≡ CP2' R R"

text ‹If @{term R} and @{term R'} are finite, then @{term "CP2' R R'"} is finite
by @{thm finite_CP2'}. Thus it suffices to prove joinability of finitely many
critical pairs in order to conclude joinability of all critical pairs @{term "CP2 R R'"}.›
lemma CP2'_representatives_join_imp_CP2_join:
  assumes "∀C∈CP2' R R'. ∃(s, t)∈C. (s, t) ∈ (rstep S)"
  shows "∀(s, t)∈CP2 R R'. (s, t) ∈ (rstep S)"
  using assms
  by (auto simp: CP2'_def CP2_Union_CP2')
     (blast dest: CP2_rules_pos_join [of _ R R' _ _ _ _ S])

lemma CS3_ctxt:
  assumes "(t, p, s, u) ∈ CS3 A"
  shows "(C⟨t⟩, hole_pos C <#> p, C⟨s⟩, C⟨u⟩) ∈ CS3 A"
proof -
  from assms obtain D σ t' s' u' p'
    where "(t', p', s', u') ∈ A" and "t = D⟨t' ⋅ σ⟩" "s = D⟨s' ⋅ σ⟩" "u = D⟨u' ⋅ σ⟩"
    and "p = hole_pos D <#> p'"
    by (cases)
  with CS3.intros [OF this(1), of "C ∘c D" σ] show ?thesis by simp
qed

lemma overlap_imp_rstep:
  assumes "overlap R R' r p r'"
  shows "r ∈ rstep R" and "r' ∈ rstep R'"
  apply (insert assms)
  apply (case_tac [!] r, case_tac [!] r')
  apply (auto simp: overlap_def)
  by (metis perm_rstep_conv rstep.rule surj_pair)+

lemma overlap_imp_rstep_pos_Empty:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "overlap R R' r p r'"
  shows "r ∈ rstep_pos R ε" and "r' ∈ rstep_pos R' ε"
proof -
  from assms [unfolded overlap_def] obtain π1 π2 l1 r1 l2 r2 and σ :: "('f, 'v) subst"
    where p: "p ∈ poss l2"
      and [simp]: "r = (l1, r1)" "r' = (l2, r2)"
      and 1: "(l1, r1) ∈ -π1 ∙ R" and 2: "(l2, r2) ∈ -π2 ∙ R'"
      by (cases r, cases r') (fastforce dest: funposs_imp_poss)
  from rstep_pos.intros [OF 1, of ε l1 Var]
    show "r ∈ rstep_pos R ε" by simp
  from rstep_pos.intros [OF 2, of ε l2 Var]
    show "r' ∈ rstep_pos R' ε" by simp
qed

lemma overlap_source_eq:
  fixes R :: "('f, 'v :: infinite) trs" and r p r'
  defines "σ ≡ the_mgu (fst r) (fst r' |_ p)"
  assumes "overlap R R' r p r'"
  shows "p ∈ poss (fst r')" (is ?A)
    and "fst r' ⋅ σ = replace_at (fst r') p (fst r) ⋅ σ" (is ?B)
proof -
  from assms obtain τ :: "('f, 'v) subst"
    where p: "p ∈ poss (fst r')"
    and "fst r ⋅ τ = (fst r' |_ p) ⋅ τ"
    by (auto simp: overlap_def dest: funposs_imp_poss)
  from the_mgu [OF this(2)] and assms
    have "fst r ⋅ σ = (fst r' |_ p) ⋅ σ" by simp
  with p show ?B by (metis ctxt_supt_id subst_apply_term_ctxt_apply_distrib)
  show ?A by fact
qed

lemma overlap_rstep_pos_right:
  fixes R :: "('f, 'v :: infinite) trs" and r p r'
  defines "σ ≡ the_mgu (fst r) (fst r' |_ p)"
  assumes ol: "overlap R R' r p r'"
  shows "(fst r' ⋅ σ, snd r' ⋅ σ) ∈ rstep_pos R' ε"
  using overlap_imp_rstep_pos_Empty(2) [OF ol]
    and overlap_source_eq [OF ol, folded σ_def]
    and rstep_pos_subst [of "fst r'" "snd r'" R' ε σ]
    by simp

lemma overlap_rstep_pos_left:
  fixes R :: "('f, 'v :: infinite) trs" and r p r'
  defines "σ ≡ the_mgu (fst r) (fst r' |_ p)"
  assumes ol: "overlap R R' r p r'"
  shows "(fst r' ⋅ σ, (ctxt_of_pos_term p (fst r'))⟨snd r⟩ ⋅ σ) ∈ rstep_pos R p"
  using overlap_imp_rstep_pos_Empty(1) [OF ol]
    and overlap_source_eq [OF ol, folded σ_def]
    and rstep_pos_supt [of "fst r ⋅ σ" "snd r ⋅ σ"  R ε p "fst r' ⋅ σ"]
    apply (cases r, cases r')
    apply auto
    by (metis ctxt_of_pos_term_subst poss_imp_subst_poss rstep_pos_subst subt_at_ctxt_of_pos_term)

end