Theory Ground_Superposition_Completeness

theory Ground_Superposition_Completeness
  imports
    Ground_Superposition

    First_Order_Clause.HOL_Extra
    First_Order_Clause.Ground_Critical_Pairs

    Abstract_Rewriting_Extra
    Relation_Extra
begin

subsection ‹Model Construction›

(* TODO: Move *)
lemma singleton_eq_CollectD: "{x} = {y. P y} ⟹ P x"
  by blast

lemma subset_Union_mem_CollectI: "P x ⟹ f x ⊆ (⋃y ∈ {z. P z}. f y)"
  by blast

lemma from_neq_double_rtrancl_to_eqE:
  assumes "x ≠ y" and "(x, z) ∈ r*" and "(y, z) ∈ r*"
  obtains
    w where "(x, w) ∈ r" and "(w, z) ∈ r*" |
    w where "(y, w) ∈ r" and "(w, z) ∈ r*"
  using assms
  by (metis converse_rtranclE)

lemma ex_step_if_joinable:
  assumes "asymp R" "(x, z) ∈ r*" and "(y, z) ∈ r*"
  shows
    "R== z y ⟹ R y x ⟹ ∃w. (x, w) ∈ r ∧ (w, z) ∈ r*"
    "R== z x ⟹ R x y ⟹ ∃w. (y, w) ∈ r ∧ (w, z) ∈ r*"
  using assms
  by (metis asympD converse_rtranclE reflclp_iff)+

lemma (in ground_order) mem_join_union_iff_mem_join_lhs':
  assumes
    ball_R1_rhs_lt_lhs: "⋀t1 t2. (t1, t2) ∈ R1 ⟹ t2 ≺t t1" and
    ball_R2_lt_lhs: "⋀t1 t2. (t1, t2) ∈ R2 ⟹ s ≺t t1 ∧ t ≺t t1"
  shows "(s, t) ∈ (R1 ∪ R2)↓ ⟷ (s, t) ∈ R1↓"
proof -
  have ball_R1_rhs_lt_lhs': "(t1, t2) ∈ R1* ⟹ t2 ≼t t1" for t1 t2
  proof (induction t2 rule: rtrancl_induct)
    case base
    show ?case
      by order
  next
    case (step y z)
    thus ?case
      using ball_R1_rhs_lt_lhs
      by (metis reflclp_iff transpD term.order.transp)
  qed

  show ?thesis
  proof (rule mem_join_union_iff_mem_join_lhs)
    fix u assume "(s, u) ∈ R1*"
    hence "u ≼t s"
      using ball_R1_rhs_lt_lhs' by metis

    show "u ∉ Domain R2"
    proof (rule notI)
      assume "u ∈ Domain R2"
      then obtain u' where "(u, u') ∈ R2"
        by auto

      hence "s ≺t u"
        using ball_R2_lt_lhs
        by simp

      with ‹u ≼t s› show False
        by order
    qed
  next
    fix u assume "(t, u) ∈ R1*"
    hence "u ≼t t"
      using ball_R1_rhs_lt_lhs'
      by simp

    show "u ∉ Domain R2"
    proof (rule notI)
      assume "u ∈ Domain R2"
      then obtain u' where "(u, u') ∈ R2"
        by auto

      hence "t ≺t u"
        using ball_R2_lt_lhs
        by simp

      with ‹u ≼t t› show False
        by order
    qed
  qed
qed

lemma (in ground_order) mem_join_union_iff_mem_join_rhs':
  assumes
    ball_R1_rhs_lt_lhs: "⋀t1 t2. (t1, t2) ∈ R2 ⟹ t2 ≺t t1" and
    ball_R2_lt_lhs: "⋀t1 t2. (t1, t2) ∈ R1 ⟹ s ≺t t1 ∧ t ≺t t1"
  shows "(s, t) ∈ (R1 ∪ R2)↓ ⟷ (s, t) ∈ R2↓"
  using assms mem_join_union_iff_mem_join_lhs'
  by (metis (no_types, opaque_lifting) sup_commute)

lemma (in ground_order) mem_join_union_iff_mem_join_lhs'':
  assumes
    Range_R1_lt_Domain_R2: "⋀t1 t2. t1 ∈ Range R1 ⟹ t2 ∈ Domain R2 ⟹ t1 ≺t t2" and
    s_lt_Domain_R2: "⋀t2. t2 ∈ Domain R2 ⟹ s ≺t t2" and
    t_lt_Domain_R2: "⋀t2. t2 ∈ Domain R2 ⟹ t ≺t t2"
  shows "(s, t) ∈ (R1 ∪ R2)↓ ⟷ (s, t) ∈ R1↓"
proof (rule mem_join_union_iff_mem_join_lhs)
  fix u assume "(s, u) ∈ R1*"
  hence "u = s ∨ u ∈ Range R1"
    by (meson Range.intros rtrancl.cases)

  thus "u ∉ Domain R2"
    using Range_R1_lt_Domain_R2 s_lt_Domain_R2
    by (metis irreflpD term.order.irreflp_on_less)
next
  fix u assume "(t, u) ∈ R1*"
  hence "u = t ∨ u ∈ Range R1"
    by (meson Range.intros rtrancl.cases)

  thus "u ∉ Domain R2"
    using Range_R1_lt_Domain_R2 t_lt_Domain_R2
    by (metis irreflpD term.order.irreflp_on_less)
qed

context ground_superposition_calculus begin

function epsilon :: "'t clause set ⇒ 't clause ⇒ 't rel" where
  "epsilon N C = {(s, t)| s t C'.
    C ∈ N ∧
    C = add_mset (Pos (Upair s t)) C' ∧
    select C = {#} ∧
    is_strictly_maximal (Pos (Upair s t)) C ∧
    t ≺t s ∧
    (let RC = (⋃D ∈ {D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c D} D) in
    ¬ upair ` (rewrite_in_context RC)↓ ⊫ C ∧
    ¬ upair ` (rewrite_in_context (insert (s, t) RC))↓ ⊫ C' ∧
    s ∈ NF (rewrite_in_context RC))}"
  by auto

termination epsilon
proof (relation "{((_, C), (_, C')). C ≺c C'}")

  have "wfp (λ(_, C) (_, C'). C ≺c C')"
    by (rule wfp_if_convertible_to_wfp[OF wfp_less, of _ snd]) auto

  thus "wf {((_, C), (_, C')). C ≺c C'}"
    by (simp add: wfp_def)
qed simp

declare epsilon.simps[simp del]

lemma epsilon_filter_le_conv: "epsilon {D ∈ N. D ≼c C} C = epsilon N C"
proof (intro subset_antisym subrelI)
  fix x y
  assume "(x, y) ∈ epsilon {D ∈ N. D ≼c C} C"
  then obtain C' where
    "C ∈ N" and
    "C = add_mset (x ≈ y) C'" and
    "select C = {#}" and
    "is_strictly_maximal (x ≈ y) C" and
    "y ≺t x" and
    "(let RC = ⋃x∈{D ∈ N. (D ≺c C ∨ D = C) ∧ D ≺c C}. epsilon {E ∈ N. (E ≺c C ∨ E = C) ∧ E ≼c x} x in
      ¬ upair ` (rewrite_in_context RC)↓ ⊫ C ∧
      ¬ upair ` (rewrite_in_context (insert (x, y) RC))↓ ⊫ C' ∧
      x ∈ NF (rewrite_in_context RC))"
    unfolding epsilon.simps[of _ C] mem_Collect_eq
    by auto

  moreover have "(⋃x∈{D ∈ N. (D ≺c C ∨ D = C) ∧ D ≺c C}. epsilon {E ∈ N. (E ≺c C ∨ E = C) ∧ E ≼c x} x) = (⋃D∈{D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c D} D)"
  proof (rule SUP_cong)
    show "{D ∈ N. (D ≺c C ∨ D = C) ∧ D ≺c C} = {D ∈ N. D ≺c C}"
      by metis
  next
    show "⋀x. x ∈ {D ∈ N. D ≺c C} ⟹ epsilon {E ∈ N. (E ≺c C ∨ E = C) ∧ E ≼c x} x = epsilon {E ∈ N. E ≼c x} x"
      by (metis (no_types, lifting) clause.order.dual_order.strict_trans2 mem_Collect_eq)
  qed

  ultimately show "(x, y) ∈ epsilon N C"
    unfolding epsilon.simps[of _ C] by simp
next
  fix x y
  assume "(x, y) ∈ epsilon N C"
  then obtain C' where
    "C ∈ N" and
    "C = add_mset (x ≈ y) C'" and
    "select C = {#}" and
    "is_strictly_maximal (x ≈ y) C" and
    "y ≺t x" and
    "(let RC = ⋃x∈{D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c x} x in
      ¬ upair ` (rewrite_in_context RC)↓ ⊫ C ∧
      ¬ upair ` (rewrite_in_context (insert (x, y) RC))↓ ⊫ C' ∧
      x ∈ NF (rewrite_in_context RC))"
    unfolding epsilon.simps[of _ C] mem_Collect_eq
    by auto

  moreover have "(⋃x∈{D ∈ N. (D ≺c C ∨ D = C) ∧ D ≺c C}. epsilon {E ∈ N. (E ≺c C ∨ E = C) ∧ E ≼c x} x) = (⋃D∈{D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c D} D)"
  proof (rule SUP_cong)
    show "{D ∈ N. (D ≺c C ∨ D = C) ∧ D ≺c C} = {D ∈ N. D ≺c C}"
      by metis
  next
    show "⋀x. x ∈ {D ∈ N. D ≺c C} ⟹ epsilon {E ∈ N. (E ≺c C ∨ E = C) ∧ E ≼c x} x = epsilon {E ∈ N. E ≼c x} x"
      by (metis (mono_tags, lifting) clause.order.dual_order.strict_trans2
          mem_Collect_eq)
  qed

  ultimately show "(x, y) ∈ epsilon {D ∈ N. (≺c)== D C} C"
    unfolding epsilon.simps[of _ C] by simp
qed

lemma epsilon_eq_empty_or_singleton:
  "epsilon N C = {} ∨ (∃s t. epsilon N C = {(s, t)})"
proof -
  have "∃≤1 (x, y). ∃C'.
    C = add_mset (x ≈ y) C' ∧ is_strictly_maximal (x ≈ y) C ∧ y ≺t x"
    by (rule Uniq_prodI)
       (metis (mono_tags, lifting) Upair_inject
        add_mset_remove_trivial insert_noteq_member
        is_strictly_maximal_def literal.order.nle_le literal.simps(1)
        term.order.dual_order.strict_implies_not_eq
        term.order.dual_order.strict_trans)

  hence Uniq_epsilon: "∃≤1 (x, y). ∃C'.
    C ∈ N ∧
    C = add_mset (x ≈ y) C' ∧ select C = {#} ∧
    is_strictly_maximal  (x ≈ y) C ∧ y ≺t x ∧
    (let RC = ⋃D ∈ {D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c D} D in
      ¬ upair ` (rewrite_in_context RC)↓ ⊫ C ∧
      ¬ upair ` (rewrite_in_context (insert (x, y) RC))↓ ⊫ C' ∧
      x ∈ NF (rewrite_in_context RC))"
    using Uniq_antimono'
    by (smt (verit) Uniq_def Uniq_prodI case_prod_conv)

  show ?thesis
    unfolding epsilon.simps[of N C]
    using Collect_eq_if_Uniq_prod[OF Uniq_epsilon]
    by (smt (verit, best) Collect_cong Collect_empty_eq Uniq_def Uniq_epsilon case_prod_conv
        insertCI mem_Collect_eq)
qed

lemma card_epsilon_le_one:
  "card (epsilon N C) ≤ 1"
  using epsilon_eq_empty_or_singleton[of N C]
  by auto

definition rewrite_sys where
  "rewrite_sys N C ≡ (⋃D ∈ {D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c D} D)"

definition rewrite_sys' where
  "rewrite_sys' N ≡ (⋃C ∈ N. epsilon N C)"

lemma rewrite_sys_alt: "rewrite_sys' {D ∈ N. D ≺c C} = rewrite_sys N C"
  unfolding rewrite_sys'_def rewrite_sys_def
proof (rule SUP_cong)
  show "{D ∈ N. D ≺c C} = {D ∈ N. D ≺c C}" ..
next
  show "⋀x. x ∈ {D ∈ N. D ≺c C} ⟹ epsilon {D ∈ N. D ≺c C} x = epsilon {E ∈ N. (≺c)== E x} x"
    using epsilon_filter_le_conv
    by (smt (verit, best) Collect_cong clause.order.le_less_trans mem_Collect_eq)
qed

lemma mem_epsilonE:
  assumes rule_in: "rule ∈ epsilon N C"
  obtains l r C' where
    "C ∈ N" and
    "rule = (l, r)" and
    "C = add_mset (Pos (Upair l r)) C'" and
    "select C = {#}" and
    "is_strictly_maximal (Pos (Upair l r)) C" and
    "r ≺t l" and
    "¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C" and
    "¬ upair ` (rewrite_in_context (insert (l, r) (rewrite_sys N C)))↓ ⊫ C'" and
    "l ∈ NF (rewrite_in_context (rewrite_sys N C))"
  using rule_in
  unfolding epsilon.simps[of N C] mem_Collect_eq Let_def rewrite_sys_def
  by (metis (no_types, lifting))

lemma mem_epsilon_iff:
  "(l, r) ∈ epsilon N C ⟷
    (∃C'. C ∈ N ∧ C = add_mset (Pos (Upair l r)) C' ∧ select C = {#} ∧
      is_strictly_maximal (Pos (Upair l r)) C ∧ r ≺t l ∧
      ¬ upair ` (rewrite_in_context (rewrite_sys' {D ∈ N. D ≺c C}))↓ ⊫ C ∧
      ¬ upair ` (rewrite_in_context (insert (l, r) (rewrite_sys' {D ∈ N. D ≺c C})))↓ ⊫ C' ∧
      l ∈ NF (rewrite_in_context (rewrite_sys' {D ∈ N. D ≺c C})))"
  (is "?LHS ⟷ ?RHS")
proof (rule iffI)
  assume ?LHS
  thus ?RHS
    using rewrite_sys_alt
    by (auto elim: mem_epsilonE)
next
  assume ?RHS
  thus ?LHS
    unfolding epsilon.simps[of N C] mem_Collect_eq
    unfolding rewrite_sys_alt rewrite_sys_def by auto
qed

lemma rhs_lt_lhs_if_mem_rewrite_sys:
  assumes "(t1, t2) ∈ rewrite_sys N C"
  shows "t2 ≺t t1"
  using assms
  unfolding rewrite_sys_def
  by (smt (verit, best) UN_iff mem_epsilonE prod.inject)

lemma rhs_less_trm_lhs_if_mem_rewrite_inside_gctxt_rewrite_sys:
  assumes rule_in: "(t1, t2) ∈ rewrite_in_context (rewrite_sys N C)"
  shows "t2 ≺t t1"
proof -
  from rule_in obtain c t1' t2' where
    "(t1, t2) = (c⟨t1'⟩, c⟨t2'⟩) ∧ (t1', t2') ∈ rewrite_sys N C"
    unfolding rewrite_in_context_def mem_Collect_eq
    by auto

  thus ?thesis
  using rhs_lt_lhs_if_mem_rewrite_sys[of t1' t2']
  by (metis Pair_inject term.order.context_compatibility)
qed

lemma rhs_lesseq_trm_lhs_if_mem_rtrancl_rewrite_inside_gctxt_rewrite_sys:
  assumes rule_in: "(t1, t2) ∈ (rewrite_in_context (rewrite_sys N C))*"
  shows "t2 ≼t t1"
  using rule_in
proof (induction t2 rule: rtrancl_induct)
  case base
  show ?case
    by order
next
  case (step t2 t3)
  from step.hyps have "t3 ≺t t2"
    using rhs_less_trm_lhs_if_mem_rewrite_inside_gctxt_rewrite_sys
    by metis
  with step.IH show ?case
    by order
qed

lemma rewrite_sys_subset_if_less_cls:
  "C ≺c D ⟹ rewrite_sys N C ⊆ rewrite_sys N D"
  unfolding rewrite_sys_def
  unfolding epsilon_filter_le_conv
  by (smt (verit, del_insts) SUP_mono clause.order.dual_order.strict_trans mem_Collect_eq subset_eq)

lemma mem_rewrite_sys_if_less_cls:
  assumes "D ∈ N" and "D ≺c C" and "(u, v) ∈ epsilon N D"
  shows "(u, v) ∈ rewrite_sys N C"
  unfolding rewrite_sys_def UN_iff
proof (intro bexI)
  show "D ∈ {D ∈ N. D ≺c C}"
    using ‹D ∈ N› ‹D ≺c C› by simp
next
  show "(u, v) ∈ epsilon {E ∈ N. E ≼c D} D"
    using ‹(u, v) ∈ epsilon N D› epsilon_filter_le_conv by simp
qed

lemma less_trm_iff_less_cls_if_lhs_epsilon:
  assumes EC: "epsilon N C = {(s, t)}" and ED: "epsilon N D = {(u, v)}"
  shows "u ≺t s ⟷ D ≺c C"
proof -
  from EC have "(s, t) ∈ epsilon N C"
    by simp
  then obtain C' where
    "C ∈ N" and
    C_def: "C = add_mset (Pos (Upair s t)) C'" and
    "is_strictly_maximal (Pos (Upair s t)) C" and
    "t ≺t s" and
    s_irreducible: "s ∈ NF (rewrite_in_context (rewrite_sys N C))"
    by (auto elim!: mem_epsilonE)
  hence "∀L ∈# C'. L ≺l Pos (Upair s t)"
    unfolding is_strictly_maximal_def
    by auto

  from ED obtain D' where
    "D ∈ N" and
    D_def: "D = add_mset (u ≈ v) D'" and
    "is_strictly_maximal (u ≈ v) D" and
    "v ≺t u"
    by (auto simp:  elim: epsilon.elims dest: singleton_eq_CollectD)
  hence "∀L ∈# D'. L ≺l Pos (Upair u v)"
    by (auto simp: is_strictly_maximal_def)

  show ?thesis
  proof (rule iffI)
    assume "u ≺t s"

    moreover hence "v ≺t s"
      using ‹v ≺t u›
      by order

    ultimately have "multp (≺t) {#u, v#} {#s, t#}"
      using one_step_implies_multp[of "{#s, t#}" "{#u, v#}" _ "{#}"]
      by simp

    hence "u ≈ v ≺l s ≈ t"
      by (simp add: lessl_def)

    moreover hence "∀L ∈# D'. L ≺l s ≈ t"
      using ‹∀L ∈# D'. L ≺l u ≈ v›
      by fastforce

    ultimately show "D ≺c C"
      using one_step_implies_multp[of C D _ "{#}"] lessc_def
      by (simp add: D_def C_def)
  next
    assume "D ≺c C"

    have "(u, v) ∈ rewrite_sys N C"
      using ED ‹D ∈ N› ‹D ≺c C› mem_rewrite_sys_if_less_cls
      by auto

    hence "(u, v) ∈ rewrite_in_context (rewrite_sys N C)"
      by blast

    hence "s ≠ u"
      using s_irreducible
      by auto

    moreover have "¬ (s ≺t u)"
    proof (rule notI)
      assume "s ≺t u"

      moreover hence "t ≺t u"
        using ‹t ≺t s›
        by order

      ultimately have "multp (≺t) {#s, t#} {#u, v#}"
        using one_step_implies_multp[of "{#u, v#}" "{#s, t#}" _ "{#}"]
        by simp

      hence "Pos (Upair s t) ≺l Pos (Upair u v)"
        by (simp add: lessl_def)

      moreover hence "∀L ∈# C'. L ≺l Pos (Upair u v)"
        using ‹∀L ∈# C'. L ≺l Pos (Upair s t)›
        by fastforce

      ultimately have "C ≺c D"
        using one_step_implies_multp[of D C _ "{#}"] lessc_def
        by (simp add: D_def C_def)

      thus False
        using ‹D ≺c C›
        by order
    qed
    ultimately show "u ≺t s"
      by order
  qed
qed

lemma termination_rewrite_sys: "wf ((rewrite_sys N C)¯)"
proof (rule wf_if_convertible_to_wf)
  show "wf {(x, y). x ≺t y}"
    using term.order.wfp
    by (simp add: wfp_def)
next
  fix t s
  assume "(t, s) ∈ (rewrite_sys N C)¯"
  hence "(s, t) ∈ rewrite_sys N C"
    by simp
  then obtain D where "D ≺c C" and "(s, t) ∈ epsilon N D"
    unfolding rewrite_sys_def using epsilon_filter_le_conv by blast
  hence "t ≺t s"
    by (auto elim: mem_epsilonE)
  thus "(t, s) ∈ {(x, y). x ≺t y}"
    by (simp add: )
qed

lemma termination_Union_rewrite_sys: "wf ((⋃D ∈ N. rewrite_sys N D)¯)"
proof (rule wf_if_convertible_to_wf)
  show "wf {(x, y). x ≺t y}"
    using term.order.wfp
    by (simp add: wfp_def)
next
  fix t s
  assume "(t, s) ∈ (⋃D ∈ N. rewrite_sys N D)¯"

  hence "(s, t) ∈ (⋃D ∈ N. rewrite_sys N D)"
    by simp

  then obtain C where "C ∈ N" "(s, t) ∈ rewrite_sys N C"
    by auto

  then obtain D where "D ≺c C" and "(s, t) ∈ epsilon N D"
    unfolding rewrite_sys_def using epsilon_filter_le_conv
    by blast

  hence "t ≺t s"
    by (auto elim: mem_epsilonE)

  thus "(t, s) ∈ {(x, y). x ≺t y}"
    by simp
qed

lemma no_crit_pairs: "{(t1, t2) ∈ ground_critical_pairs (⋃ (epsilon N2 ` N)). t1 ≠ t2} = {}"
proof (rule ccontr)
  assume "{(t1, t2).
    (t1, t2) ∈ ground_critical_pairs (⋃ (epsilon N2 ` N)) ∧ t1 ≠ t2} ≠ {}"
  then obtain c l r1 r2 where
    "(c⟨r2⟩, r1) ∈ ground_critical_pairs (⋃ (epsilon N2 ` N))" and
    "c⟨r2⟩ ≠ r1" and
    rule1_in: "(c⟨l⟩, r1) ∈ ⋃ (epsilon N2 ` N)" and
    rule2_in: "(l, r2) ∈ ⋃ (epsilon N2 ` N)"
    unfolding ground_critical_pairs_def mem_Collect_eq by blast

  from rule1_in rule2_in obtain C1 C2 where
    "C1 ∈ N" and rule1_in': "(c⟨l⟩, r1) ∈ epsilon N2 C1" and
    "C2 ∈ N" and rule2_in': "(l, r2) ∈ epsilon N2 C2"
    by auto

  from rule1_in' obtain C1' where
    C1_def: "C1 = add_mset (Pos (Upair c⟨l⟩ r1)) C1'" and
    C1_max: "is_strictly_maximal (Pos (Upair c⟨l⟩ r1)) C1" and
    "r1 ≺t c⟨l⟩" and
    l1_irreducible: "c⟨l⟩ ∈ NF (rewrite_in_context (rewrite_sys N2 C1))"
    by (auto elim: mem_epsilonE)

  from rule2_in' obtain C2' where
    C2_def: "C2 = add_mset (Pos (Upair l r2)) C2'" and
    C2_max: "is_strictly_maximal (Pos (Upair l r2)) C2" and
    "r2 ≺t l"
    by (auto elim: mem_epsilonE)

  have "epsilon N2 C1 = {(c⟨l⟩, r1)}"
    using rule1_in' epsilon_eq_empty_or_singleton
    by (metis empty_iff singletonD)

  have "epsilon N2 C2 = {(l, r2)}"
    using rule2_in' epsilon_eq_empty_or_singleton 
    by (metis empty_iff singletonD)

  show False
  proof (cases "c = □")
    case True
    hence "¬ (c⟨l⟩ ≺t l)" and "¬ (l ≺t c⟨l⟩)"
      by (simp_all add: irreflpD)

    hence "¬ (C1 ≺c C2)" and "¬ (C2 ≺c C1)"
      using ‹epsilon N2 C1 = {(c⟨l⟩, r1)}› ‹epsilon N2 C2 = {(l, r2)}›
        less_trm_iff_less_cls_if_lhs_epsilon
      by simp_all

    hence "C1 = C2"
      by order

    hence "r1 = r2"
      using ‹epsilon N2 C1 = {(c⟨l⟩, r1)}› ‹epsilon N2 C2 = {(l, r2)}›
      by simp

    moreover have "r1 ≠ r2"
      using ‹c⟨r2⟩ ≠ r1›
      unfolding ‹c = □›
      by simp

    ultimately show ?thesis
      by contradiction
  next
    case False
    hence "l ≺t c⟨l⟩"
      by (metis term.order.subterm_property)

    hence "C2 ≺c C1"
      using ‹epsilon N2 C1 = {(c⟨l⟩, r1)}› ‹epsilon N2 C2 = {(l, r2)}›
        less_trm_iff_less_cls_if_lhs_epsilon
      by simp

    then have "(l, r2) ∈ rewrite_sys N2 C1"
      by (metis (no_types, lifting) mem_epsilon_iff mem_rewrite_sys_if_less_cls rule2_in')

    hence "(c⟨l⟩, c⟨r2⟩) ∈ rewrite_in_context (rewrite_sys N2 C1)"
      by auto

    thus False
      using l1_irreducible
      by auto
  qed
qed

sublocale ground_critical_pairs
  by unfold_locales

lemma WCR_Union_rewrite_sys: "WCR (rewrite_in_context (⋃D ∈ N. epsilon N2 D))"
  unfolding ground_critical_pair_theorem
proof (intro subsetI ballI)
  fix tuple
  assume tuple_in: "tuple ∈ ground_critical_pairs (⋃ (epsilon N2 ` N))"

  obtain t1 t2 where tuple_def: "tuple = (t1, t2)"
    by fastforce

  moreover have "(t1, t2) ∈ (rewrite_in_context (⋃ (epsilon N2 ` N)))↓" if "t1 = t2"
    using that
    by auto

  moreover have False if "t1 ≠ t2"
    using that tuple_def tuple_in no_crit_pairs 
    by simp

  ultimately show "tuple ∈ (rewrite_in_context (⋃ (epsilon N2 ` N)))↓"
    by (cases "t1 = t2") simp_all
qed

lemma
  assumes
    "D ≼c C" and
    EC_eq: "epsilon N C = {(s, t)}" and
    L_in: "L ∈# D" and
    topmost_trms_of_L: "mset_uprod (atm_of L) = {#u, v#}"
  shows
    lesseq_trm_if_pos: "is_pos L ⟹ u ≼t s" and
    less_trm_if_neg: "is_neg L ⟹ u ≺t s"
proof -
  from EC_eq have "(s, t) ∈ epsilon N C"
    by simp
  then obtain C' where
    C_def: "C = add_mset (Pos (Upair s t)) C'" and
    C_max_lit: "is_strictly_maximal (Pos (Upair s t)) C" and
    "t ≺t s"
    by (auto elim: mem_epsilonE)

  have "Pos (Upair s t) ≺l L" if "is_pos L" and "¬ u ≼t s"
  proof -
    from that(2) have "s ≺t u"
      by order

    hence "multp (≺t) {#s, t#} {#u, v#}"
      using ‹t ≺t s›
      by (smt (verit, del_insts) add.right_neutral empty_iff insert_iff one_step_implies_multp
          set_mset_add_mset_insert set_mset_empty transpD term.order.transp
          union_mset_add_mset_right)

    with that(1) show "s ≈ t ≺l L"
      using topmost_trms_of_L
      by (cases L) (simp_all add: lessl_def)
  qed

  moreover have "s ≈ t ≺l L" if "is_neg L" and "¬ u ≺t s"
  proof -
    from that(2) have "s ≼t u"
      by order

    have "multp (≺t) {#s, t#} {#u, v, u, v#}"
    proof(cases "s ≺t u")
      case True

      then show ?thesis
        using
          ‹t ≺t s› 
          multp_add_mset[OF term.order.asymp term.order.transp]
          multp_singleton_left[OF term.order.transp]
        by force
    next
      case False
      then have "s = u"
        using ‹s ≼t u›
        by order

      then show ?thesis
        using ‹t ≺t s›
        by auto
    qed

    with that(1) show "s ≈ t ≺l L"
      using topmost_trms_of_L
      by (cases L) (simp_all add: lessl_def)
  qed

  moreover have False if "s ≈ t ≺l L"
  proof -
    have "C ≺c D"
      unfolding lessc_def
    proof (rule multp_if_maximal_of_lhs_is_less)
      show "s ≈ t ∈# C"
        by (simp add: C_def)
    next
      show "L ∈# D"
        using L_in
        by simp
    next
      show "is_maximal (s ≈ t) C"
        using is_maximal_if_is_strictly_maximal[OF C_max_lit].
    next
      show "s ≈ t ≺l L"
        using that .
    qed simp_all

    with ‹D ≼c C› show False
      by order
  qed

  ultimately show "is_pos L ⟹ u ≼t s" and "is_neg L ⟹ u ≺t s"
    by argo+
qed

lemma less_trm_const_lhs_if_mem_rewrite_inside_gctxt:
  fixes t t1 t2 r
  assumes
    rule_in: "(t1, t2) ∈ rewrite_in_context r" and
    ball_lt_lhs: "⋀t1 t2. (t1, t2) ∈ r ⟹ t ≺t t1"
  shows "t ≺t t1"
proof -
  from rule_in obtain c t1' t2' where
    rule_in': "(t1', t2') ∈ r" and
    l_def: "t1 = c⟨t1'⟩" and
    r_def: "t2 = c⟨t2'⟩"
    unfolding rewrite_in_context_def by fast

  show ?thesis
    using ball_lt_lhs[OF rule_in'] term.order.less_eq_subterm_property[of t1' c] l_def
    by order
qed

lemma split_Union_epsilon:
  assumes D_in: "D ∈ N"
  shows "(⋃C ∈ N. epsilon N C) =
    rewrite_sys N D ∪ epsilon N D ∪ (⋃C ∈ {C ∈ N. D ≺c C}. epsilon N C)"
proof -
  have "N = {C ∈ N. C ≺c D} ∪ {D} ∪ {C ∈ N. D ≺c C}"
  proof (rule partition_set_around_element)
    show "totalp_on N (≺c)"
      using clause.order.totalp_on_less .
  next
    show "D ∈ N"
      using D_in
      by simp
  qed
  hence "(⋃C ∈ N. epsilon N C) =
      (⋃C ∈ {C ∈ N. C ≺c D}. epsilon N C) ∪ epsilon N D ∪ (⋃C ∈ {C ∈ N. D ≺c C}. epsilon N C)"
    by auto

  thus "(⋃C ∈ N. epsilon N C) =
    rewrite_sys N D ∪ epsilon N D ∪ (⋃C ∈ {C ∈ N. D ≺c C}. epsilon N C)"
    using epsilon_filter_le_conv rewrite_sys_def
    by simp
qed

lemma split_Union_epsilon':
  assumes D_in: "D ∈ N"
  shows "(⋃C ∈ N. epsilon N C) = rewrite_sys N D ∪ (⋃C ∈ {C ∈ N. D ≼c C}. epsilon N C)"
  using split_Union_epsilon[OF D_in] D_in
  by auto

lemma split_rewrite_sys:
  assumes "C ∈ N" and D_in: "D ∈ N" and "D ≺c C"
  shows "rewrite_sys N C = rewrite_sys N D ∪ (⋃C' ∈ {C' ∈ N. D ≼c C' ∧ C' ≺c C}. epsilon N C')"
proof -
  have "{D ∈ N. D ≺c C} =
        {y ∈ {D ∈ N. D ≺c C}. y ≺c D} ∪ {D} ∪ {y ∈ {D ∈ N. D ≺c C}. D ≺c y}"
  proof (rule partition_set_around_element)
    show "totalp_on {D ∈ N. D ≺c C} (≺c)"
      using clause.order.totalp_on_less .
  next
    from D_in ‹D ≺c C› show "D ∈ {D ∈ N. D ≺c C}"
      by simp
  qed

  also have "… = {x ∈ N. x ≺c C ∧ x ≺c D} ∪ {D} ∪ {x ∈ N. D ≺c x ∧ x ≺c C}"
    by auto

  also have "… = {x ∈ N. x ≺c D} ∪ {D} ∪ {x ∈ N. D ≺c x ∧ x ≺c C}"
    using ‹D ≺c C› clause.order.less_trans
    by blast

  finally have Collect_N_lt_C: "{x ∈ N. x ≺c C} = {x ∈ N. x ≺c D} ∪ {x ∈ N. D ≼c x ∧ x ≺c C}"
    by auto

  have "rewrite_sys N C = (⋃C' ∈ {D ∈ N. D ≺c C}. epsilon N C')"
    using epsilon_filter_le_conv
    by (simp add: rewrite_sys_def)

  also have "… = (⋃C' ∈ {x ∈ N. x ≺c D}. epsilon N C') ∪ (⋃C' ∈ {x ∈ N. D ≼c x ∧ x ≺c C}. epsilon N C')"
    unfolding Collect_N_lt_C
    by simp

  finally show "rewrite_sys N C = rewrite_sys N D ∪ ⋃ (epsilon N ` {C' ∈ N. D ≼c C' ∧ C' ≺c C})"
    using epsilon_filter_le_conv
    unfolding rewrite_sys_def
    by simp
qed

lemma lift_entailment_to_Union:
  fixes N D
  defines "RD ≡ rewrite_sys N D"
  assumes
    D_in: "D ∈ N" and
    RD_entails_D: "upair ` (rewrite_in_context RD)↓ ⊫ D"
  shows
    "upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ D" and
    "⋀C. C ∈ N ⟹ D ≺c C ⟹ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ D"
proof -
  from RD_entails_D obtain L s t where
    L_in: "L ∈# D" and
    L_eq_disj_L_eq: "L = Pos (Upair s t) ∧ (s, t) ∈ (rewrite_in_context RD)↓ ∨
     L = Neg (Upair s t) ∧ (s, t) ∉ (rewrite_in_context RD)↓"
    unfolding true_cls_def true_lit_iff
    by (metis (no_types, opaque_lifting) image_iff prod.case surj_pair uprod_exhaust)

  from L_eq_disj_L_eq show
    "upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ D" and
    "⋀C. C ∈ N ⟹ D ≺c C ⟹ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ D"
    unfolding atomize_all atomize_conj atomize_imp
  proof (elim disjE conjE)
    assume L_def: "L = Pos (Upair s t)" and "(s, t) ∈ (rewrite_in_context RD)↓"
    have "RD ⊆ (⋃D ∈ N. epsilon N D)" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ RD ⊆ rewrite_sys N C"
      unfolding RD_def rewrite_sys_def
      using D_in clause.order.transp_on_less[THEN transpD]
      using epsilon_filter_le_conv
      by (auto intro: Collect_mono)

    hence "rewrite_in_context RD ⊆ rewrite_in_context (⋃D ∈ N. epsilon N D)" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ rewrite_in_context RD ⊆ rewrite_in_context (rewrite_sys N C)"
      by (auto intro!: rewrite_in_context_mono)

    hence "(s, t) ∈ (rewrite_in_context (⋃D ∈ N. epsilon N D))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ (s, t) ∈ (rewrite_in_context (rewrite_sys N C))↓"
      by (auto intro!: join_mono intro: set_mp[OF _ ‹(s, t) ∈ (rewrite_in_context RD)↓›])

    thus "upair ` (rewrite_in_context (⋃ (epsilon N ` N)))↓ ⊫ D ∧
      (∀C. C ∈ N ⟶ D ≺c C ⟶ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ D)"
      unfolding true_cls_def true_lit_iff
      using L_in L_def by blast
  next
    have "(t1, t2) ∈ RD ⟹ t2 ≺t t1" for t1 t2
      by (auto simp: RD_def rewrite_sys_def elim: mem_epsilonE)

    hence ball_RD_rhs_lt_lhs: "(t1, t2) ∈ rewrite_in_context RD ⟹ t2 ≺t t1" for t1 t2
      by (smt (verit, ccfv_SIG) Pair_inject term.order.context_compatibility mem_Collect_eq
          rewrite_in_context_def)

    assume L_def: "L = Neg (Upair s t)" and "(s, t) ∉ (rewrite_in_context RD)↓"

    have "(s, t) ∈ (rewrite_in_context RD ∪ rewrite_in_context (⋃C ∈ {C ∈ N. D ≼c C}. epsilon N C))↓ ⟷
      (s, t) ∈ (rewrite_in_context RD)↓"
    proof (rule mem_join_union_iff_mem_join_lhs')
      show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context RD ⟹ t2 ≺t t1"
        using ball_RD_rhs_lt_lhs by simp
    next
      have ball_Rinf_minus_lt_lhs: "s ≺t fst rule ∧ t ≺t fst rule"
        if rule_in: "rule ∈ (⋃C ∈ {C ∈ N. D ≼c C}. epsilon N C)"
        for rule
      proof -
        from rule_in obtain C where
          "C ∈ N" and "D ≼c C" and "rule ∈ epsilon N C"
          by auto

        have epsilon_C_eq: "epsilon N C = {(fst rule, snd rule)}"
          using ‹rule ∈ epsilon N C› epsilon_eq_empty_or_singleton by force

        show ?thesis
          using less_trm_if_neg[OF ‹D ≼c C› epsilon_C_eq L_in]
          by (simp add: L_def)
      qed

      show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context (⋃ (epsilon N ` {C ∈ N. (≺c)== D C})) ⟹
        s ≺t t1 ∧ t ≺t t1"
        using less_trm_const_lhs_if_mem_rewrite_inside_gctxt
        using ball_Rinf_minus_lt_lhs
        by force
    qed

    moreover have
      "(s, t) ∈ (rewrite_in_context RD ∪ rewrite_in_context (⋃C' ∈ {C' ∈ N. D ≼c C' ∧ C' ≺c C}. epsilon N C'))↓ ⟷
       (s, t) ∈ (rewrite_in_context RD)↓"
      if "C ∈ N" and "D ≺c C"
      for C
    proof (rule mem_join_union_iff_mem_join_lhs')
      show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context RD ⟹ t2 ≺t t1"
        using ball_RD_rhs_lt_lhs by simp
    next
      have ball_lt_lhs: "s ≺t t1 ∧ t ≺t t1"
        if "C ∈ N" and "D ≺c C" and
          rule_in: "(t1, t2) ∈ (⋃C' ∈ {C' ∈ N. D ≼c C' ∧ C' ≺c C}. epsilon N C')"
        for C t1 t2
      proof -
        from rule_in obtain C' where
          "C' ∈ N" and "D ≼c C'" and "C' ≺c C" and "(t1, t2) ∈ epsilon N C'"
          by (auto simp: rewrite_sys_def)

        have epsilon_C'_eq: "epsilon N C' = {(t1, t2)}"
          using ‹(t1, t2) ∈ epsilon N C'› epsilon_eq_empty_or_singleton 
          by (metis insert_absorb singletonD)

        show ?thesis
          using less_trm_if_neg[OF ‹D ≼c C'› epsilon_C'_eq L_in]
          by (simp add: L_def)
      qed

      show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context (⋃ (epsilon N ` {C' ∈ N. (≺c)== D C' ∧ C' ≺c C})) ⟹
        s ≺t t1 ∧ t ≺t t1"
        using less_trm_const_lhs_if_mem_rewrite_inside_gctxt
        using ball_lt_lhs[OF that(1,2)]
        by (metis (no_types, lifting))
    qed

    ultimately have "(s, t) ∉ (rewrite_in_context RD ∪ rewrite_in_context (⋃C ∈ {C ∈ N. D ≼c C}. epsilon N C))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶
        (s, t) ∉ (rewrite_in_context RD ∪ rewrite_in_context (⋃C' ∈ {C' ∈ N. D ≼c C' ∧ C' ≺c C}. epsilon N C'))↓"
      using ‹(s, t) ∉ (rewrite_in_context RD)↓› by simp_all

    hence "(s, t) ∉ (rewrite_in_context (⋃D ∈ N. epsilon N D))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ (s, t) ∉ (rewrite_in_context (rewrite_sys N C))↓"
      using split_Union_epsilon'[OF D_in, folded RD_def]
      using split_rewrite_sys[OF _ D_in, folded RD_def]
      by (simp_all add: rewrite_in_context_union)

    hence "(Upair s t) ∉ upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ (Upair s t) ∉ upair ` (rewrite_in_context (rewrite_sys N C))↓"
      unfolding atomize_conj
      by (meson sym_join true_lit_simps(2) true_lit_uprod_iff_true_lit_prod(2))

    thus "upair ` (rewrite_in_context (⋃ (epsilon N ` N)))↓ ⊫ D ∧
    (∀C. C ∈ N ⟶ D ≺c C ⟶ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ D)"
      unfolding true_cls_def true_lit_iff
      using L_in L_def
      by blast
  qed
qed

lemma
  assumes productive: "epsilon N C = {(l, r)}"
  shows
    true_cls_if_productive_epsilon:
      "upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ C"
      "⋀D. D ∈ N ⟹ C ≺c D ⟹ upair ` (rewrite_in_context (rewrite_sys N D))↓ ⊫ C" and
    false_cls_if_productive_epsilon:
      "¬ upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ C - {#l ≈ r#}"
      "⋀D. D ∈ N ⟹ C ≺c D ⟹ ¬ upair ` (rewrite_in_context (rewrite_sys N D))↓ ⊫ C - {#l ≈ r#}"
proof -
  from productive have "(l, r) ∈ epsilon N C"
    by simp

  then obtain C' where
    C_in: "C ∈ N" and
    C_def: "C = add_mset (l ≈ r) C'" and
    "select C = {#}" and
    "is_strictly_maximal (l ≈ r) C" and
    "r ≺t l" and
    e: "¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C" and
    f: "¬ upair ` (rewrite_in_context (insert (l, r) (rewrite_sys N C)))↓ ⊫ C'" and
    "l ∈ NF (rewrite_in_context (rewrite_sys N C))"
    by (rule mem_epsilonE) blast

  have "(l, r) ∈ (rewrite_in_context (⋃D ∈ N. epsilon N D))↓"
    using C_in ‹(l, r) ∈ epsilon N C› mem_rewrite_in_context_if_mem_rewrite_rules
    by blast

  thus "upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ C"
    using C_def
    by blast

  have "rewrite_in_context (⋃D ∈ N. epsilon N D) =
        rewrite_in_context (rewrite_sys N C ∪ epsilon N C ∪ (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D))"
    using split_Union_epsilon[OF C_in]
    by simp

  also have "… =
    rewrite_in_context (rewrite_sys N C ∪ epsilon N C) ∪
    rewrite_in_context (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D)"
    by (simp add: rewrite_in_context_union)

  finally have rewrite_inside_gctxt_Union_epsilon_eq:
    "rewrite_in_context (⋃D ∈ N. epsilon N D) =
      rewrite_in_context (insert (l, r) (rewrite_sys N C)) ∪
      rewrite_in_context (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D)"
    unfolding productive
    by simp

  have mem_join_union_iff_mem_lhs:"(t1, t2) ∈ (rewrite_in_context (insert (l, r) (rewrite_sys N C)) ∪
    rewrite_in_context (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D))↓ ⟷
    (t1, t2) ∈ (rewrite_in_context (insert (l, r) (rewrite_sys N C)))↓"
    if "t1 ≼t l" and "t2 ≼t l"
    for t1 t2
  proof (rule mem_join_union_iff_mem_join_lhs')
    fix s1 s2 assume "(s1, s2) ∈ rewrite_in_context (insert (l, r) (rewrite_sys N C))"

    moreover have "s2 ≺t s1" if "(s1, s2) ∈ rewrite_in_context {(l, r)}"
    proof (rule rhs_lt_lhs_if_rule_in_rewrite_in_context[OF that])
      show "⋀s1 s2. (s1, s2) ∈ {(l, r)} ⟹ s2 ≺t s1"
        using ‹r ≺t l›
        by simp
    qed simp_all

    moreover have "s2 ≺t s1" if "(s1, s2) ∈ rewrite_in_context (rewrite_sys N C)"
    proof (rule rhs_lt_lhs_if_rule_in_rewrite_in_context[OF that])
      show "⋀s1 s2. (s1, s2) ∈ rewrite_sys N C ⟹ s2 ≺t s1"
        by (simp add: rhs_lt_lhs_if_mem_rewrite_sys)
    qed simp

    ultimately show "s2 ≺t s1"
      using rewrite_in_context_union[of "{(l, r)}", simplified] by blast
  next
    have ball_lt_lhs: "t1 ≺t s1 ∧ t2 ≺t s1"
      if rule_in: "(s1, s2) ∈ (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D)"
      for s1 s2
    proof -
      from rule_in obtain D where
        "D ∈ N" and "C ≺c D" and "(s1, s2) ∈ epsilon N D"
        by (auto simp: rewrite_sys_def)

      have ED_eq: "epsilon N D = {(s1, s2)}"
        using ‹(s1, s2) ∈ epsilon N D› epsilon_eq_empty_or_singleton by force

      have "l ≺t s1"
        using ‹C ≺c D›
        using less_trm_iff_less_cls_if_lhs_epsilon[OF ED_eq productive]
        by metis

      with ‹t1 ≼t l› ‹t2 ≼t l› show ?thesis
        by (metis reflclp_iff transpD term.order.transp)
    qed
    thus "⋀l r. (l, r) ∈ rewrite_in_context (⋃ (epsilon N ` {D ∈ N. C ≺c D})) ⟹ t1 ≺t l ∧ t2 ≺t l"
      using rewrite_inside_gctxt_Union_epsilon_eq
      using less_trm_const_lhs_if_mem_rewrite_inside_gctxt
      by presburger
  qed

  have neg_concl1: "¬ upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ C'"
    unfolding true_cls_def Set.bex_simps
  proof (intro ballI)
    fix L assume L_in: "L ∈# C'"
    hence "L ∈# C"
      by (simp add: C_def)

    obtain t1 t2 where
      atm_L_eq: "atm_of L = Upair t1 t2"
      by (metis uprod_exhaust)

    hence trms_of_L: "mset_uprod (atm_of L) = {#t1, t2#}"
      by simp

    hence "t1 ≼t l" and "t2 ≼t l"
      unfolding atomize_conj
      using less_trm_if_neg[OF reflclp_refl productive ‹L ∈# C›]
      using lesseq_trm_if_pos[OF reflclp_refl productive ‹L ∈# C›]
      by (metis (no_types, opaque_lifting) add_mset_commute sup2CI)

    have "(t1, t2) ∉ (rewrite_in_context (⋃D ∈ N. epsilon N D))↓" if L_def: "L = Pos (Upair t1 t2)"
    proof -
      from that have "(t1, t2) ∉ (rewrite_in_context (insert (l, r) (rewrite_sys N C)))↓"
        using f ‹L ∈# C'›
        by blast

      thus ?thesis
        using rewrite_inside_gctxt_Union_epsilon_eq mem_join_union_iff_mem_lhs[OF ‹t1 ≼t l› ‹t2 ≼t l›]
        by simp
    qed

    moreover have "(t1, t2) ∈ (rewrite_in_context (⋃D ∈ N. epsilon N D))↓"
      if L_def: "L = Neg (Upair t1 t2)"
    proof -
      from that have "(t1, t2) ∈ (rewrite_in_context (insert (l, r) (rewrite_sys N C)))↓"
        using f ‹L ∈# C'›
        by (meson true_lit_uprod_iff_true_lit_prod(2) sym_join true_cls_def true_lit_simps(2))

      thus ?thesis
        using rewrite_inside_gctxt_Union_epsilon_eq
          mem_join_union_iff_mem_lhs[OF ‹t1 ≼t l› ‹t2 ≼t l›]
        by simp
    qed

    ultimately show "¬ upair ` (rewrite_in_context (⋃ (epsilon N ` N)))↓ ⊫l L"
      using atm_L_eq true_lit_uprod_iff_true_lit_prod[OF sym_join] true_lit_simps
      by (smt (verit, ccfv_SIG) literal.exhaust_sel)
  qed

  then show "¬ upair ` (rewrite_in_context (⋃D ∈ N. epsilon N D))↓ ⊫ C - {#Pos (Upair l r)#}"
    by (simp add: C_def)

  fix D
  assume "D ∈ N" and "C ≺c D"

  have "(l, r) ∈ rewrite_sys N D"
    using C_in ‹(l, r) ∈ epsilon N C› ‹C ≺c D› mem_rewrite_sys_if_less_cls
    by iprover

  hence "(l, r) ∈ (rewrite_in_context (rewrite_sys N D))↓"
    by auto

  thus "upair ` (rewrite_in_context (rewrite_sys N D))↓ ⊫ C"
    using C_def
    by blast

  from ‹D ∈ N› have "rewrite_sys N D ⊆ (⋃D ∈ N. epsilon N D)"
    by (simp add: split_Union_epsilon')

  hence "rewrite_in_context (rewrite_sys N D) ⊆ rewrite_in_context (⋃D ∈ N. epsilon N D)"
    using rewrite_in_context_mono
    by metis

  hence "(rewrite_in_context (rewrite_sys N D))↓ ⊆ (rewrite_in_context (⋃D ∈ N. epsilon N D))↓"
    using join_mono
    by metis

  have "¬ upair ` (rewrite_in_context (rewrite_sys N D))↓ ⊫ C'"
    unfolding true_cls_def Set.bex_simps
  proof (intro ballI)
    fix L assume L_in: "L ∈# C'"
    hence "L ∈# C"
      by (simp add: C_def)

    obtain t1 t2 where
      atm_L_eq: "atm_of L = Upair t1 t2"
      by (metis uprod_exhaust)

    hence trms_of_L: "mset_uprod (atm_of L) = {#t1, t2#}"
      by simp

    hence "t1 ≼t l" and "t2 ≼t l"
      unfolding atomize_conj
      using less_trm_if_neg[OF reflclp_refl productive ‹L ∈# C›]
      using lesseq_trm_if_pos[OF reflclp_refl productive ‹L ∈# C›]
      by (metis (no_types, opaque_lifting) add_mset_commute sup2CI)

    have "(t1, t2) ∉ (rewrite_in_context (rewrite_sys N D))↓" if L_def: "L = Pos (Upair t1 t2)"
    proof -
      from that have "(t1, t2) ∉ (rewrite_in_context (insert (l, r) (rewrite_sys N C)))↓"
        using f ‹L ∈# C'› by blast
      thus ?thesis
        using rewrite_inside_gctxt_Union_epsilon_eq
        using mem_join_union_iff_mem_lhs[OF ‹t1 ≼t l› ‹t2 ≼t l›]
        using ‹(rewrite_in_context (rewrite_sys N D))↓ ⊆ (rewrite_in_context (⋃ (epsilon N ` N)))↓› by auto
    qed

    moreover have "(t1, t2) ∈ (rewrite_in_context (rewrite_sys N D))↓" if L_def: "L = Neg (Upair t1 t2)"
      using e
    proof (rule contrapos_np)
      assume "(t1, t2) ∉ (rewrite_in_context (rewrite_sys N D))↓"

      hence "(t1, t2) ∉ (rewrite_in_context (rewrite_sys N C))↓"
        using rewrite_sys_subset_if_less_cls[OF ‹C ≺c D›]
        by (meson join_mono rewrite_in_context_mono subsetD)

      thus "upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C"
        using neg_literal_notin_imp_true_cls[of "Upair t1 t2" C "upair ` _↓"]
        unfolding uprod_mem_image_iff_prod_mem[OF sym_join]
        using L_def L_in C_def
        by simp
    qed

    ultimately show "¬ upair ` (rewrite_in_context (rewrite_sys N D))↓ ⊫l L"
      using atm_L_eq true_lit_uprod_iff_true_lit_prod[OF sym_join] true_lit_simps
      by (smt (verit, ccfv_SIG) literal.exhaust_sel)
  qed
  thus "¬ upair ` (rewrite_in_context (rewrite_sys N D))↓ ⊫ C - {#l ≈ r#}"
    by (simp add: C_def)
qed

lemma trans_join_rewrite_inside_gctxt_rewrite_sys: "trans ((rewrite_in_context (rewrite_sys N C))↓)"
proof (rule trans_join)
  have "wf ((rewrite_in_context (rewrite_sys N C))¯)"
  proof (rule wf_converse_rewrite_in_context)
    fix s t
    assume "(s, t) ∈ rewrite_sys N C"

    then obtain D where "(s, t) ∈ epsilon N D"
      unfolding rewrite_sys_def
      using epsilon_filter_le_conv
      by auto

    thus "t ≺t s"
      by (auto elim: mem_epsilonE)
  qed auto
  thus "SN (rewrite_in_context (rewrite_sys N C))"
    by (simp only: SN_iff_wf)
next
  show "WCR (rewrite_in_context (rewrite_sys N C))"
    unfolding rewrite_sys_def epsilon_filter_le_conv
    using WCR_Union_rewrite_sys
    by (metis (mono_tags, lifting))
qed

lemma true_cls_insert_and_not_true_clsE:
  assumes
    "upair ` (rewrite_in_context (insert r R))↓ ⊫ C" and
    "¬ upair ` (rewrite_in_context R)↓ ⊫ C"
  obtains t t' where
    "Pos (Upair t t') ∈# C" and
    "t ≺t t'" and
    "(t, t') ∈ (rewrite_in_context (insert r R))↓" and
    "(t, t') ∉ (rewrite_in_context R)↓"
proof -
  assume hyp: "⋀t t'. t ≈ t' ∈# C ⟹ t ≺t t' ⟹ (t, t') ∈ (rewrite_in_context (insert r R))↓ ⟹
    (t, t') ∉ (rewrite_in_context R)↓ ⟹ thesis"

  from assms obtain L where
    "L ∈# C" and
    entails_L: "upair ` (rewrite_in_context (insert r R))↓ ⊫l L" and
    doesnt_entail_L: "¬ upair ` (rewrite_in_context R)↓ ⊫l L"
    by (meson true_cls_def)

  have "totalp_on (set_uprod (atm_of L)) (≺t)"
    by simp

  then obtain t t' where "atm_of L = Upair t t'" and "t ≼t t'"
    using ex_ordered_Upair by metis

  show ?thesis
  proof (cases L)
    case (Pos A)

    hence L_def: "L = t ≈ t'"
      using ‹atm_of L = Upair t t'›
      by simp

    moreover have "(t, t') ∈ (rewrite_in_context (insert r R))↓"
      using entails_L
      unfolding L_def
      unfolding true_lit_uprod_iff_true_lit_prod[OF sym_join]
      by (simp add: true_lit_def)

    moreover have "(t, t') ∉ (rewrite_in_context R)↓"
      using doesnt_entail_L
      unfolding L_def
      unfolding true_lit_uprod_iff_true_lit_prod[OF sym_join]
      by (simp add: true_lit_def)

    ultimately show ?thesis
      using hyp ‹L ∈# C› ‹t ≼t t'› by auto
  next
    case (Neg A)
    hence L_def: "L = Neg (Upair t t')"
      using ‹atm_of L = Upair t t'› by simp

    have "(t, t') ∉ (rewrite_in_context (insert r R))↓"
      using entails_L
      unfolding L_def
      unfolding true_lit_uprod_iff_true_lit_prod[OF sym_join]
      by (simp add: true_lit_def)

    moreover have "(t, t') ∈ (rewrite_in_context R)↓"
      using doesnt_entail_L
      unfolding L_def
      unfolding true_lit_uprod_iff_true_lit_prod[OF sym_join]
      by (simp add: true_lit_def)

    moreover have "(rewrite_in_context R)↓ ⊆ (rewrite_in_context (insert r R))↓"
      using join_mono rewrite_in_context_mono
      by (metis subset_insertI)

    ultimately have False
      by auto

    thus ?thesis ..
  qed
qed

lemma model_preconstruction:
  fixes
    N :: "'t clause set" and
    C :: "'t clause"
  defines
    "entails ≡ λE C. upair ` (rewrite_in_context E)↓ ⊫ C"
  assumes "saturated N" and "{#} ∉ N" and C_in: "C ∈ N"
  shows
    "epsilon N C = {} ⟷ entails (rewrite_sys N C) C"
    "⋀D. D ∈ N ⟹ C ≺c D ⟹ entails (rewrite_sys N D) C"
  unfolding atomize_all atomize_conj atomize_imp
  using clause.order.wfp C_in
proof (induction C rule: wfp_induct_rule)
  case (less C)
  note IH = less.IH

  from ‹{#} ∉ N› ‹C ∈ N› have "C ≠ {#}"
    by metis

  define I where
    "I = (rewrite_in_context (rewrite_sys N C))↓"

  have "refl I"
    by (simp only: I_def refl_join)

  have "trans I"
    unfolding I_def
    using trans_join_rewrite_inside_gctxt_rewrite_sys .

  have "sym I"
    by (simp only: I_def sym_join)

  have "compatible_with_context I"
    by (simp only: I_def compatible_with_context_join compatible_with_context_rewrite_in_context)

  note I_interp = ‹refl I› ‹trans I› ‹sym I› ‹compatible_with_context I›

  have i: "(epsilon N C = {}) ⟷ entails (rewrite_sys N C) C"
  proof (rule iffI)
    show "entails (rewrite_sys N C) C ⟹ epsilon N C = {}"
      unfolding entails_def rewrite_sys_def
      by (metis (no_types) empty_iff equalityI mem_epsilonE rewrite_sys_def subsetI)
  next
    assume "epsilon N C = {}"

    have cond_conv: "(∃L. L ∈# select C ∨ (select C = {#} ∧ is_maximal L C ∧ is_neg L)) ⟷
      (∃A. Neg A ∈# C ∧ (Neg A ∈# select C ∨ select C = {#} ∧ is_maximal (Neg A) C))"
    proof(cases "select C = {#}")
      case True

      have "⋀L. is_maximal L C ⟹ is_neg L ⟹ ∃A. Neg A ∈# C ∧ is_maximal (Neg A) C"
        by (metis (lifting) is_maximal_def literal.collapse(2))

       then show ?thesis
         using True
         by auto
    next
      case False

      have "⋀L. L ∈# select C ⟹ ∃A. Neg A ∈# C ∧ Neg A ∈# select C"
        by (metis literal.collapse(2) mset_subset_eqD select_negative_literals select_subset)

      then show ?thesis
        using False
        by auto
    qed

    show "entails (rewrite_sys N C) C"
    proof (cases "∃L. is_maximal L (select C) ∨ (select C = {#} ∧ is_maximal L C ∧ is_neg L)")
      case ex_neg_lit_sel_or_max: True

      hence exists_neg: 
        "∃A. Neg A ∈# C ∧ (is_maximal (Neg A) (select C) ∨ select C = {#} ∧ is_maximal (Neg A) C)"
        by (metis (lifting) literal.collapse(2) maximal_in_clause mset_subset_eqD 
            select_negative_literals select_subset)

      then obtain s s' where
        "s !≈ s' ∈# C" and
        sel_or_max: "select C = {#} ∧ is_maximal (s !≈ s') C ∨ is_maximal (s !≈ s') (select C)"
      proof -
        obtain A where 
          "Neg A ∈# C ∧ (is_maximal (Neg A) (select C) ∨ select C = {#} ∧ is_maximal (Neg A) C)"
          using exists_neg
          by presburger

        moreover then obtain s s' where "s !≈ s' = Neg A"
          by (metis uprod_exhaust)
        
        ultimately show ?thesis
          using that
          by blast
      qed

      then obtain C' where
        C_def: "C = add_mset (Neg (Upair s s')) C'"
        by (metis mset_add)

      show ?thesis
      proof (cases "upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫l Pos (Upair s s')")
        case True
        hence "(s, s') ∈ (rewrite_in_context (rewrite_sys N C))↓"
          by (meson sym_join true_lit_simps(1) true_lit_uprod_iff_true_lit_prod(1))

        have "s = s' ∨ s ≺t s' ∨ s' ≺t s"
          by auto

        thus ?thesis
        proof (rule disjE)
          assume "s = s'"
          define ι :: "'t clause inference" where
            "ι = Infer [C] C'"

          have "eq_resolution C C'"
          proof (rule eq_resolutionI)
            show "C = add_mset (Neg (Upair s s')) C'"
              by (simp only: C_def)
          next
            show "s !≈ s' = s !≈ s"
              by (simp only: ‹s = s'›)
          next
            show "select C = {#} ∧ is_maximal (s !≈ s') C ∨ is_maximal (s !≈ s') (select C)"
              using sel_or_max .
          qed simp

          hence "ι ∈ G_Inf"
            by (auto simp only: ι_def G_Inf_def)

          moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
            using ‹C ∈ N›
            by (simp add: ι_def)

          ultimately have "ι ∈ Inf_from N"
            by (auto simp: Inf_from_def)

          hence "ι ∈ Red_I N"
            using ‹saturated N›
            by (auto simp: saturated_def)

          then obtain DD where
            DD_subset: "DD ⊆ N" and
            "finite DD" and
            DD_entails_C': "G_entails DD {C'}" and
            ball_DD_lt_C: "∀D ∈ DD. D ≺c C"
            unfolding Red_I_def redundant_infer_def
            by (auto simp: ι_def)

          moreover have "∀D∈DD. entails (rewrite_sys N C) D"
            using IH[THEN conjunct2, rule_format, of _ C]
            using ‹C ∈ N› DD_subset ball_DD_lt_C
            by blast

          ultimately have "entails (rewrite_sys N C) C'"
            using I_interp DD_entails_C'
            unfolding entails_def G_entails_def
            by (simp add: I_def true_clss_def)

          then show "entails (rewrite_sys N C) C"
            using C_def entails_def
            by simp
        next
          from ‹(s, s') ∈ (rewrite_in_context (rewrite_sys N C))↓› obtain u where
            s_u: "(s, u) ∈ (rewrite_in_context (rewrite_sys N C))*" and
            s'_u: "(s', u) ∈ (rewrite_in_context (rewrite_sys N C))*"
            by auto

          moreover hence "u ≼t s" and "u ≼t s'"
            using rhs_lesseq_trm_lhs_if_mem_rtrancl_rewrite_inside_gctxt_rewrite_sys by simp_all

          moreover assume "s ≺t s' ∨ s' ≺t s"

          ultimately obtain u0 where
            "s' ≺t s ⟹ (s, u0) ∈ rewrite_in_context (rewrite_sys N C)"
            "s ≺t s' ⟹ (s', u0) ∈ rewrite_in_context (rewrite_sys N C)" and
            "(u0, u) : (rewrite_in_context (rewrite_sys N C))*"
            using ex_step_if_joinable[OF _ s_u s'_u]
            by (metis asympD term.order.asymp)

          then obtain c t t' where
            s_eq_if: "s' ≺t s ⟹ s = c⟨t⟩" and
            s'_eq_if: "s ≺t s' ⟹ s' = c⟨t⟩" and
            "u0 = c⟨t'⟩" and
            "(t, t') ∈ rewrite_sys N C"
            by (smt (verit) Pair_inject ‹s ≺t s' ∨ s' ≺t s› asympD term.order.asymp mem_Collect_eq
                rewrite_in_context_def)

          then obtain D where
            "(t, t') ∈ epsilon N D" and "D ∈ N" and "D ≺c C"
            unfolding rewrite_sys_def epsilon_filter_le_conv
            by auto

          then obtain D' where
            D_def: "D = add_mset (Pos (Upair t t')) D'" and
            sel_D: "select D = {#}" and
            max_t_t': "is_strictly_maximal (Pos (Upair t t')) D" and
            "t' ≺t t"
            by (elim mem_epsilonE) fast

          have superI: "neg_superposition D C (add_mset (s1⟨t'⟩ !≈ s1') (C' + D'))"
            if "{s, s'} = {s1⟨t⟩, s1'}" and "s1' ≺t s1⟨t⟩"
            for s1 s1'
          proof (rule neg_superpositionI)
            show "C = add_mset (s !≈ s') C'"
              by (simp only: C_def)
          next
            show "D = add_mset (t ≈ t') D'"
              by (simp only: D_def)
          next
            show "D ≺c C"
              using ‹D ≺c C› .
          next
            show "select C = {#} ∧ is_maximal (s !≈ s') C ∨ is_maximal (s !≈ s') (select C)"
              using sel_or_max .
          next
            show "select D = {#}"
              using sel_D .
          next
            show "is_strictly_maximal (t ≈ t') D"
              using max_t_t' .
          next
            show "t' ≺t t"
              using ‹t' ≺t t› .
          next
            from that(1) show "s !≈ s' = s1⟨t⟩ !≈ s1'"
              by (simp add: doubleton_eq_iff)
          next
            from that(2) show "s1' ≺t s1⟨t⟩" .
          qed simp_all

          have "neg_superposition D C (add_mset (c⟨t'⟩ !≈ s') (C' + D'))"
            if ‹s' ≺t s›
          proof (rule superI)
            from that show "{s, s'} = {c⟨t⟩, s'}"
              using s_eq_if
              by simp
          next
            from that show "s' ≺t c⟨t⟩"
              using s_eq_if
              by simp
          qed

          moreover have "neg_superposition D C (add_mset (c⟨t'⟩ !≈ s) (C' + D'))"
            if ‹s ≺t s'›
          proof (rule superI)
            from that show "{s, s'} = {c⟨t⟩, s}"
              using s'_eq_if
              by auto
          next
            from that show "s ≺t c⟨t⟩"
              using s'_eq_if
              by simp
          qed

          ultimately obtain CD where
            super: "neg_superposition D C CD" and
            CD_eq1: "s' ≺t s ⟹ CD = add_mset (c⟨t'⟩ !≈ s') (C' + D')" and
            CD_eq2: "s ≺t s' ⟹ CD = add_mset (c⟨t'⟩ !≈ s) (C' + D')"
            using ‹s ≺t s' ∨ s' ≺t s› s'_eq_if s_eq_if
            by metis

          define ι :: "'t clause inference" where
            "ι = Infer [D, C] CD"

          have "ι ∈ G_Inf"
            using superposition_if_neg_superposition[OF super]
            by (auto simp only: ι_def G_Inf_def)

          moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
            using ‹C ∈ N› ‹D ∈ N›
            by (auto simp add: ι_def)

          ultimately have "ι ∈ Inf_from N"
            by (auto simp: Inf_from_def)

          hence "ι ∈ Red_I N"
            using ‹saturated N›
            by (auto simp: saturated_def)

          then obtain DD where
            DD_subset: "DD ⊆ N" and
            "finite DD" and
            DD_entails_CD: "G_entails (insert D DD) {CD}" and
            ball_DD_lt_C: "∀D∈DD. D ≺c C"
            unfolding Red_I_def redundant_infer_def mem_Collect_eq
            by (auto simp: ι_def)

          moreover have "∀D∈ insert D DD. entails (rewrite_sys N C) D"
            using IH[THEN conjunct2, rule_format, of _ C]
            using ‹C ∈ N› ‹D ∈ N› ‹D ≺c C› DD_subset ball_DD_lt_C
            by blast

          ultimately have "entails (rewrite_sys N C) CD"
            using I_interp DD_entails_CD
            unfolding entails_def G_entails_def
            by (simp add: I_def true_clss_def)

          moreover have "¬ entails (rewrite_sys N C) D'"
            unfolding entails_def
            using false_cls_if_productive_epsilon(2)[OF _ ‹C ∈ N› ‹D ≺c C›]
            by (metis D_def ‹(t, t') ∈ epsilon N D› add_mset_remove_trivial empty_iff
                 epsilon_eq_empty_or_singleton singletonD)

          moreover have "¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫l c⟨t'⟩ !≈ s'"
            if "s' ≺t s"
            using ‹(u0, u) ∈ (rewrite_in_context (rewrite_sys N C))*› ‹u0 = c⟨t'⟩› s'_u
            by blast

          moreover have "¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫l c⟨t'⟩ !≈ s"
            if "s ≺t s'"
            using ‹(u0, u) ∈ (rewrite_in_context (rewrite_sys N C))*› ‹u0 = c⟨t'⟩› s_u
            by blast

          ultimately show "entails (rewrite_sys N C) C"
            unfolding entails_def C_def
            using ‹s ≺t s' ∨ s' ≺t s› CD_eq1 CD_eq2
            by fast
        qed
      next
        case False
        thus ?thesis
          using ‹Neg (Upair s s') ∈# C›
          by (auto simp add: entails_def true_cls_def)
      qed
    next
      case False
      hence "select C = {#}"
        using literal.order.ex_maximal_in_mset by blast

      from False obtain A where Pos_A_in: "Pos A ∈# C" and max_Pos_A: "is_maximal (Pos A) C"
        using ‹select C = {#}› literal.order.ex_maximal_in_mset[OF ‹C ≠ {#}›]
        by (metis (lifting) is_pos_def maximal_in_clause)

      then obtain C' where C_def: "C = add_mset (Pos A) C'"
        by (meson mset_add)

      have "totalp_on (set_uprod A) (≺t)"
        by simp

      then obtain s s' where A_def: "A = Upair s s'" and "s' ≼t s"
        using ex_ordered_Upair[of A "(≺t)"] by fastforce

      show ?thesis
      proof (cases "upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C' ∨ s = s'")
        case True
        then show ?thesis
          using ‹epsilon N C = {}›
          using A_def C_def entails_def
          by blast
      next
        case False

        from False have "¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C'"
          by simp

        from False have "s' ≺t s"
          using ‹s' ≼t s› term.order.asymp[THEN asympD]
          by auto

        then show ?thesis
        proof (cases "is_strictly_maximal (Pos A) C")
          case strictly_maximal: True
          show ?thesis
          proof (cases "s ∈ NF (rewrite_in_context (rewrite_sys N C))")
            case s_irreducible: True

            hence e_or_f_doesnt_hold: "upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C ∨
              upair ` (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓ ⊫ C'"
              using ‹epsilon N C = {}›[unfolded  epsilon.simps[of N C]]
              using ‹C ∈ N› C_def ‹select C = {#}› strictly_maximal ‹s' ≺t s›
              unfolding A_def rewrite_sys_def
              by (smt (verit, best) Collect_empty_eq)

            show ?thesis
            proof (cases "upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C")
              case e_doesnt_hold: True
              thus ?thesis
                by (simp add: entails_def)
            next
              case e_holds: False
              hence R_C_doesnt_entail_C': "¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C'"
                unfolding C_def
                by simp

              show ?thesis
              proof (cases "upair ` (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓ ⊫ C'")
                case f_doesnt_hold: True
                then obtain C'' t t' where C'_def: "C' = add_mset (Pos (Upair t t')) C''" and
                  "t' ≺t t" and
                  "(t, t') ∈ (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓" and
                  "(t, t') ∉ (rewrite_in_context (rewrite_sys N C))↓"
                  using f_doesnt_hold R_C_doesnt_entail_C'
                  using true_cls_insert_and_not_true_clsE
                  by (metis insert_DiffM join_sym Upair_sym)

                have "Pos (Upair t t') ≺l Pos (Upair s s')"
                  using strictly_maximal literal.order.not_less_iff_gr_or_eq
                  unfolding literal.order.is_strictly_maximal_in_mset_iff A_def C'_def C_def
                  by auto

                have "¬ (t ≺t s)"
                proof (rule notI)
                  assume "t ≺t s"

                  have "(t, t') ∈ (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓ ⟷
                    (t, t') ∈ (rewrite_in_context (rewrite_sys N C))↓"
                    unfolding rewrite_in_context_union[of "{(s, s')}" "rewrite_sys N C", simplified]
                  proof (rule mem_join_union_iff_mem_join_rhs')
                    show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context {(s, s')} ⟹ t ≺t t1 ∧ t' ≺t t1"
                      using ‹t ≺t s› ‹t' ≺t t›
                      by (smt (verit, ccfv_threshold) fst_conv singletonD
                          less_trm_const_lhs_if_mem_rewrite_inside_gctxt transpD term.order.transp)
                  next
                    show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context (rewrite_sys N C) ⟹ t2 ≺t t1"
                      using rhs_less_trm_lhs_if_mem_rewrite_inside_gctxt_rewrite_sys by force
                  qed
                  thus False
                    using ‹(t, t') ∈ (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓›
                    using ‹(t, t') ∉ (rewrite_in_context (rewrite_sys N C))↓›
                    by metis
                qed

                moreover have "¬ (s ≺t t)"
                proof (rule notI)
                  assume "s ≺t t"
                  hence "multp (≺t) {#s, s'#} {#t, t'#}"
                    using ‹s' ≺t s› ‹t' ≺t t›
                    using one_step_implies_multp[of _ _ _ "{#}", simplified]
                    by (metis (mono_tags, opaque_lifting) empty_not_add_mset insert_iff
                        set_mset_add_mset_insert set_mset_empty singletonD transpD term.order.transp)

                  hence "Pos (Upair s s') ≺l Pos (Upair t t')"
                    by (simp add: lessl_def)

                  thus False
                    using ‹t ≈ t' ≺l s ≈ s'›
                    by order
                qed

                ultimately have "t = s"
                  by order
                hence "t' ≺t s'"
                  using ‹t' ≺t t› ‹s' ≺t s›
                  using ‹Pos (Upair t t') ≺l Pos (Upair s s')›
                  unfolding lessl_def
                  by (simp add: multp_cancel_add_mset term.order.transp)

                obtain t'' where
                  "(t, t'') ∈ rewrite_in_context (insert (s, s') (rewrite_sys N C))" and
                  "(t'', t') ∈ (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓"
                  using ‹(t, t') ∈ (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓›[THEN joinD]
                  using ex_step_if_joinable[OF term.order.asymp _ _ _ ‹t' ≺t t›]
                  by (smt (verit, ccfv_threshold) ‹t = s› converse_rtranclE insertCI joinI_right
                      join_sym r_into_rtrancl mem_rewrite_in_context_if_mem_rewrite_rules rtrancl_join_join)

                have "t'' ≺t t"
                proof (rule predicate_holds_of_mem_rewrite_in_context[of _ _ _ "λx y. y ≺t x"])
                  show "(t, t'') ∈ rewrite_in_context (insert (s, s') (rewrite_sys N C))"
                    using ‹(t, t'') ∈ rewrite_in_context (insert (s, s') (rewrite_sys N C))› .
                next
                  show "⋀t1 t2. (t1, t2) ∈ insert (s, s') (rewrite_sys N C) ⟹ t2 ≺t t1"
                    by (metis ‹s' ≺t s› insert_iff old.prod.inject rhs_lt_lhs_if_mem_rewrite_sys)
                next
                  show "⋀t1 t2 c σ. (t1, t2) ∈ insert (s, s') (rewrite_sys N C) ⟹
                    t2 ≺t t1 ⟹ c⟨t2⟩ ≺t c⟨t1⟩"
                    by (simp only: term.order.context_compatibility)
                qed

                have "(t, t'') ∈ rewrite_in_context {(s, s')}"
                  using ‹(t, t'') ∈ rewrite_in_context (insert (s, s') (rewrite_sys N C))›
                  using ‹t = s› s_irreducible mem_rewrite_step_union_NF
                  using rewrite_in_context_insert
                  by blast

                hence "∃c. s = c⟨s⟩ ∧ t'' = c⟨s'⟩"
                  by (simp add: ‹t = s› rewrite_in_context_def)

                hence "t'' = s'"
                  by (metis apply_hole term.order.dual_order.strict_iff_not 
                      term.order.subterm_property)

                moreover have "(t'', t') ∈ (rewrite_in_context (rewrite_sys N C))↓"
                proof (rule mem_join_union_iff_mem_join_rhs'[THEN iffD1])
                  show "(t'', t') ∈ (rewrite_in_context {(s, s')} ∪
                    rewrite_in_context (rewrite_sys N C))↓"
                    using ‹(t'', t') ∈ (rewrite_in_context (insert (s, s') (rewrite_sys N C)))↓›
                    using rewrite_in_context_union[of "{_}", simplified]
                    by metis
                next
                  show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context (rewrite_sys N C) ⟹ t2 ≺t t1"
                    using rhs_less_trm_lhs_if_mem_rewrite_inside_gctxt_rewrite_sys .
                next
                  show "⋀t1 t2. (t1, t2) ∈ rewrite_in_context {(s, s')} ⟹ t'' ≺t t1 ∧ t' ≺t t1"
                    using ‹t' ≺t t› ‹t'' ≺t t›
                    unfolding ‹t = s›
                    using less_trm_const_lhs_if_mem_rewrite_inside_gctxt
                    by fastforce
                qed

                ultimately have "(s', t') ∈ (rewrite_in_context (rewrite_sys N C))↓"
                  by simp

                let ?concl = "(add_mset (s' !≈ t') (add_mset (t ≈ t') C''))"

                define ι :: "'t clause inference" where
                  "ι = Infer [C] ?concl"

                have eq_fact: "eq_factoring C ?concl"
                proof (rule eq_factoringI)
                  show "C = add_mset (Pos (Upair s s')) (add_mset (Pos (Upair t t')) C'')"
                    by (simp add: C_def C'_def A_def)
                next
                  show "select C = {#}"
                    using ‹select C = {#}› .
                next
                  show "is_maximal (Pos (Upair s s')) C"
                    by (metis A_def max_Pos_A)
                next
                  show "s' ≺t s"
                    using ‹s' ≺t s› .
                next
                  show "Pos (Upair t t') = Pos (Upair s t')"
                    unfolding ‹t = s› ..
                next
                  show "add_mset (s' !≈ t') (add_mset (t ≈ t') C'') =
                        add_mset (s' !≈ t') (add_mset (s ≈ t') C'')"
                    by (auto simp add: ‹t = s›)
                qed simp_all

                hence "ι ∈ G_Inf"
                  by (auto simp: ι_def G_Inf_def)

                moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
                  using ‹C ∈ N›
                  by (auto simp add: ι_def)

                ultimately have "ι ∈ Inf_from N"
                  by (auto simp: Inf_from_def)

                hence "ι ∈ Red_I N"
                  using ‹saturated N›
                  by (auto simp: saturated_def)

                then obtain DD where
                  DD_subset: "DD ⊆ N" and
                  "finite DD" and
                  DD_entails_C': "G_entails DD {?concl}" and
                  ball_DD_lt_C: "∀D∈DD. D ≺c C"
                  unfolding Red_I_def redundant_infer_def
                  by (auto simp: ι_def)

                have "∀D∈DD. entails (rewrite_sys N C) D"
                  using IH[THEN conjunct2, rule_format, of _ C]
                  using ‹C ∈ N› DD_subset ball_DD_lt_C
                  by blast

                hence "entails (rewrite_sys N C) ?concl"
                  unfolding entails_def I_def[symmetric]
                  using DD_entails_C'[unfolded G_entails_def]
                  using I_interp
                  by (simp add: true_clss_def)

                thus "entails (rewrite_sys N C) C"
                  unfolding entails_def I_def[symmetric]
                  unfolding C_def C'_def A_def
                  using I_def ‹(s', t') ∈ (rewrite_in_context (rewrite_sys N C))↓›
                  by blast
              next
                case f_holds: False
                hence False
                  using e_or_f_doesnt_hold e_holds
                  by metis

                thus ?thesis ..
              qed
            qed
          next
            case s_reducible: False

            hence "∃ss. (s, ss) ∈ rewrite_in_context (rewrite_sys N C)"
              unfolding NF_def
              by auto

            then obtain c t t' D where
              "D ∈ N" and
              "D ≺c C" and
              "(t, t') ∈ epsilon N D" and
              "s = c⟨t⟩"
              using epsilon_filter_le_conv
              by (auto simp: rewrite_in_context_def rewrite_sys_def)

            obtain D' where
              D_def: "D = add_mset (Pos (Upair t t')) D'" and
              "select D = {#}" and
              max_t_t': "is_strictly_maximal (t ≈ t') D" and
              "t' ≺t t"
              using ‹(t, t') ∈ epsilon N D›
              by (elim mem_epsilonE) simp

            let ?concl = "(add_mset (c⟨t'⟩ ≈ s') (C' + D'))"

            define ι :: "'t clause inference" where
              "ι = Infer [D, C] ?concl"

            have super: "pos_superposition D C ?concl"
            proof (rule pos_superpositionI)
              show "C = add_mset (s ≈ s') C'"
                by (simp only: C_def A_def)
            next
              show "D = add_mset (t ≈ t') D'"
                by (simp only: D_def)
            next
              show "D ≺c C"
                using ‹D ≺c C› .
            next
              show "select D = {#}"
                using ‹select D = {#}› .
            next
              show "select C = {#}"
                using ‹select C = {#}› .
            next
              show "is_strictly_maximal (s ≈ s') C"
                using A_def strictly_maximal
                by simp
            next
              show "is_strictly_maximal (t ≈ t') D"
                using max_t_t' .
            next
              show "t' ≺t t"
                using ‹t' ≺t t› .
            next
              show "s ≈ s' = c⟨t⟩ ≈ s'"
                by (simp only: ‹s = c⟨t⟩›)
            next
              show "s' ≺t c⟨t⟩"
                using ‹s' ≺t s›
                unfolding ‹s = c⟨t⟩› .
            qed simp_all

            hence "ι ∈ G_Inf"
              using superposition_if_pos_superposition
              by (auto simp: ι_def G_Inf_def)

            moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
              using ‹C ∈ N› ‹D ∈ N›
              by (auto simp add: ι_def)

            ultimately have "ι ∈ Inf_from N"
              by (auto simp only: Inf_from_def)

            hence "ι ∈ Red_I N"
              using ‹saturated N›
              by (auto simp only: saturated_def)

            then obtain DD where
              DD_subset: "DD ⊆ N" and
              "finite DD" and
              DD_entails_concl: "G_entails (insert D DD) {?concl}" and
              ball_DD_lt_C: "∀D∈DD. D ≺c C"
              unfolding Red_I_def redundant_infer_def mem_Collect_eq
              by (auto simp: ι_def)

            moreover have "∀D∈ insert D DD. entails (rewrite_sys N C) D"
              using IH[THEN conjunct2, rule_format, of _ C]
              using ‹C ∈ N› ‹D ∈ N› ‹D ≺c C› DD_subset ball_DD_lt_C
              by blast

            ultimately have "entails (rewrite_sys N C) ?concl"
              using I_interp DD_entails_concl
              unfolding entails_def G_entails_def
              by (simp add: I_def true_clss_def)

            moreover have "¬ entails (rewrite_sys N C) D'"
              unfolding entails_def
              using false_cls_if_productive_epsilon(2)[OF _ ‹C ∈ N› ‹D ≺c C›]
              by (metis D_def ‹(t, t') ∈ epsilon N D› add_mset_remove_trivial empty_iff
                   epsilon_eq_empty_or_singleton singletonD)

            ultimately have "entails (rewrite_sys N C) {#c⟨t'⟩ ≈ s'#}"
              unfolding entails_def
              using ‹¬ upair ` (rewrite_in_context (rewrite_sys N C))↓ ⊫ C'›
              by fastforce

            hence "(c⟨t'⟩, s') ∈ (rewrite_in_context (rewrite_sys N C))↓"
              by (simp add: entails_def true_cls_def uprod_mem_image_iff_prod_mem[OF sym_join])

            moreover have "(c⟨t⟩, c⟨t'⟩) ∈ rewrite_in_context (rewrite_sys N C)"
              using ‹(t, t') ∈ epsilon N D› ‹D ∈ N› ‹D ≺c C› rewrite_sys_def epsilon_filter_le_conv
              by (auto simp: rewrite_in_context_def)

            ultimately have "(c⟨t⟩, s') ∈ (rewrite_in_context (rewrite_sys N C))↓"
              using r_into_rtrancl rtrancl_join_join
              by metis

            hence "entails (rewrite_sys N C) {#c⟨t⟩ ≈ s'#}"
              unfolding entails_def true_cls_def
              by auto

            thus ?thesis
              using A_def C_def ‹s = c⟨t⟩› entails_def
              by fastforce
          qed
        next
          case False
          hence "2 ≤ count C (Pos A)"
            using max_Pos_A
            unfolding C_def is_maximal_def is_strictly_maximal_def
            by auto

          then obtain C' where C_def: "C = add_mset (Pos A) (add_mset (Pos A) C')"
            using two_le_countE
            by metis

          define ι :: "'t clause inference" where
            "ι = Infer [C] (add_mset (s ≈ s') (add_mset (s' !≈ s') C'))"

          let ?concl = "add_mset (s ≈ s') (add_mset (s' !≈ s') C')"

          have eq_fact: "eq_factoring C ?concl"
          proof (rule eq_factoringI)
            show "C = add_mset (Pos A) (add_mset (Pos A) C')"
              by (simp add: C_def)
          next
            show "Pos A = s ≈ s'"
              by (simp add: A_def)
          next
            show "Pos A = s ≈ s'"
              by (simp add: A_def)
          next
            show "select C = {#}"
              using ‹select C = {#}› .
          next
            show "is_maximal (Pos A) C"
              using max_Pos_A .
          next
            show "s' ≺t s"
              using ‹s' ≺t s› .
          qed simp_all

          hence "ι ∈ G_Inf"
            by (auto simp: ι_def G_Inf_def)

          moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
            using ‹C ∈ N›
            by (auto simp add: ι_def)

          ultimately have "ι ∈ Inf_from N"
            by (auto simp: Inf_from_def)

          hence "ι ∈ Red_I N"
            using ‹saturated N›
            by (auto simp: saturated_def)

          then obtain DD where
            DD_subset: "DD ⊆ N" and
            "finite DD" and
            DD_entails_concl: "G_entails DD {?concl}" and
            ball_DD_lt_C: "∀D∈DD. D ≺c C"
            unfolding Red_I_def redundant_infer_def mem_Collect_eq
            by (auto simp: ι_def)

          moreover have "∀D∈DD. entails (rewrite_sys N C) D"
            using IH[THEN conjunct2, rule_format, of _ C]
            using ‹C ∈ N› DD_subset ball_DD_lt_C
            by blast

          ultimately have "entails (rewrite_sys N C) ?concl"
            using I_interp DD_entails_concl
            unfolding entails_def G_entails_def
            by (simp add: I_def true_clss_def)

          then show ?thesis
            by (simp add: entails_def A_def C_def joinI_right pair_imageI)
        qed
      qed
    qed
  qed

  moreover have iib: "entails (rewrite_sys N D) C" if "D ∈ N" and "C ≺c D" for D
    using epsilon_eq_empty_or_singleton[of N C, folded ]
  proof (elim disjE exE)
    assume "epsilon N C = {}"
    hence "entails (rewrite_sys N C) C"
      unfolding i by simp
    thus ?thesis
      using lift_entailment_to_Union(2)[OF ‹C ∈ N› _ that]
      by (simp only: entails_def)
  next
    fix l r assume "epsilon N C = {(l, r)}"
    thus ?thesis
      using true_cls_if_productive_epsilon(2)[OF ‹epsilon N C = {(l, r)}› that]
      by (simp only: entails_def)
  qed

  ultimately show ?case
    by argo
qed

lemma model_construction:
  fixes
    N :: "'t clause set" and
    C :: "'t clause"
  defines
    "entails ≡ λE C. upair ` (rewrite_in_context E)↓ ⊫ C"
  assumes "saturated N" and "{#} ∉ N" and C_in: "C ∈ N"
  shows "entails (⋃D ∈ N. epsilon N D) C"
  using epsilon_eq_empty_or_singleton[of N C]
proof (elim disjE exE)
  assume "epsilon N C = {}"

  hence "entails (rewrite_sys N C) C"
    using model_preconstruction(1)[OF assms(2,3,4)]
    by (metis entails_def)

  thus ?thesis
    using lift_entailment_to_Union(1)[OF ‹C ∈ N›]
    by (simp only: entails_def)
next
  fix l r assume "epsilon N C = {(l, r)}"
  thus ?thesis
    using true_cls_if_productive_epsilon(1)[OF ‹epsilon N C = {(l, r)}›]
    by (simp only: entails_def)
qed

subsection ‹Static Refutational Completeness›

lemma statically_complete:
  fixes N :: "'t clause set"
  assumes "saturated N" and "G_entails N {{#}}"
  shows "{#} ∈ N"
  using ‹G_entails N {{#}}›
proof (rule contrapos_pp)
  assume "{#} ∉ N"

  define I :: "'t rel" where
    "I = (rewrite_in_context (⋃D ∈ N. epsilon N D))↓"

  show "¬ G_entails N G_Bot"
    unfolding G_entails_def not_all not_imp
  proof (intro exI conjI)
    show "refl I"
      by (simp only: I_def refl_join)
  next
    show "trans I"
      unfolding I_def
    proof (rule trans_join)
      have "wf ((rewrite_in_context (⋃D ∈ N. epsilon N D))¯)"
      proof (rule wf_converse_rewrite_in_context)
        fix s t
        assume "(s, t) ∈ (⋃D ∈ N. epsilon N D)"
        then obtain C where "C ∈ N" "(s, t) ∈ epsilon N C"
          by auto

        thus "t ≺t s"
          by (auto elim: mem_epsilonE)
      qed auto
      thus "SN (rewrite_in_context (⋃D ∈ N. epsilon N D))"
        unfolding SN_iff_wf .
    next
      show "WCR (rewrite_in_context (⋃D ∈ N. epsilon N D))"
        using WCR_Union_rewrite_sys .
    qed
  next
    show "sym I"
      by (simp only: I_def sym_join)
  next
    show "compatible_with_context I"
      unfolding I_def
      by (simp only: I_def compatible_with_context_join compatible_with_context_rewrite_in_context)
  next
    show "upair ` I ⊫s N"
      unfolding I_def
      using model_construction[OF ‹saturated N› ‹{#} ∉ N›]
      by (simp add: true_clss_def)
  next
    show "¬ upair ` I ⊫s G_Bot"
      by simp
  qed
qed

sublocale statically_complete_calculus where
  Bot = G_Bot and
  Inf = G_Inf and
  entails = G_entails and
  Red_I = Red_I and
  Red_F = Red_F
  using statically_complete
  by unfold_locales simp

end

end