Theory Ground_Superposition_Completeness

theory Ground_Superposition_Completeness
  imports Ground_Superposition
begin

subsection ‹Redundancy Criterion›

sublocale ground_superposition_calculus ⊆ calculus_with_finitary_standard_redundancy where
  Inf = G_Inf and
  Bot = G_Bot and
  entails = G_entails and
  less = "(≺c)"
  defines GRed_I = Red_I and GRed_F = Red_F
proof unfold_locales
  show "transp (≺c)"
    using clause_order.transp_on_less .
next
  show "wfP (≺c)"
    using wfP_less_cls .
next
  show "⋀ι. ι ∈ G_Inf ⟹ prems_of ι ≠ []"
    by (auto simp: G_Inf_def)
next
  fix ι
  have "concl_of ι ≺c main_prem_of ι"
    if ι_def: "ι = Infer [P2, P1] C" and
      infer: "ground_superposition P2 P1 C"
    for P2 P1 C
    unfolding ι_def
    using infer
    using ground_superposition_smaller_conclusion
    by simp

  moreover have "concl_of ι ≺c main_prem_of ι"
    if ι_def: "ι = Infer [P] C" and
      infer: "ground_eq_resolution P C"
    for P C
    unfolding ι_def
    using infer
    using ground_eq_resolution_smaller_conclusion
    by simp

  moreover have "concl_of ι ≺c main_prem_of ι"
    if ι_def: "ι = Infer [P] C" and
      infer: "ground_eq_factoring P C"
    for P C
    unfolding ι_def
    using infer
    using ground_eq_factoring_smaller_conclusion
    by simp

  ultimately show "ι ∈ G_Inf ⟹ concl_of ι ≺c main_prem_of ι"
    unfolding G_Inf_def
    by fast
qed


subsection ‹Mode Construction›

context ground_superposition_calculus begin

function epsilon :: "_ ⇒ 'f gatom clause ⇒ 'f gterm 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_lit (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_inside_gctxt RC)↓ ⊫ C ∧
    ¬ upair ` (rewrite_inside_gctxt (insert (s, t) RC))↓ ⊫ C' ∧
    s ∈ NF (rewrite_inside_gctxt RC))}"
  by auto

termination epsilon
proof (relation "{((x1, x2), (y1, y2)). x2 ≺c y2}")
  define f :: "'c × 'f gterm uprod literal multiset ⇒ 'f gterm uprod literal multiset" where
    "f = (λ(x1, x2). x2)"
  have "wfp (λ(x1, x2) (y1, y2). x2 ≺c y2)"
  proof (rule wfP_if_convertible_to_wfP)
    show "⋀x y. (case x of (x1, x2) ⇒ λ(y1, y2). x2 ≺c y2) y ⟹ (snd x) ≺c (snd y)"
      by auto
  next
    show "wfP (≺c)"
      by simp
  qed
  thus "wf {((x1, x2), (y1, y2)). x2 ≺c y2}"
    by (simp add: wfP_def)
next
  show "⋀N C x xa xb xc xd. xd ∈ {D ∈ N. D ≺c C} ⟹ (({E ∈ N. E ≼c xd}, xd), N, C) ∈ {((x1, x2), y1, y2). x2 ≺c y2}"
    by simp
qed

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_lit (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_inside_gctxt RC)↓ ⊫ C ∧
      ¬ upair ` (rewrite_inside_gctxt (insert (x, y) RC))↓ ⊫ C' ∧
      x ∈ NF (rewrite_inside_gctxt 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.order.strict_trans1 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_lit (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_inside_gctxt RC)↓ ⊫ C ∧
      ¬ upair ` (rewrite_inside_gctxt (insert (x, y) RC))↓ ⊫ C' ∧
      x ∈ NF (rewrite_inside_gctxt 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.order.strict_trans1 mem_Collect_eq)
  qed

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

end

lemma (in ground_ordering) Uniq_striclty_maximal_lit_in_ground_cls:
  "∃≤1L. is_strictly_maximal_lit L C"
  using literal_order.Uniq_is_greatest_in_mset .

lemma (in ground_superposition_calculus) epsilon_eq_empty_or_singleton:
  "epsilon N C = {} ∨ (∃s t. epsilon N C = {(s, t)})"
proof -
  have "∃≤1 (x, y). ∃C'.
    C = add_mset (Pos (Upair x y)) C' ∧ is_strictly_maximal_lit (Pos (Upair x y)) C ∧ y ≺t x"
    by (rule Uniq_prodI)
      (metis Uniq_D Upair_inject literal_order.Uniq_is_greatest_in_mset term_order.min.absorb3
        term_order.min.absorb4 literal.inject(1))
  hence Uniq_epsilon: "∃≤1 (x, y). ∃C'.
    C ∈ N ∧
    C = add_mset (Pos (Upair x y)) C' ∧ select C = {#} ∧
    is_strictly_maximal_lit (Pos (Upair x y)) C ∧ y ≺t x ∧
    (let RC = ⋃D ∈ {D ∈ N. D ≺c C}. epsilon {E ∈ N. E ≼c D} D in
      ¬ upair ` (rewrite_inside_gctxt RC)↓ ⊫ C ∧
      ¬ upair ` (rewrite_inside_gctxt (insert (x, y) RC))↓ ⊫ C' ∧
      x ∈ NF (rewrite_inside_gctxt 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 (in ground_superposition_calculus) card_epsilon_le_one:
  "card (epsilon N C) ≤ 1"
  using epsilon_eq_empty_or_singleton[of N C]
  by auto

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

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

lemma (in ground_superposition_calculus) 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 (in ground_superposition_calculus) 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_lit (Pos (Upair l r)) C" and
    "r ≺t l" and
    "¬ upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫ C" and
    "¬ upair ` (rewrite_inside_gctxt (insert (l, r) (rewrite_sys N C)))↓ ⊫ C'" and
    "l ∈ NF (rewrite_inside_gctxt (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 (in ground_superposition_calculus) mem_epsilon_iff:
  "(l, r) ∈ epsilon N C ⟷
    (∃C'. C ∈ N ∧ C = add_mset (Pos (Upair l r)) C' ∧ select C = {#} ∧
      is_strictly_maximal_lit (Pos (Upair l r)) C ∧ r ≺t l ∧
      ¬ upair ` (rewrite_inside_gctxt (rewrite_sys' {D ∈ N. D ≺c C}))↓ ⊫ C ∧
      ¬ upair ` (rewrite_inside_gctxt (insert (l, r) (rewrite_sys' {D ∈ N. D ≺c C})))↓ ⊫ C' ∧
      l ∈ NF (rewrite_inside_gctxt (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 (in ground_superposition_calculus) 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 (in ground_superposition_calculus) rhs_less_trm_lhs_if_mem_rewrite_inside_gctxt_rewrite_sys:
  assumes rule_in: "(t1, t2) ∈ rewrite_inside_gctxt (rewrite_sys N C)"
  shows "t2 ≺t t1"
proof -
  from rule_in obtain ctxt t1' t2' where
    "(t1, t2) = (ctxt⟨t1'⟩G, ctxt⟨t2'⟩G) ∧ (t1', t2') ∈ rewrite_sys N C"
    unfolding rewrite_inside_gctxt_def mem_Collect_eq
    by auto
  thus ?thesis
  using rhs_lt_lhs_if_mem_rewrite_sys[of t1' t2']
  by (metis Pair_inject less_trm_compatible_with_gctxt)
qed

lemma (in ground_superposition_calculus) rhs_lesseq_trm_lhs_if_mem_rtrancl_rewrite_inside_gctxt_rewrite_sys:
  assumes rule_in: "(t1, t2) ∈ (rewrite_inside_gctxt (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 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 (in ground_superposition_calculus) 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 (in ground_superposition_calculus) 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 (in ground_superposition_calculus) 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_lit (Pos (Upair s t)) C" and
    "t ≺t s" and
    s_irreducible: "s ∈ NF (rewrite_inside_gctxt (rewrite_sys N C))"
    by (auto elim!: mem_epsilonE)
  hence "∀L ∈# C'. L ≺l Pos (Upair s t)"
    by (simp add: literal_order.is_greatest_in_mset_iff)

  from ED obtain D' where
    "D ∈ N" and
    D_def: "D = add_mset (Pos (Upair u v)) D'" and
    "is_strictly_maximal_lit (Pos (Upair 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 (simp add: literal_order.is_greatest_in_mset_iff)

  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 "Pos (Upair u v) ≺l Pos (Upair s t)"
      by (simp add: less_lit_def)
    moreover hence "∀L ∈# D'. L ≺l Pos (Upair s t)"
      using ‹∀L ∈# D'. L ≺l Pos (Upair u v)›
      by (meson literal_order.transp_on_less transpD)
    ultimately show "D ≺c C"
      using one_step_implies_multp[of C D _ "{#}"] less_cls_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_inside_gctxt (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: less_lit_def)
      moreover hence "∀L ∈# C'. L ≺l Pos (Upair u v)"
        using ‹∀L ∈# C'. L ≺l Pos (Upair s t)›
        by (meson literal_order.transp_on_less transpD)
      ultimately have "C ≺c D"
        using one_step_implies_multp[of D C _ "{#}"] less_cls_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 (in ground_superposition_calculus) termination_rewrite_sys: "wf ((rewrite_sys N C)¯)"
proof (rule wf_if_convertible_to_wf)
  show "wf {(x, y). x ≺t y}"
    using wfP_less_trm
    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 (in ground_superposition_calculus) 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 wfP_less_trm
    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 (in ground_superposition_calculus) 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 ctxt l r1 r2 where
    "(ctxt⟨r2⟩G, r1) ∈ ground_critical_pairs (⋃ (epsilon N2 ` N))" and
    "ctxt⟨r2⟩G ≠ r1" and
    rule1_in: "(ctxt⟨l⟩G, 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': "(ctxt⟨l⟩G, 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 ctxt⟨l⟩G r1)) C1'" and
    C1_max: "is_strictly_maximal_lit (Pos (Upair ctxt⟨l⟩G r1)) C1" and
    "r1 ≺t ctxt⟨l⟩G" and
    l1_irreducible: "ctxt⟨l⟩G ∈ NF (rewrite_inside_gctxt (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_lit (Pos (Upair l r2)) C2" and
    "r2 ≺t l"
    by (auto elim: mem_epsilonE)

  have "epsilon N2 C1 = {(ctxt⟨l⟩G, r1)}"
    using rule1_in' epsilon_eq_empty_or_singleton by fastforce

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

  show False
  proof (cases "ctxt = □G")
    case True
    hence "¬ (ctxt⟨l⟩G ≺t l)" and "¬ (l ≺t ctxt⟨l⟩G)"
      by (simp_all add: irreflpD)
    hence "¬ (C1 ≺c C2)" and "¬ (C2 ≺c C1)"
      using ‹epsilon N2 C1 = {(ctxt⟨l⟩G, 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 = {(ctxt⟨l⟩G, r1)}› ‹epsilon N2 C2 = {(l, r2)}› by simp
    moreover have "r1 ≠ r2"
      using ‹ctxt⟨r2⟩G ≠ r1›
      unfolding ‹ctxt = □G›
      by simp
    ultimately show ?thesis
      by contradiction
  next
    case False
    hence "l ≺t ctxt⟨l⟩G"
      by (metis less_trm_if_subterm)
    hence "C2 ≺c C1"
      using ‹epsilon N2 C1 = {(ctxt⟨l⟩G, r1)}› ‹epsilon N2 C2 = {(l, r2)}›
        less_trm_iff_less_cls_if_lhs_epsilon
      by simp
    have "(l, r2) ∈ rewrite_sys N2 C1"
      by (metis ‹C2 ≺c C1› ‹epsilon N2 C2 = {(l, r2)}› mem_epsilonE mem_rewrite_sys_if_less_cls
          singletonI)
    hence "(ctxt⟨l⟩G, ctxt⟨r2⟩G) ∈ rewrite_inside_gctxt (rewrite_sys N2 C1)"
      by auto
    thus False
      using l1_irreducible by auto
  qed
qed

lemma (in ground_superposition_calculus) WCR_Union_rewrite_sys:
  "WCR (rewrite_inside_gctxt (⋃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))"
  then obtain t1 t2 where tuple_def: "tuple = (t1, t2)"
    by fastforce

  moreover have "(t1, t2) ∈ (rewrite_inside_gctxt (⋃ (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_inside_gctxt (⋃ (epsilon N2 ` N)))↓"
    by (cases "t1 = t2") simp_all
qed

lemma (in ground_superposition_calculus)
  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_lit (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 transp_less_trm union_mset_add_mset_right)
    with that(1) show "Pos (Upair s t) ≺l L"
      using topmost_trms_of_L
      by (cases L) (simp_all add: less_lit_def)
  qed

  moreover have "Pos (Upair s t) ≺l L" if "is_neg L" and "¬ u ≺t s"
  proof -
    from that(2) have "s ≼t u"
      by order
    hence "multp (≺t) {#s, t#} {#u, v, u, v#}"
      using ‹t ≺t s›
      by (smt (z3) add_mset_add_single add_mset_remove_trivial add_mset_remove_trivial_iff
          empty_not_add_mset insert_DiffM insert_noteq_member one_step_implies_multp reflclp_iff
          transp_def transp_less_trm union_mset_add_mset_left union_mset_add_mset_right)
    with that(1) show "Pos (Upair s t) ≺l L"
      using topmost_trms_of_L
      by (cases L) (simp_all add: less_lit_def)
  qed

  moreover have False if "Pos (Upair s t) ≺l L"
  proof -
    have "C ≺c D"
      unfolding less_cls_def
    proof (rule multp_if_maximal_of_lhs_is_less)
      show "Pos (Upair s t) ∈# C"
        by (simp add: C_def)
    next
      show "L ∈# D"
        using L_in by simp
    next
      show "is_maximal_lit (Pos (Upair s t)) C"
        using C_max_lit by auto
    next
      show "Pos (Upair 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 (in ground_ordering) less_trm_const_lhs_if_mem_rewrite_inside_gctxt:
  fixes t t1 t2 r
  assumes
    rule_in: "(t1, t2) ∈ rewrite_inside_gctxt r" and
    ball_lt_lhs: "⋀t1 t2. (t1, t2) ∈ r ⟹ t ≺t t1"
  shows "t ≺t t1"
proof -
  from rule_in obtain ctxt t1' t2' where
    rule_in': "(t1', t2') ∈ r" and
    l_def: "t1 = ctxt⟨t1'⟩G" and
    r_def: "t2 = ctxt⟨t2'⟩G"
    unfolding rewrite_inside_gctxt_def by fast

  show ?thesis
    using ball_lt_lhs[OF rule_in'] lesseq_trm_if_subtermeq[of t1' ctxt] l_def by order
qed

lemma (in ground_superposition_calculus) 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 (in ground_superposition_calculus) 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 (in ground_superposition_calculus) 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.transp_on_less
    by (metis (no_types, opaque_lifting) transpD)
  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 (in ground_ordering) 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 transp_less_trm)
  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_ordering) 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_ordering) 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

lemma (in ground_superposition_calculus) lift_entailment_to_Union:
  fixes N D
  defines "RD ≡ rewrite_sys N D"
  assumes
    D_in: "D ∈ N" and
    RD_entails_D: "upair ` (rewrite_inside_gctxt RD)↓ ⊫ D"
  shows
    "upair ` (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓ ⊫ D" and
    "⋀C. C ∈ N ⟹ D ≺c C ⟹ upair ` (rewrite_inside_gctxt (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_inside_gctxt RD)↓ ∨
     L = Neg (Upair s t) ∧ (s, t) ∉ (rewrite_inside_gctxt 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_inside_gctxt (⋃D ∈ N. epsilon N D))↓ ⊫ D" and
    "⋀C. C ∈ N ⟹ D ≺c C ⟹ upair ` (rewrite_inside_gctxt (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_inside_gctxt 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_inside_gctxt RD ⊆ rewrite_inside_gctxt (⋃D ∈ N. epsilon N D)" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ rewrite_inside_gctxt RD ⊆ rewrite_inside_gctxt (rewrite_sys N C)"
      by (auto intro!: rewrite_inside_gctxt_mono)
    hence "(s, t) ∈ (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ (s, t) ∈ (rewrite_inside_gctxt (rewrite_sys N C))↓"
      by (auto intro!: join_mono intro: set_mp[OF _ ‹(s, t) ∈ (rewrite_inside_gctxt RD)↓›])
    thus "upair ` (rewrite_inside_gctxt (⋃ (epsilon N ` N)))↓ ⊫ D ∧
      (∀C. C ∈ N ⟶ D ≺c C ⟶ upair ` (rewrite_inside_gctxt (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_inside_gctxt RD ⟹ t2 ≺t t1" for t1 t2
      by (smt (verit, ccfv_SIG) Pair_inject less_trm_compatible_with_gctxt mem_Collect_eq
          rewrite_inside_gctxt_def)

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

    have "(s, t) ∈ (rewrite_inside_gctxt RD ∪ rewrite_inside_gctxt (⋃C ∈ {C ∈ N. D ≼c C}. epsilon N C))↓ ⟷
      (s, t) ∈ (rewrite_inside_gctxt RD)↓"
    proof (rule mem_join_union_iff_mem_join_lhs')
      show "⋀t1 t2. (t1, t2) ∈ rewrite_inside_gctxt 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_inside_gctxt (⋃ (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_inside_gctxt RD ∪ rewrite_inside_gctxt (⋃C' ∈ {C' ∈ N. D ≼c C' ∧ C' ≺c C}. epsilon N C'))↓ ⟷
       (s, t) ∈ (rewrite_inside_gctxt 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_inside_gctxt 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 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_inside_gctxt (⋃ (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_inside_gctxt RD ∪ rewrite_inside_gctxt (⋃C ∈ {C ∈ N. D ≼c C}. epsilon N C))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶
        (s, t) ∉ (rewrite_inside_gctxt RD ∪ rewrite_inside_gctxt (⋃C' ∈ {C' ∈ N. D ≼c C' ∧ C' ≺c C}. epsilon N C'))↓"
      using ‹(s, t) ∉ (rewrite_inside_gctxt RD)↓› by simp_all
    hence "(s, t) ∉ (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ (s, t) ∉ (rewrite_inside_gctxt (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_inside_gctxt_union)
    hence "(Upair s t) ∉ upair ` (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓" and
      "∀C. C ∈ N ⟶ D ≺c C ⟶ (Upair s t) ∉ upair ` (rewrite_inside_gctxt (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_inside_gctxt (⋃ (epsilon N ` N)))↓ ⊫ D ∧
    (∀C. C ∈ N ⟶ D ≺c C ⟶ upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫ D)"
      unfolding true_cls_def true_lit_iff
      using L_in L_def by metis
  qed
qed

lemma (in ground_superposition_calculus)
  assumes productive: "epsilon N C = {(l, r)}"
  shows
    true_cls_if_productive_epsilon:
      "upair ` (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓ ⊫ C"
      "⋀D. D ∈ N ⟹ C ≺c D ⟹ upair ` (rewrite_inside_gctxt (rewrite_sys N D))↓ ⊫ C" and
    false_cls_if_productive_epsilon:
      "¬ upair ` (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓ ⊫ C - {#Pos (Upair l r)#}"
      "⋀D. D ∈ N ⟹ C ≺c D ⟹ ¬ upair ` (rewrite_inside_gctxt (rewrite_sys N D))↓ ⊫ C - {#Pos (Upair 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 (Pos (Upair l r)) C'" and
    "select C = {#}" and
    "is_strictly_maximal_lit (Pos (Upair l r)) C" and
    "r ≺t l" and
    e: "¬ upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫ C" and
    f: "¬ upair ` (rewrite_inside_gctxt (insert (l, r) (rewrite_sys N C)))↓ ⊫ C'" and
    "l ∈ NF (rewrite_inside_gctxt (rewrite_sys N C))"
    by (rule mem_epsilonE) blast

  have "(l, r) ∈ (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓"
    using C_in ‹(l, r) ∈ epsilon N C› mem_rewrite_inside_gctxt_if_mem_rewrite_rules by blast
  thus "upair ` (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓ ⊫ C"
    using C_def by blast

  have "rewrite_inside_gctxt (⋃D ∈ N. epsilon N D) =
        rewrite_inside_gctxt (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_inside_gctxt (rewrite_sys N C ∪ epsilon N C) ∪
    rewrite_inside_gctxt (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D)"
    by (simp add: rewrite_inside_gctxt_union)
  finally have rewrite_inside_gctxt_Union_epsilon_eq:
    "rewrite_inside_gctxt (⋃D ∈ N. epsilon N D) =
      rewrite_inside_gctxt (insert (l, r) (rewrite_sys N C)) ∪
      rewrite_inside_gctxt (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D)"
    unfolding productive by simp

  have mem_join_union_iff_mem_lhs:"(t1, t2) ∈ (rewrite_inside_gctxt (insert (l, r) (rewrite_sys N C)) ∪
    rewrite_inside_gctxt (⋃D ∈ {D ∈ N. C ≺c D}. epsilon N D))↓ ⟷
    (t1, t2) ∈ (rewrite_inside_gctxt (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_inside_gctxt (insert (l, r) (rewrite_sys N C))"

    moreover have "s2 ≺t s1" if "(s1, s2) ∈ rewrite_inside_gctxt {(l, r)}"
    proof (rule rhs_lt_lhs_if_rule_in_rewrite_inside_gctxt[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_inside_gctxt (rewrite_sys N C)"
    proof (rule rhs_lt_lhs_if_rule_in_rewrite_inside_gctxt[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_inside_gctxt_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 transp_less_trm)
    qed
    thus "⋀l r. (l, r) ∈ rewrite_inside_gctxt (⋃ (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_inside_gctxt (⋃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_inside_gctxt (⋃D ∈ N. epsilon N D))↓" if L_def: "L = Pos (Upair t1 t2)"
    proof -
      from that have "(t1, t2) ∉ (rewrite_inside_gctxt (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_inside_gctxt (⋃D ∈ N. epsilon N D))↓"
      if L_def: "L = Neg (Upair t1 t2)"
    proof -
      from that have "(t1, t2) ∈ (rewrite_inside_gctxt (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_inside_gctxt (⋃ (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_inside_gctxt (⋃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 metis
  hence "(l, r) ∈ (rewrite_inside_gctxt (rewrite_sys N D))↓"
    by auto
  thus "upair ` (rewrite_inside_gctxt (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_inside_gctxt (rewrite_sys N D) ⊆ rewrite_inside_gctxt (⋃D ∈ N. epsilon N D)"
    using rewrite_inside_gctxt_mono by metis
  hence "(rewrite_inside_gctxt (rewrite_sys N D))↓ ⊆ (rewrite_inside_gctxt (⋃D ∈ N. epsilon N D))↓"
    using join_mono by metis

  have "¬ upair ` (rewrite_inside_gctxt (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_inside_gctxt (rewrite_sys N D))↓" if L_def: "L = Pos (Upair t1 t2)"
    proof -
      from that have "(t1, t2) ∉ (rewrite_inside_gctxt (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_inside_gctxt (rewrite_sys N D))↓ ⊆ (rewrite_inside_gctxt (⋃ (epsilon N ` N)))↓› by auto
    qed

    moreover have "(t1, t2) ∈ (rewrite_inside_gctxt (rewrite_sys N D))↓" if L_def: "L = Neg (Upair t1 t2)"
      using e
    proof (rule contrapos_np)
      assume "(t1, t2) ∉ (rewrite_inside_gctxt (rewrite_sys N D))↓"
      hence "(t1, t2) ∉ (rewrite_inside_gctxt (rewrite_sys N C))↓"
        using rewrite_sys_subset_if_less_cls[OF ‹C ≺c D›]
        by (meson join_mono rewrite_inside_gctxt_mono subsetD)
      thus "upair ` (rewrite_inside_gctxt (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_inside_gctxt (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_inside_gctxt (rewrite_sys N D))↓ ⊫ C - {#Pos (Upair l r)#}"
    by (simp add: C_def)
qed

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_superposition_calculus) trans_join_rewrite_inside_gctxt_rewrite_sys:
  "trans ((rewrite_inside_gctxt (rewrite_sys N C))↓)"
proof (rule trans_join)
  have "wf ((rewrite_inside_gctxt (rewrite_sys N C))¯)"
  proof (rule wf_converse_rewrite_inside_gctxt)
    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_inside_gctxt (rewrite_sys N C))"
    by (simp only: SN_iff_wf)
next
  show "WCR (rewrite_inside_gctxt (rewrite_sys N C))"
    unfolding rewrite_sys_def epsilon_filter_le_conv
    using WCR_Union_rewrite_sys
    by (metis (mono_tags, lifting))
qed

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

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

  have "totalp_on (set_uprod (atm_of L)) (≺t)"
    using totalp_less_trm totalp_on_subset by blast
  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 = Pos (Upair t t')"
      using ‹atm_of L = Upair t t'› by simp

    moreover have "(t, t') ∈ (rewrite_inside_gctxt (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_inside_gctxt 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_inside_gctxt (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_inside_gctxt 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_inside_gctxt R)↓ ⊆ (rewrite_inside_gctxt (insert r R))↓"
      using join_mono rewrite_inside_gctxt_mono
      by (metis subset_insertI)

    ultimately have False
      by auto
    thus ?thesis ..
  qed
qed

lemma (in ground_superposition_calculus) model_preconstruction:
  fixes
    N :: "'f gatom clause set" and
    C :: "'f gatom clause"
  defines
    "entails ≡ λE C. upair ` (rewrite_inside_gctxt 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 wfP_less_cls 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_inside_gctxt (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_gctxt I"
    by (simp only: I_def compatible_with_gctxt_join compatible_with_gctxt_rewrite_inside_gctxt)

  note I_interp = ‹refl I› ‹trans I› ‹sym I› ‹compatible_with_gctxt 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_lit L C ∧ is_neg L)) ⟷
      (∃A. Neg A ∈# C ∧ (Neg A ∈# select C ∨ select C = {#} ∧ is_maximal_lit (Neg A) C))"
      by (metis (no_types, opaque_lifting) is_pos_def literal_order.is_maximal_in_mset_iff
          literal.disc(2) literal.exhaust mset_subset_eqD select_negative_lits select_subset)

    show "entails (rewrite_sys N C) C"
    proof (cases "∃L. is_maximal_lit L (select C) ∨ (select C = {#} ∧ is_maximal_lit L C ∧ is_neg L)")
      case ex_neg_lit_sel_or_max: True
      hence "∃A. Neg A ∈# C ∧ (is_maximal_lit (Neg A) (select C) ∨ select C = {#} ∧ is_maximal_lit (Neg A) C)"
        by (metis is_pos_def literal.exhaust literal_order.is_maximal_in_mset_iff mset_subset_eqD
            select_negative_lits select_subset)
      then obtain s s' where
        "Neg (Upair s s') ∈# C" and
        sel_or_max: "select C = {#} ∧ is_maximal_lit (Neg (Upair s s')) C ∨ is_maximal_lit (Neg (Upair s s')) (select C)"
        by (metis uprod_exhaust)
      then obtain C' where
        C_def: "C = add_mset (Neg (Upair s s')) C'"
        by (metis mset_add)

      show ?thesis
      proof (cases "upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫l Pos (Upair s s')")
        case True
        hence "(s, s') ∈ (rewrite_inside_gctxt (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"
          using totalp_less_trm
          by (metis totalpD)
        thus ?thesis
        proof (rule disjE)
          assume "s = s'"
          define ι :: "'f gatom clause inference" where
            "ι = Infer [C] C'"

          have "ground_eq_resolution C C'"
          proof (rule ground_eq_resolutionI)
            show "C = add_mset (Neg (Upair s s')) C'"
              by (simp only: C_def)
          next
            show "Neg (Upair s s') = Neg (Upair s s)"
              by (simp only: ‹s = s'›)
          next
            show "select C = {#} ∧ is_maximal_lit (s !≈ s') C ∨ is_maximal_lit (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_inside_gctxt (rewrite_sys N C))↓› obtain u where
            s_u: "(s, u) ∈ (rewrite_inside_gctxt (rewrite_sys N C))*" and
            s'_u: "(s', u) ∈ (rewrite_inside_gctxt (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_inside_gctxt (rewrite_sys N C)"
            "s ≺t s' ⟹ (s', u0) : rewrite_inside_gctxt (rewrite_sys N C)" and
            "(u0, u) : (rewrite_inside_gctxt (rewrite_sys N C))*"
            using ex_step_if_joinable[OF _ s_u s'_u]
            by (metis asympD asymp_less_trm)
          then obtain ctxt t t' where
            s_eq_if: "s' ≺t s ⟹ s = ctxt⟨t⟩G" and
            s'_eq_if: "s ≺t s' ⟹ s' = ctxt⟨t⟩G" and
            "u0 = ctxt⟨t'⟩G" and
            "(t, t') ∈ rewrite_sys N C"
            by (smt (verit) Pair_inject ‹s ≺t s' ∨ s' ≺t s› asympD asymp_less_trm mem_Collect_eq
                rewrite_inside_gctxt_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_lit (Pos (Upair t t')) D" and
            "t' ≺t t"
            by (elim mem_epsilonE) fast

          have superI: "ground_neg_superposition D C (add_mset (Neg (Upair s1⟨t'⟩G s1')) (C' + D'))"
            if "{s, s'} = {s1⟨t⟩G, s1'}" and "s1' ≺t s1⟨t⟩G"
            for s1 s1'
          proof (rule ground_neg_superpositionI)
            show "C = add_mset (Neg (Upair s s')) C'"
              by (simp only: C_def)
          next
            show "D = add_mset (Pos (Upair t t')) D'"
              by (simp only: D_def)
          next
            show "D ≺c C"
              using ‹D ≺c C› .
          next
            show "select C = {#} ∧ is_maximal_lit (Neg (Upair s s')) C ∨ is_maximal_lit (s !≈ s') (select C)"
              using sel_or_max .
          next
            show "select D = {#}"
              using sel_D .
          next
            show "is_strictly_maximal_lit (Pos (Upair t t')) D"
              using max_t_t' .
          next
            show "t' ≺t t"
              using ‹t' ≺t t› .
          next
            from that(1) show "Neg (Upair s s') = Neg (Upair s1⟨t⟩G s1')"
              by fastforce
          next
            from that(2) show "s1' ≺t s1⟨t⟩G" .
          qed simp_all

          have "ground_neg_superposition D C (add_mset (Neg (Upair ctxt⟨t'⟩G s')) (C' + D'))"
            if ‹s' ≺t s›
          proof (rule superI)
            from that show "{s, s'} = {ctxt⟨t⟩G, s'}"
              using s_eq_if by simp
          next
            from that show "s' ≺t ctxt⟨t⟩G"
              using s_eq_if by simp
          qed

          moreover have "ground_neg_superposition D C (add_mset (Neg (Upair ctxt⟨t'⟩G s)) (C' + D'))"
            if ‹s ≺t s'›
          proof (rule superI)
            from that show "{s, s'} = {ctxt⟨t⟩G, s}"
              using s'_eq_if by auto
          next
            from that show "s ≺t ctxt⟨t⟩G"
              using s'_eq_if by simp
          qed

          ultimately obtain CD where
            super: "ground_neg_superposition D C CD" and
            CD_eq1: "s' ≺t s ⟹ CD = add_mset (Neg (Upair ctxt⟨t'⟩G s')) (C' + D')" and
            CD_eq2: "s ≺t s' ⟹ CD = add_mset (Neg (Upair ctxt⟨t'⟩G s)) (C' + D')"
            using ‹s ≺t s' ∨ s' ≺t s› s'_eq_if s_eq_if by metis

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

          have "ι ∈ G_Inf"
            using ground_superposition_if_ground_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 (metis in_mono insert_iff)

          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_inside_gctxt (rewrite_sys N C))↓ ⊫l
            (Neg (Upair ctxt⟨t'⟩G s'))"
            if "s' ≺t s"
            using ‹(u0, u) ∈ (rewrite_inside_gctxt (rewrite_sys N C))*› ‹u0 = ctxt⟨t'⟩G› s'_u by blast

          moreover have "¬ upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫l
            (Neg (Upair ctxt⟨t'⟩G s))"
            if "s ≺t s'"
            using ‹(u0, u) ∈ (rewrite_inside_gctxt (rewrite_sys N C))*› ‹u0 = ctxt⟨t'⟩G› 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_lit (Pos A) C"
        using ‹select C = {#}› literal_order.ex_maximal_in_mset[OF ‹C ≠ {#}›]
        by (metis is_pos_def literal_order.is_maximal_in_mset_iff)
      then obtain C' where C_def: "C = add_mset (Pos A) C'"
        by (meson mset_add)

      have "totalp_on (set_uprod A) (≺t)"
        using totalp_less_trm totalp_on_subset by blast
      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_inside_gctxt (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_inside_gctxt (rewrite_sys N C))↓ ⊫ C'"
          by simp

        from False have "s' ≺t s"
          using ‹s' ≼t s› asymp_less_trm[THEN asympD] by auto

        then show ?thesis
        proof (cases "is_strictly_maximal_lit (Pos A) C")
          case strictly_maximal: True
          show ?thesis
          proof (cases "s ∈ NF (rewrite_inside_gctxt (rewrite_sys N C))")
            case s_irreducible: True
            hence e_or_f_doesnt_hold: "upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫ C ∨
              upair ` (rewrite_inside_gctxt (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_inside_gctxt (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_inside_gctxt (rewrite_sys N C))↓ ⊫ C'"
                unfolding C_def by simp
              show ?thesis
              proof (cases "upair ` (rewrite_inside_gctxt (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_inside_gctxt (insert (s, s') (rewrite_sys N C)))↓" and
                  "(t, t') ∉ (rewrite_inside_gctxt (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
                  by (simp add: A_def C'_def C_def literal_order.is_greatest_in_mset_iff)

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

                  have "(t, t') ∈ (rewrite_inside_gctxt (insert (s, s') (rewrite_sys N C)))↓ ⟷
                    (t, t') ∈ (rewrite_inside_gctxt (rewrite_sys N C))↓"
                    unfolding rewrite_inside_gctxt_union[of "{(s, s')}" "rewrite_sys N C", simplified]
                  proof (rule mem_join_union_iff_mem_join_rhs')
                    show "⋀t1 t2. (t1, t2) ∈ rewrite_inside_gctxt {(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 transp_less_trm)
                  next
                    show "⋀t1 t2. (t1, t2) ∈ rewrite_inside_gctxt (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_inside_gctxt (insert (s, s') (rewrite_sys N C)))↓›
                    using ‹(t, t') ∉ (rewrite_inside_gctxt (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 transp_less_trm)
                  hence "Pos (Upair s s') ≺l Pos (Upair t t')"
                    by (simp add: less_lit_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 less_lit_def
                  by (simp add: multp_cancel_add_mset transp_less_trm)

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

                have "t'' ≺t t"
                proof (rule predicate_holds_of_mem_rewrite_inside_gctxt[of _ _ _ "λx y. y ≺t x"])
                  show "(t, t'') ∈ rewrite_inside_gctxt (insert (s, s') (rewrite_sys N C))"
                    using ‹(t, t'') ∈ rewrite_inside_gctxt (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 ctxt σ. (t1, t2) ∈ insert (s, s') (rewrite_sys N C) ⟹
                    t2 ≺t t1 ⟹ ctxt⟨t2⟩G ≺t ctxt⟨t1⟩G"
                    by (simp only: less_trm_compatible_with_gctxt)
                qed

                have "(t, t'') ∈ rewrite_inside_gctxt {(s, s')}"
                  using ‹(t, t'') ∈ rewrite_inside_gctxt (insert (s, s') (rewrite_sys N C))›
                  using ‹t = s› s_irreducible mem_rewrite_step_union_NF
                  using rewrite_inside_gctxt_insert by blast
                hence "∃ctxt. s = ctxt⟨s⟩G ∧ t'' = ctxt⟨s'⟩G"
                  by (simp add: ‹t = s› rewrite_inside_gctxt_def)
                hence "t'' = s'"
                  by (metis gctxt_ident_iff_eq_GHole)

                moreover have "(t'', t') ∈ (rewrite_inside_gctxt (rewrite_sys N C))↓"
                proof (rule mem_join_union_iff_mem_join_rhs'[THEN iffD1])
                  show "(t'', t') ∈ (rewrite_inside_gctxt {(s, s')} ∪
                    rewrite_inside_gctxt (rewrite_sys N C))↓"
                    using ‹(t'', t') ∈ (rewrite_inside_gctxt (insert (s, s') (rewrite_sys N C)))↓›
                    using rewrite_inside_gctxt_union[of "{_}", simplified] by metis
                next
                  show "⋀t1 t2. (t1, t2) ∈ rewrite_inside_gctxt (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_inside_gctxt {(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_inside_gctxt (rewrite_sys N C))↓"
                  by simp

                let ?concl = "add_mset (Neg (Upair s' t')) (add_mset (Pos (Upair t t')) C'')"

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

                have eq_fact: "ground_eq_factoring C ?concl"
                proof (rule ground_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_lit (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 (Neg (Upair s' t')) (add_mset (Pos (Upair t t')) C'') =
                    add_mset (Neg (Upair s' t')) (add_mset (Pos (Upair 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_inside_gctxt (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_inside_gctxt (rewrite_sys N C)"
              unfolding NF_def by auto
            then obtain ctxt t t' D where
              "D ∈ N" and
              "D ≺c C" and
              "(t, t') ∈ epsilon N D" and
              "s = ctxt⟨t⟩G"
              using epsilon_filter_le_conv
              by (auto simp: rewrite_inside_gctxt_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_lit (t ≈ t') D" and
              "t' ≺t t"
              using ‹(t, t') ∈ epsilon N D›
              by (elim mem_epsilonE) simp

            let ?concl = "add_mset (Pos (Upair ctxt⟨t'⟩G s')) (C' + D')"

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

            have super: "ground_pos_superposition D C ?concl"
            proof (rule ground_pos_superpositionI)
              show "C = add_mset (Pos (Upair s s')) C'"
                by (simp only: C_def A_def)
            next
              show "D = add_mset (Pos (Upair 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_lit (s ≈ s') C"
                using A_def strictly_maximal by simp
            next
              show "is_strictly_maximal_lit (t ≈ t') D"
                using max_t_t' .
            next
              show "t' ≺t t"
                using ‹t' ≺t t› .
            next
              show "Pos (Upair s s') = Pos (Upair ctxt⟨t⟩G s')"
                by (simp only: ‹s = ctxt⟨t⟩G›)
            next
              show "s' ≺t ctxt⟨t⟩G"
                using ‹s' ≺t s›
                unfolding ‹s = ctxt⟨t⟩G› .
            qed simp_all
            hence "ι ∈ G_Inf"
              using ground_superposition_if_ground_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 (metis in_mono insert_iff)

            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) {#Pos (Upair ctxt⟨t'⟩G s')#}"
              unfolding entails_def
              using ‹¬ upair ` (rewrite_inside_gctxt (rewrite_sys N C))↓ ⊫ C'›
              by fastforce

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

            moreover have "(ctxt⟨t⟩G, ctxt⟨t'⟩G) ∈ rewrite_inside_gctxt (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_inside_gctxt_def)

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

            hence "entails (rewrite_sys N C) {#Pos (Upair ctxt⟨t⟩G s')#}"
              unfolding entails_def true_cls_def by auto

            thus ?thesis
              using A_def C_def ‹s = ctxt⟨t⟩G› entails_def by fastforce
          qed
        next
          case False
          hence "2 ≤ count C (Pos A)"
            using max_Pos_A
            by (metis literal_order.count_ge_2_if_maximal_in_mset_and_not_greatest_in_mset)
          then obtain C' where C_def: "C = add_mset (Pos A) (add_mset (Pos A) C')"
            using two_le_countE by metis

          define ι :: "'f gatom clause inference" where
            "ι = Infer [C] (add_mset (Pos (Upair s s')) (add_mset (Neg (Upair s' s')) C'))"

          let ?concl = "add_mset (Pos (Upair s s')) (add_mset (Neg (Upair s' s')) C')"

          have eq_fact: "ground_eq_factoring C ?concl"
          proof (rule ground_eq_factoringI)
            show "C = add_mset (Pos A) (add_mset (Pos A) C')"
              by (simp add: C_def)
          next
            show "Pos A = Pos (Upair s s')"
              by (simp add: A_def)
          next
            show "Pos A = Pos (Upair s s')"
              by (simp add: A_def)
          next
            show "select C = {#}"
              using ‹select C = {#}› .
          next
            show "is_maximal_lit (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 metis
qed

lemma (in ground_superposition_calculus) model_construction:
  fixes
    N :: "'f gatom clause set" and
    C :: "'f gatom clause"
  defines
    "entails ≡ λE C. upair ` (rewrite_inside_gctxt 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 (in ground_superposition_calculus) statically_complete:
  fixes N :: "'f gatom clause set"
  assumes "saturated N" and "G_entails N {{#}}"
  shows "{#} ∈ N"
  using ‹G_entails N {{#}}›
proof (rule contrapos_pp)
  assume "{#} ∉ N"

  define I :: "'f gterm rel" where
    "I = (rewrite_inside_gctxt (⋃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_inside_gctxt (⋃D ∈ N. epsilon N D))¯)"
      proof (rule wf_converse_rewrite_inside_gctxt)
        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_inside_gctxt (⋃D ∈ N. epsilon N D))"
        unfolding SN_iff_wf .
    next
      show "WCR (rewrite_inside_gctxt (⋃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_gctxt I"
      unfolding I_def
      by (simp only: I_def compatible_with_gctxt_join compatible_with_gctxt_rewrite_inside_gctxt)
  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 ground_superposition_calculus ⊆ 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
proof unfold_locales
  fix B :: "'f gatom clause" and N :: "'f gatom clause set"
  assume "B ∈ G_Bot" and "saturated N"
  hence "B = {#}"
    by simp

  assume "G_entails N {B}"
  hence "{#} ∈ N"
    unfolding ‹B = {#}›
    using statically_complete[OF ‹saturated N›] by argo
  thus "∃B'∈G_Bot. B' ∈ N"
    by auto
qed

end