Theory Prime_Critical_Pairs

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014-2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Prime Critical Pairs›

theory Prime_Critical_Pairs
  imports
    CP
    Peak_Decreasingness
begin

  (*TODO: move*)
lemma relpow_2 [simp]: "r ^^ 2 = r O r"
  by (metis Suc_1 relpow_1 relpow_Suc)

no_notation
  subset_mset (infix "<#" 50)

text ‹A prime critical pair is a critical pair s.t. the non-root step is innermost.›
definition "PCP 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) ∧
    (∀u ⊲ fst r ⋅ σ. u ∈ NF (rstep R))}"

lemma PCP_subset_CP:
  "PCP R ⊆ CP R"
  by (force simp: PCP_def CP2_def)

text ‹A (non-empty) peak that is joinable or a prime critical pair.›
definition "nabla R s = {(t, u).
  (s, t) ∈ (rstep R)⇧+ ∧ (s, u) ∈ (rstep R)⇧+ ∧
  ((t, u) ∈ (rstep R)⇧↓ ∨ (t, u) ∈ (rstep (PCP R))⇧↔)}"

lemma nablaE:
  assumes "(t, u) ∈ nabla R s"
  obtains "(s, t) ∈ (rstep R)⇧+" and "(s, u) ∈ (rstep R)⇧+" and "(t, u) ∈ (rstep R)⇧↓"
  | "(s, t) ∈ (rstep R)⇧+" and "(s, u) ∈ (rstep R)⇧+" and "(t, u) ∈ (rstep (PCP R))⇧↔"
  using assms by (auto simp: nabla_def)

lemma nabla_joinI [intro]:
  assumes "(t, u) ∈ (rstep R)⇧↓"
    and "(s, t) ∈ (rstep R)⇧+" and "(s, u) ∈ (rstep R)⇧+"
  shows "(t, u) ∈ nabla R s"
  using assms by (auto simp: nabla_def)

lemma nabla_rstep_PCP_I [intro]:
  assumes "(t, u) ∈ (rstep (PCP R))⇧↔"
    and "(s, t) ∈ (rstep R)⇧+" and "(s, u) ∈ (rstep R)⇧+"
  shows "(t, u) ∈ nabla R s"
  using assms by (auto simp: nabla_def)

lemma nabla_refl_on_rstep_trancl:
  "(s, t) ∈ (rstep R)⇧+ ⟹ (t, t) ∈ nabla R s"
  by auto

lemma nabla_imp_nabla_refl:
  assumes "(t, u) ∈ nabla R s"
  shows "(u, u) ∈ nabla R s"
proof -
  have "(s, u) ∈ (rstep R)⇧+" using assms by (auto simp: nabla_def)
  from nabla_refl_on_rstep_trancl [OF this]
  show ?thesis .
qed

lemma nabla_ctxt:
  assumes "(t, u) ∈ nabla R s"
  shows "(C⟨t⟩, C⟨u⟩) ∈ nabla R (C⟨s⟩)"
  using assms by (auto simp: nabla_def dest: trancl_rstep_ctxt)

lemma nabla_subst:
  assumes "(t, u) ∈ nabla R s"
  shows "(t ⋅ σ, u ⋅ σ) ∈ nabla R (s ⋅ σ)"
  using assms by (auto simp: nabla_def dest: rsteps_subst_closed)

lemma nabla_sym:
  "(t, u) ∈ nabla R s ⟹ (u, t) ∈ nabla R s"
  by (auto simp: nabla_def)

lemma cpeaks_max_imp_PCP:
  assumes cpeaks: "(t, p, s, u) ∈ cpeaks R"
    and max: "∀v ⊲ s |_ p. v ∈ NF (rstep R)"
  shows "(t, u) ∈ PCP R"
proof -
  from cpeaks obtain l⇩1 r⇩1 l⇩2 r⇩2 σ
    where "t = replace_at l⇩2 p r⇩1 ⋅ σ"
      and s: "s = l⇩2 ⋅ σ" and "u = r⇩2 ⋅ σ"
      and σ: "σ = the_mgu l⇩1 (l⇩2 |_ p)"
      and ol: "overlap R R (l⇩1, r⇩1) p (l⇩2, r⇩2)"
    by (force simp: cpeaks2_def)
  moreover have "∀u ⊲ l⇩1 ⋅ σ. u ∈ NF (rstep R)"
  proof -
    have "p ∈ poss l⇩2" using overlap_source_eq [OF ol] by simp
    then have p: "p ∈ poss (l⇩2 ⋅ σ)" by (rule poss_imp_subst_poss)
    from overlap_source_eq [OF ol, simplified, folded σ]
    have "l⇩2 ⋅ σ = replace_at (l⇩2 ⋅ σ) p (l⇩1 ⋅ σ)"
      by (auto simp: ctxt_of_pos_term_subst [symmetric])
    then have "l⇩2 ⋅ σ |_ p = l⇩1 ⋅ σ" using replace_at_subt_at [OF p, of "l⇩1 ⋅ σ"] by simp
    with max show ?thesis by (simp add: s)
  qed
  ultimately show ?thesis by (force simp: PCP_def)
qed

lemma cpeaks_imp_poss:
  assumes "(t, p, s, u) ∈ cpeaks R"
  shows "p ∈ poss s"
  using assms
  apply (auto simp: cpeaks2_def)
  by (metis fst_conv overlap_source_eq(1) poss_imp_subst_poss)

lemma S3_cpeaks_max_imp_rstep_PCP:
  assumes "(t, p, s, u) ∈ S3 (cpeaks R)"
    and "∀v ⊲ s |_ p. v ∈ NF (rstep R)"
  shows "(t, u) ∈ rstep (PCP R)"
  using assms
  apply (cases)
  apply auto
  by (metis NF_instance cpeaks_imp_poss cpeaks_max_imp_PCP rstep.rule rstep.subst subt_at_subst supt_subst)

lemma cpeaks_imp_nabla2:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes vc: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and "(t, p, s, u) ∈ cpeaks R"
  shows "(t, u) ∈ nabla R s ^^ 2"
proof -
  from assms obtain l⇩1 r⇩1 p l⇩2 r⇩2 and σ :: "('f, 'v) subst"
    where ol: "overlap R R (l⇩1, r⇩1) p (l⇩2, r⇩2)"
      and σ: "σ = the_mgu l⇩1 (l⇩2 |_ p)"
      and s: "s = l⇩2 ⋅ σ" and t: "t = replace_at l⇩2 p r⇩1 ⋅ σ" and u: "u = r⇩2 ⋅ σ"
    by (auto simp: cpeaks2_def)
  from ol have *: "(l⇩1, r⇩1) ∈ rstep R" "(l⇩2, r⇩2) ∈ rstep R"
    and **: "l⇩2 ⋅ σ = replace_at l⇩2 p l⇩1 ⋅ σ"
    using overlap_source_eq [OF ol]
    by (auto dest: overlap_imp_rstep simp: σ)
  from ol have p: "p ∈ poss l⇩2" by (auto simp: overlap_def dest: funposs_imp_poss)
  with ** have sp: "s |_ p = l⇩1 ⋅ σ"
    by (auto simp: s) (metis hole_pos_ctxt_of_pos_term hole_pos_subst subt_at_hole_pos)
  have peak: "(s, t) ∈ (rstep R)" "(s, u) ∈ (rstep R)"
    using * by (auto simp: s t u) (auto simp: **)
  from overlap_rstep_pos_left [OF ol]
  have stp: "(s, t) ∈ rstep_pos R p" by (auto simp: s t σ)
  from overlap_rstep_pos_right [OF ol]
  have sue: "(s, u) ∈ rstep_pos R ε" by (auto simp: s u σ)
  show ?thesis
  proof (cases "∀w ⊲ s |_ p. w ∈ NF (rstep R)")
    txt ‹@{term "(t, s, u)"} is a critical peak (at position @{term p}).›
    case True
    with ol have "(t, u) ∈ PCP R" unfolding sp by (force simp: PCP_def s t u σ)
    with peak have "(t, u) ∈ nabla R s" by (auto)
    with nabla_imp_nabla_refl [OF this] show ?thesis by auto
  next
    case False
    then obtain w where w: "w ⊲ s |_ p" and "w ∉ NF (rstep R)" by blast
    then obtain v' where "(w, v') ∈ rstep R" by blast
    from rstep_imp_max_pos [OF this] obtain w' q'
      where "q' ∈ poss w" and q'_step: "(w, w') ∈ rstep_pos R q'"
        and max: "∀v ⊲ w |_ q'. v ∈ NF (rstep R)" by blast
    from supt_imp_subt_at_nepos [OF w] obtain p'
      where "p' ≠ ε" and "p' ∈ poss (s |_ p)" and "s |_ p |_ p' = w" by blast
    then have 0: "(p <#> p') ∈ poss s" and 1: "s |_ (p <#> p') = w" using p by (auto simp: s)
    define q where "q = p <#> p' <#> q'"
    define v where "v = (ctxt_of_pos_term (p <#> p') s)⟨w'⟩"
    from rstep_pos_supt [OF q'_step 0 1]
    have svq: "(s, v) ∈ rstep_pos R q" by (auto simp: q_def v_def)
    then have "(s, v) ∈ rstep R" by (auto simp: rstep_rstep_pos_conv)
    have "q > p" using ‹p' ≠ ε› by (simp add: q_def)
    from max have max: "∀v ⊲ s |_ q. v ∈ NF (rstep R)"
      using 0 and 1 by (auto simp: q_def ac_simps)

    from peak_imp_join_or_S3_cpeaks [OF vc svq sue]
    have svu: "(v, u) ∈ nabla R s"
    proof (cases "(v, q, s, u) ∈ S3 (cpeaks R)")
      case True
      from S3_cpeaks_max_imp_rstep_PCP [OF this max]
      show ?thesis using ‹(s, v) ∈ rstep R› and ‹(s, u) ∈ rstep R› by auto
    next
      case False
      with peak_imp_join_or_S3_cpeaks [OF vc svq sue]
      have "(v, u) ∈ (rstep R)⇧↓"
        using ‹p < q› by (insert Empty_least [of p], auto simp del: Empty_least)
      then show ?thesis using ‹(s, v) ∈ rstep R› and ‹(s, u) ∈ rstep R› by auto
    qed

    from peak_imp_join_or_S3_cpeaks [OF vc stp svq]
    show ?thesis
    proof
      assume "(t, v) ∈ (rstep R)⇧↓"
      then have *: "(t, v) ∈ nabla R s" using ‹(s, t) ∈ rstep R› and ‹(s, v) ∈ rstep R› by auto
      with svu show ?thesis by auto
    next
      assume "q ≤ p ∧
       (ctxt_of_pos_term q s)⟨t |_ q⟩ = t ∧
       (ctxt_of_pos_term q s)⟨v |_ q⟩ = v ∧
       (t |_ q, pos_diff p q, s |_ q, v |_ q) ∈ S3 (cpeaks R) ∨
       p ≤ q ∧
       (ctxt_of_pos_term p s)⟨t |_ p⟩ = t ∧
       (ctxt_of_pos_term p s)⟨v |_ p⟩ = v ∧
       (v |_ p, pos_diff q p, s |_ p, t |_ p) ∈ S3 (cpeaks R)"
      with ‹q > p› have t: "(ctxt_of_pos_term p s)⟨t |_ p⟩ = t"
        and v: "(ctxt_of_pos_term p s)⟨v |_ p⟩ = v"
        and *: "(v |_ p, pos_diff q p, s |_ p, t |_ p) ∈ S3 (cpeaks R)" by auto
      from S3_cpeaks_max_imp_rstep_PCP [OF *] and max
      have "(v |_ p,  t |_ p) ∈ rstep (PCP R)"
        using ‹p < q› and 0 using subt_at_pos_diff [OF ‹p < q›, of s] by simp
      then have "(t, v) ∈ (rstep (PCP R))⇧↔"
        apply (subst t [symmetric])
        apply (subst v [symmetric])
        by (metis Un_iff converse_iff rstep.ctxt)
      then have *: "(t, v) ∈ nabla R s" using ‹(s, t) ∈ rstep R› and ‹(s, v) ∈ rstep R› by auto
      with svu show ?thesis by auto
    qed
  qed
qed

lemma CS3_cpeaks_imp_nabla2:
  assumes vc: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and *: "(t, p, s, u) ∈ CS3 (cpeaks R)"
  shows "(t, u) ∈ nabla R s ^^ 2"
proof -
  from * obtain C t' s' p' u' σ where cp: "(t', p', s', u') ∈ cpeaks R"
    and t: "t = C⟨t' ⋅ σ⟩" and s: "s = C⟨s' ⋅ σ⟩" and u: "u = C⟨u' ⋅ σ⟩"
    and p: "p = hole_pos C <#> p'"
    by (cases)
  from cpeaks_imp_nabla2 [OF vc cp] obtain v
    where "(t', v) ∈ nabla R s'" and "(v, u') ∈ nabla R s'" by auto
  then have "(t, C⟨v ⋅ σ⟩) ∈ nabla R s" and "(C⟨v ⋅ σ⟩, u) ∈ nabla R s"
    unfolding s t u by (auto intro: nabla_subst nabla_ctxt)
  then show ?thesis by auto
qed

  (*Lemma 5.1.15*)
lemma peak_imp_nabla2:
  assumes vc: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and peak: "(s, t) ∈ rstep R" "(s, u) ∈ rstep R"
  shows "(t, u) ∈ nabla R s ^^ 2"
proof -
  { assume "(t, u) ∈ (rstep R)⇧↓"
    with peak have "(t, u) ∈ nabla R s" by (auto simp: nabla_def)
    with nabla_imp_nabla_refl [OF this] have ?thesis by auto }
  moreover
  { fix p assume "(t, p, s, u) ∈ CS3 (cpeaks R)"
    from CS3_cpeaks_imp_nabla2 [OF vc this] have ?thesis . }
  moreover
  { fix p assume "(u, p, s, t) ∈ CS3 (cpeaks R)"
    from CS3_cpeaks_imp_nabla2 [OF vc this] have ?thesis
      by (auto dest: nabla_sym) }
  ultimately show ?thesis
    using peak_imp_join_or_CS3_cpeaks [OF vc peak] by blast
qed

lemma PCP_join_nabla_imp_join:
  assumes "PCP R ⊆ (rstep R)⇧↓"
    and "(t, u) ∈ nabla R s"
  shows "(t, u) ∈ (rstep R)⇧↓"
  using assms
  apply (auto simp: nabla_def elim!: rstepE)
  apply blast
  done

lemma conversion_trans':
  "(x, y) ∈ A⇧↔⇧* ⟹ (y, z) ∈ A⇧↔⇧* ⟹ (x, z) ∈ A⇧↔⇧*"
  by (auto simp: conversion_def)

lemma SN_PCP_join_imp_CR:
  assumes vc: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and SN: "SN (rstep R)"
    and PCP_join: "PCP R ⊆ (rstep R)⇧↓"
  shows "CR (rstep R)"
proof -
  define less (infix "≻" 50) where "s ≻ t ⟷ (s, t) ∈ (rstep R)⇧+" for s t
  define lesseq (infix "≽" 50) where "s ≽ t ⟷ (s, t) ∈ (rstep R)⇧*" for s t
  define prestep where "prestep = source_step (rstep R)"
  have [simp]: "(⋃a. prestep a) = rstep R" by (auto simp: prestep_def)
  define in_prestep ("_ →⇩_ _" [50, 50] 51)
    where
      [simp]: "s →⇩a t ⟷ (s, t) ∈ prestep a" for s a t
  have prestep_iff [iff]: "⋀s t a. (s, t) ∈ prestep a ⟷ a = s ∧ (s, t) ∈ rstep R"
    by (auto simp: prestep_def)
  interpret lab: ars_labeled_sn prestep UNIV "op ≻"
    by (standard, insert SN) (auto simp: SN_trancl_SN_conv less_def)
  write lab.downset2 ("∨'(_,/ _')")
  interpret ars_peak_decreasing "prestep" UNIV "op ≻"
  proof
    fix a b s t u
    presume *: "s →⇩a t" "s →⇩b u"
    then have peak: "(s, t) ∈ rstep R" "(s, u) ∈ rstep R" by (auto)
    then have "s ≻ t" and "s ≻ u" by (auto simp: less_def)
    from * have "a ≽ s" and "b ≽ s" by (auto simp: lesseq_def)
    from peak_imp_nabla2 [OF vc peak] obtain v
      where "(t, v) ∈ nabla R s" and "(v, u) ∈ nabla R s" by auto
    with PCP_join have "(t, v) ∈ (rstep R)⇧↓" and "(v, u) ∈ (rstep R)⇧↓"
      by (auto dest: PCP_join_nabla_imp_join)
    then obtain x z
      where "(t, x) ∈ (rstep R)⇧*" and "(v, x) ∈ (rstep R)⇧*"
        and "(v, z) ∈ (rstep R)⇧*" and "(u, z) ∈ (rstep R)⇧*" by blast
    from ‹(t, v) ∈ nabla R s› have "(s, v) ∈ (rstep R)⇧+" by (auto simp: nabla_def)
    then have "s ≻ v" by (auto simp: less_def)
    { fix t u
      assume "(t, u) ∈ (rstep R)⇧*" and "s ≻ t"
      then have "(t, u) ∈ (⋃c∈∨(a, b). prestep c)⇧↔⇧*"
      proof (induct)
        case (step u v)
        then have "(u, v) ∈ prestep u" and "a ≻ u"
          using ‹a ≽ s› and ‹s ≻ t› by (auto simp: lesseq_def less_def)
        with step and ‹a ≽ s› show ?case
          by (auto simp: conversion_def iff del: prestep_iff)
            (metis (lifting, no_types) UN_I Un_iff mem_Collect_eq rtrancl.rtrancl_into_rtrancl)
      qed simp }
    note * = this
    from * [OF ‹(t, x) ∈ (rstep R)⇧*› ‹s ≻ t›]
      and * [OF ‹(v, x) ∈ (rstep R)⇧*› ‹s ≻ v›, THEN conversion_inv [THEN iffD1]]
      and * [OF ‹(v, z) ∈ (rstep R)⇧*› ‹s ≻ v›]
      and * [OF ‹(u, z) ∈ (rstep R)⇧*› ‹s ≻ u›, THEN conversion_inv [THEN iffD1]]
    show "(t, u) ∈ (⋃c∈∨(a, b). prestep c)⇧↔⇧*"
      by (blast dest: conversion_trans')
  qed auto
  show ?thesis using CR by simp
qed

lemma PCP_imp_peak:
  assumes "(t, u) ∈ PCP R"
  shows "∃s. (s, t) ∈ (rstep R)⇧* ∧ (s, u) ∈ (rstep R)⇧*"
  using assms
  apply (auto simp: PCP_def)
  by (metis fst_conv overlap_imp_rstep(1) overlap_imp_rstep(2) overlap_source_eq(2) r_into_rtrancl rstep.ctxt rstep.subst subst_apply_term_ctxt_apply_distrib)

lemma CR_imp_PCP_join:
  assumes "CR (rstep R)"
  shows "PCP R ⊆ (rstep R)⇧↓"
  using assms by (auto simp: CR_defs dest!: PCP_imp_peak)

    (*Corollary 5.1.16*)
lemma SN_imp_CR_iff_PCP_join:
  assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
    and "SN (rstep R)"
  shows "CR (rstep R) ⟷ PCP R ⊆ (rstep R)⇧↓"
  using SN_PCP_join_imp_CR [OF assms] and CR_imp_PCP_join [of R] by blast

definition
  "PCP_rules_pos 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') ∧
    (∀u ⊲ fst (π⇩1 ∙ r) ⋅ σ. u ∈ NF (rstep R))}"

lemma PCP_rules_pos_perm:
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "x ∈ PCP_rules_pos R r p r'"
    and "y ∈ PCP_rules_pos R r p r'"
  shows "∃π. π ∙ x = y"
proof -
  from assms [unfolded PCP_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 PCP_rules_pos_join:
  assumes "x ∈ PCP_rules_pos R r p r'"
    and "y ∈ PCP_rules_pos R r p r'"
  shows "x ∈ (rstep S)⇧↓ ⟷ y ∈ (rstep S)⇧↓"
  using PCP_rules_pos_perm [OF assms] by auto

text ‹Auxiliary definition to obtain the result that only finitely many PCPs have to be
considered.›
definition
  PCP' :: "('f, 'v::infinite) trs ⇒ ('f, 'v) rule set set"
  where
    "PCP' R = {PCP_rules_pos R r p r' | r p r'. r ∈ R ∧ r' ∈ R ∧ p ∈ poss (fst r')}"

lemma finite_PCP':
  assumes "finite R"
  shows "finite (PCP' R)"
proof -
  let ?R = "{(r, p, r'). r ∈ R ∧ r' ∈ R ∧ p ∈ poss (fst r')}"
  have *: "PCP' R = (λ(r, p, r'). PCP_rules_pos R r p r') ` ?R"
    by (force simp: PCP'_def)
  have "{(r, p, r'). r ∈ R ∧ r' ∈ R ∧ p ∈ poss (fst r')} ⊆ R × ⋃(poss ` lhss R) × R"
    by auto
  moreover have "finite (R × ⋃(poss ` lhss R) × R)"
    using assms and finite_poss by auto
  ultimately have "finite ?R" by (rule finite_subset)
  then show ?thesis unfolding * by (rule finite_imageI)
qed

lemma PCP_Union_PCP':
  "PCP R = ⋃(PCP' R)"
proof
  show "⋃(PCP' R) ⊆ PCP R"
  proof
    fix s t
    assume "(s, t) ∈ ⋃(PCP' R)"
    then obtain r p r' π⇩1 π⇩2 σ
      where "r ∈ R" and "r' ∈ R" and p: "p ∈ poss (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') ⋅ σ"
        and NF: "∀u ⊲ fst (π⇩1 ∙ r) ⋅ σ. u ∈ NF (rstep R)"
      by (auto simp: PCP'_def PCP_rules_pos_def eqvt)
    then have "σ = the_mgu (π⇩1 ∙ fst r) (π⇩2 ∙ fst r' |_ p)" by (simp add: the_mgu_def)
    with ol and NF show "(s, t) ∈ PCP R"
      using p
      unfolding PCP_def s t by (force simp add: eqvt ctxt_of_pos_term_subst)
  qed
next
  show "PCP R ⊆ ⋃(PCP' R)"
  proof
    fix s t
    assume "(s, t) ∈ PCP 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' ⋅ σ"
        and NF: "∀u ⊲ fst r ⋅ σ. u ∈ NF (rstep R)"
      by (auto simp: PCP_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 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 ∈ poss (fst ?r')" using funposs_imp_poss [OF p] by (simp add: eqvt [symmetric])
    moreover have "∀u ⊲ fst (-π⇩1 ∙ ?r) ⋅ σ. u ∈ NF (rstep R)" using NF by simp
    ultimately show "(s, t) ∈ ⋃(PCP' R)"
      unfolding PCP'_def PCP_rules_pos_def by blast
  qed
qed

text ‹If @{term R} is finite, then @{term "PCP' R"} is finite by @{thm finite_PCP'}.
Thus it suffices to prove joinability of finitely many prime critical pairs
in order to conclude joinability of all prime critical pairs @{term "PCP R"}.›
lemma PCP'_representatives_join_imp_PCP_join:
  assumes "∀C∈PCP' R. ∃(s, t)∈C. (s, t) ∈ (rstep S)⇧↓"
  shows "∀(s, t)∈PCP R. (s, t) ∈ (rstep S)⇧↓"
  using assms
  by (auto simp: PCP'_def PCP_Union_PCP')
    (blast dest: PCP_rules_pos_join [of _ R _ _ _ _ S])

lemma PCP_imp_peak':
  fixes R :: "('f, 'v :: infinite) trs"
  assumes "(s, t) ∈ PCP R"
  shows "(s, t) ∈ (rstep R)¯ O (rstep R)"
  using CP2_imp_peak [of s t R R] and assms and PCP_subset_CP [of R] by blast

lemma WCR_imp_PCP_join:
  assumes "(rstep R)¯ O (rstep R) ⊆ (rstep R)⇧↓"
    and "(s, t) ∈ PCP R"
  shows "(s, t) ∈ (rstep R)⇧↓"
  using PCP_imp_peak' [OF assms(2)] and assms(1) by blast

lemma PCP_rules_pos_fair:
  assumes "x ∈ PCP_rules_pos R r p r'"
    and "y ∈ PCP_rules_pos R r p r'"
  shows "x ∈ (⋃i≤n. (rstep (E i))⇧↔) ⟷ y ∈ (⋃i≤n. (rstep (E i))⇧↔)"
  using PCP_rules_pos_perm [OF assms] by auto

text ‹If @{term R} is finite, then @{term "PCP' R"} is finite by @{thm finite_PCP'}.
Thus it suffices to prove fairness of finitely many prime critical pairs in order to
conclude fairness of all prime critical pairs @{term "PCP R"}.›
lemma PCP'_representatives_fair_imp_PCP_fair:
  assumes "∀C∈PCP' R. ∃(s, t)∈C. (s, t) ∈ (⋃i≤n. (rstep (E i))⇧↔)"
  shows "∀(s, t)∈PCP R. (s, t) ∈ (⋃i≤n. (rstep (E i))⇧↔)"
proof (unfold PCP_Union_PCP', intro ballI2)
  fix s t
  assume "(s, t) ∈ ⋃PCP' R"
  then obtain C where "C ∈ PCP' R" and "(s, t) ∈ C" by auto
  from assms [THEN bspec, OF this(1)] obtain u v
    where "(u, v) ∈ C" and *: "(u, v) ∈ (⋃i≤n. (rstep (E i))⇧↔)" by auto
  from ‹(s, t) ∈ C› and ‹(u, v) ∈ C› and ‹C ∈ PCP' R› obtain r p r'
    where "(s, t) ∈ PCP_rules_pos R r p r'"
      and "(u, v) ∈ PCP_rules_pos R r p r'" by (auto simp: PCP'_def)
  from * [folded PCP_rules_pos_fair [OF this]]
  show "(s, t) ∈ (⋃i≤n. (rstep (E i))⇧↔)" .
qed

end