Theory Otter_Loop

(* Title:        Otter Loop
   Authors:      Qi Qiu, 2021
                 Jasmin Blanchette <j.c.blanchette at vu.nl>, 2022-2023
   Maintainer:   Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹Otter Loop›

text ‹The Otter loop is one of the two best-known given clause procedures. It is
formalized as an instance of the abstract procedure @{text GC}.›

theory Otter_Loop
  imports
    More_Given_Clause_Architectures
    Given_Clause_Loops_Util
begin

datatype OL_label =
  New | XX | Passive | YY | Active

primrec nat_of_OL_label :: "OL_label ⇒ nat" where
  "nat_of_OL_label New = 4"
| "nat_of_OL_label XX = 3"
| "nat_of_OL_label Passive = 2"
| "nat_of_OL_label YY = 1"
| "nat_of_OL_label Active = 0"

definition OL_Prec_L :: "OL_label ⇒ OL_label ⇒ bool" (infix "⊏L" 50) where
  "OL_Prec_L l l' ⟷ nat_of_OL_label l < nat_of_OL_label l'"

locale otter_loop = labeled_lifting_intersection Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q
  Red_F_q 𝒢_F_q 𝒢_I_q
  "{ι⇩F⇩L :: ('f × OL_label) inference. Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L)) ∈ Inf_F}"
  for
    Bot_F :: "'f set"
    and Inf_F :: "'f inference set"
    and Bot_G :: "'g set"
    and Q :: "'q set"
    and entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool"
    and Inf_G_q :: ‹'q ⇒ 'g inference set›
    and Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set"
    and Red_F_q :: "'q ⇒ 'g set ⇒ 'g set"
    and 𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set"
    and 𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option"
  + fixes
    Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix "≐" 50) and
    Prec_F :: "'f ⇒ 'f ⇒ bool" (infix "≺⋅" 50)
  assumes
    equiv_equiv_F: "equivp (≐)" and
    wf_prec_F: "minimal_element (≺⋅) UNIV" and
    compat_equiv_prec: "C1 ≐ D1 ⟹ C2 ≐ D2 ⟹ C1 ≺⋅ C2 ⟹ D1 ≺⋅ D2" and
    equiv_F_grounding: "q ∈ Q ⟹ C1 ≐ C2 ⟹ 𝒢_F_q q C1 ⊆ 𝒢_F_q q C2" and
    prec_F_grounding: "q ∈ Q ⟹ C2 ≺⋅ C1 ⟹ 𝒢_F_q q C1 ⊆ 𝒢_F_q q C2" and
    static_ref_comp: "statically_complete_calculus Bot_F Inf_F (⊨∩𝒢)
      no_labels.Red_I_𝒢 no_labels.Red_F_𝒢_empty" and
    inf_have_prems: "ιF ∈ Inf_F ⟹ prems_of ιF ≠ []"
begin

lemma po_on_OL_Prec_L: "po_on (⊏L) UNIV"
  by (metis (mono_tags, lifting) OL_Prec_L_def irreflp_onI less_imp_neq order.strict_trans po_on_def
      transp_onI)

lemma wfp_on_OL_Prec_L: "wfp_on (⊏L) UNIV"
  unfolding wfp_on_UNIV OL_Prec_L_def by (simp add: wfP_app)

lemma Active_minimal: "l2 ≠ Active ⟹ Active ⊏L l2"
  by (cases l2) (auto simp: OL_Prec_L_def)

lemma at_least_two_labels: "∃l2. Active ⊏L l2"
  using Active_minimal by blast

sublocale gc?: given_clause Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q Red_F_q 𝒢_F_q 𝒢_I_q
  Equiv_F Prec_F OL_Prec_L Active
  apply unfold_locales
             apply (rule equiv_equiv_F)
            apply (simp add: minimal_element.po wf_prec_F)
           using minimal_element.wf wf_prec_F apply blast
          apply (rule po_on_OL_Prec_L)
         apply (rule wfp_on_OL_Prec_L)
        apply (fact compat_equiv_prec)
       apply (fact equiv_F_grounding)
      apply (fact prec_F_grounding)
     apply (fact Active_minimal)
    apply (rule at_least_two_labels)
   using static_ref_comp statically_complete_calculus.statically_complete apply fastforce
  apply (fact inf_have_prems)
  done

notation gc.step (infix "↝GC" 50)


subsection ‹Basic Definitions and Lemmas›

fun state :: "'f set × 'f set × 'f set × 'f set × 'f set ⇒ ('f × OL_label) set" where
  "state (N, X, P, Y, A) =
   {(C, New) | C. C ∈ N} ∪ {(C, XX) | C. C ∈ X} ∪ {(C, Passive) | C. C ∈ P} ∪
   {(C, YY) | C. C ∈ Y} ∪ {(C, Active) | C. C ∈ A}"

lemma state_alt_def:
  "state (N, X, P, Y, A) =
   (λC. (C, New)) ` N ∪ (λC. (C, XX)) ` X ∪ (λC. (C, Passive)) ` P ∪ (λC. (C, YY)) ` Y ∪
   (λC. (C, Active)) ` A"
  by auto

inductive OL :: "('f × OL_label) set ⇒ ('f × OL_label) set ⇒ bool" (infix "↝OL" 50) where
  choose_n: "C ∉ N ⟹ state (N ∪ {C}, {}, P, {}, A) ↝OL state (N, {C}, P, {}, A)"
| delete_fwd: "C ∈ no_labels.Red_F (P ∪ A) ∨ (∃C' ∈ P ∪ A. C' ≼⋅ C) ⟹
    state (N, {C}, P, {}, A) ↝OL state (N, {}, P, {}, A)"
| simplify_fwd: "C ∈ no_labels.Red_F (P ∪ A ∪ {C'}) ⟹
    state (N, {C}, P, {}, A) ↝OL state (N, {C'}, P, {}, A)"
| delete_bwd_p: "C' ∈ no_labels.Red_F {C} ∨ C ≺⋅ C' ⟹
    state (N, {C}, P ∪ {C'}, {}, A) ↝OL state (N, {C}, P, {}, A)"
| simplify_bwd_p: "C' ∈ no_labels.Red_F {C, C''} ⟹
    state (N, {C}, P ∪ {C'}, {}, A) ↝OL state (N ∪ {C''}, {C}, P, {}, A)"
| delete_bwd_a: "C' ∈ no_labels.Red_F {C} ∨ C ≺⋅ C' ⟹
    state (N, {C}, P, {}, A ∪ {C'}) ↝OL state (N, {C}, P, {}, A)"
| simplify_bwd_a: "C' ∈ no_labels.Red_F ({C, C'' }) ⟹
    state (N, {C}, P, {}, A ∪ {C'}) ↝OL state (N ∪ {C''}, {C}, P, {}, A)"
| transfer: "state (N, {C}, P, {}, A) ↝OL state (N, {}, P ∪ {C}, {}, A)"
| choose_p: "C ∉ P ⟹ state ({}, {}, P ∪ {C}, {}, A) ↝OL state ({}, {}, P, {C}, A)"
| infer: "no_labels.Inf_between A {C} ⊆ no_labels.Red_I (A ∪ {C} ∪ M) ⟹
    state ({}, {}, P, {C}, A) ↝OL state (M, {}, P, {}, A ∪ {C})"

lemma prj_state_union_sets [simp]: "fst ` state (N, X, P, Y, A) = N ∪ X ∪ P ∪ Y ∪ A"
  using prj_fl_set_to_f_set_distr_union prj_labeledN_eq_N by auto

lemma active_subset_of_setOfFormulasWithLabelDiffActive:
  "l ≠ Active ⟹ active_subset {(C', l)} = {}"
  by (simp add: active_subset_def)

lemma state_add_C_New: "state (N, X, P, Y, A) ∪ {(C, New)} = state (N ∪ {C}, X, P, Y, A)"
  by auto

lemma state_add_C_XX: "state (N, X, P, Y, A) ∪ {(C, XX)} = state (N, X ∪ {C}, P, Y, A)"
  by auto

lemma state_add_C_Passive: "state (N, X, P, Y, A) ∪ {(C, Passive)} = state (N, X, P ∪ {C}, Y, A)"
  by auto

lemma state_add_C_YY: "state (N, X, P, Y, A) ∪ {(C, YY)} = state (N, X, P, Y ∪ {C}, A)"
  by auto

lemma state_add_C_Active: "state (N, X, P, Y, A) ∪ {(C, Active)} = state (N, X, P, Y, A ∪ {C})"
  by auto

lemma prj_ActiveSubset_of_state: "fst ` active_subset (state (N, X, P, Y, A)) = A"
  unfolding active_subset_def by force


subsection ‹Refinement›

lemma chooseN_in_GC: "state (N ∪ {C}, {}, P, {}, A) ↝GC state (N, {C}, P, {}, A)"
proof -
  have XX_ls_New: "XX ⊏L New"
    by (simp add: OL_Prec_L_def)
  hence almost_thesis:
    "state (N, {}, P, {}, A) ∪ {(C, New)} ↝GC state (N, {}, P, {}, A) ∪ {(C, XX)}"
    using relabel_inactive by blast
  have rewrite_left: "state (N, {}, P, {}, A) ∪ {(C, New)} = state (N ∪ {C}, {}, P, {}, A)"
    using state_add_C_New by blast
  moreover have rewrite_right: "state (N, {}, P, {}, A) ∪ {(C, XX)} =  state (N, {C}, P, {}, A)"
    using state_add_C_XX by auto
  ultimately show ?thesis
    using almost_thesis rewrite_left rewrite_right by simp
qed

lemma deleteFwd_in_GC:
  assumes "C ∈ no_labels.Red_F (P ∪ A) ∨ (∃C' ∈ P ∪ A. C' ≼⋅ C)"
  shows "state (N, {C}, P, {}, A) ↝GC state (N, {}, P, {}, A)"
  using assms
proof
  assume c_in_redf_PA: "C ∈ no_labels.Red_F (P ∪ A)"
  have "P ∪ A ⊆ N ∪ {} ∪ P ∪ {} ∪ A" by auto
  then have "no_labels.Red_F (P ∪ A) ⊆ no_labels.Red_F (N ∪ {} ∪ P ∪ {} ∪ A)"
    using no_labels.Red_F_of_subset by simp
  then have c_in_redf_NPA: "C ∈ no_labels.Red_F (N ∪ {} ∪ P ∪ {} ∪ A)"
    using c_in_redf_PA by auto
  have NPA_eq_prj_state_NPA: "N ∪ {} ∪ P ∪ {} ∪ A = fst ` state (N, {}, P, {}, A)"
    using prj_state_union_sets by simp
  have "C ∈ no_labels.Red_F (fst ` state (N, {}, P, {}, A))"
    using c_in_redf_NPA NPA_eq_prj_state_NPA by fastforce
  then show ?thesis
    using remove_redundant_no_label by auto
next
  assume "∃C' ∈ P ∪ A. C' ≼⋅ C"
  then obtain C' where "C' ∈ P ∪ A" and c'_le_c: "C' ≼⋅ C"
    by auto
  then have "C' ∈ P ∨ C' ∈ A"
    by blast
  then show ?thesis
  proof
    assume "C' ∈ P"
    then have c'_Passive_in: "(C', Passive) ∈ state (N, {}, P, {}, A)"
      by simp
    have "Passive ⊏L XX"
      by (simp add: OL_Prec_L_def)
    then have "state (N, {}, P, {}, A) ∪ {(C, XX)} ↝GC state (N, {}, P, {}, A)"
      using remove_succ_L c'_le_c c'_Passive_in by blast
    then show ?thesis
      by auto
  next
    assume "C' ∈ A"
    then have c'_Active_in_state_NPA: "(C', Active) ∈ state (N, {}, P, {}, A)"
      by simp
    also have Active_ls_x: "Active ⊏L XX"
      using Active_minimal by simp
    then  have " state (N, {}, P, {}, A) ∪ {(C, XX)} ↝GC state (N, {}, P, {}, A) "
      using remove_succ_L c'_le_c Active_ls_x c'_Active_in_state_NPA by blast
    then show ?thesis
      by auto
  qed
qed

lemma simplifyFwd_in_GC:
  "C ∈ no_labels.Red_F (P ∪ A ∪ {C'}) ⟹
   state (N, {C}, P, {}, A) ↝GC state (N, {C'}, P, {}, A)"
proof -
  assume c_in: "C ∈ no_labels.Red_F (P ∪ A ∪ {C'})"
  let ?𝒩 = "state (N, {}, P, {}, A)"
  and ?ℳ = "{(C, XX)}" and ?ℳ' = "{(C', XX)}"

  have "P ∪ A ∪ {C'} ⊆ fst` (?𝒩 ∪ ?ℳ')"
    by auto
  then have "no_labels.Red_F (P ∪ A ∪ {C'}) ⊆ no_labels.Red_F (fst` (?𝒩 ∪ ?ℳ'))"
    using no_labels.Red_F_of_subset by auto
  then have "C ∈ no_labels.Red_F (fst` (?𝒩 ∪ ?ℳ'))"
    using c_in by auto
  then have c_x_in: "(C, XX) ∈ Red_F (?𝒩 ∪ ?ℳ')"
    using no_labels_Red_F_imp_Red_F by auto
  then have "?ℳ ⊆ Red_F (?𝒩 ∪ ?ℳ')"
    by auto
  then have active_subset_of_m': "active_subset ?ℳ' = {}"
    using active_subset_of_setOfFormulasWithLabelDiffActive by auto
  show ?thesis
    using c_x_in active_subset_of_m' process[of _ _ "?ℳ" _ "?ℳ'"] by auto
qed

lemma deleteBwdP_in_GC:
  assumes "C' ∈ no_labels.Red_F {C} ∨ C ≺⋅ C'"
  shows  "state (N, {C}, P ∪ {C'}, {}, A) ↝GC state (N, {C}, P, {}, A)"
  using assms
  proof
    let ?𝒩 = "state (N, {C}, P, {}, A)"
    assume c_ls_c': " C ≺⋅ C' "

    have "(C, XX) ∈ state (N, {C}, P, {}, A)"
      by simp
    then have "?𝒩 ∪ {(C', Passive)} ↝GC ?𝒩"
      using c_ls_c' remove_succ_F by blast
    also have "?𝒩 ∪ {(C', Passive)} = state (N, {C}, P ∪ {C'}, {}, A)"
      by auto
    finally show ?thesis
      by auto
  next
    let ?𝒩 = "state (N, {C}, P, {}, A)"
    assume c'_in_redf_c: " C' ∈ no_labels.Red_F_𝒢 {C} "
    have " {C} ⊆ fst` ?𝒩" by auto
    then have " no_labels.Red_F {C} ⊆ no_labels.Red_F (fst` ?𝒩) "
      using no_labels.Red_F_of_subset by auto
    then have " C' ∈ no_labels.Red_F (fst` ?𝒩) "
      using c'_in_redf_c by blast
    then have "?𝒩 ∪ {(C', Passive)} ↝GC ?𝒩"
      using remove_redundant_no_label by blast
    then show ?thesis
      by (metis state_add_C_Passive)
  qed

lemma simplifyBwdP_in_GC:
  assumes "C' ∈ no_labels.Red_F {C, C''}"
  shows "state (N, {C}, P ∪ {C'}, {}, A) ↝GC state (N ∪ {C''}, {C}, P, {}, A)"
proof -
  let ?𝒩 = "state (N, {C}, P, {}, A)"
  and ?ℳ = "{(C', Passive)}"
  and ?ℳ' = "{(C'', New)}"

  have "{C, C''} ⊆ fst` (?𝒩 ∪ ?ℳ')"
    by (smt (z3) Un_commute Un_empty_left Un_insert_right insert_absorb2
        subset_Un_eq state_add_C_New prj_state_union_sets)
  then have "no_labels.Red_F {C, C''} ⊆ no_labels.Red_F (fst` (?𝒩 ∪ ?ℳ'))"
    using no_labels.Red_F_of_subset by auto
  then have "C' ∈ no_labels.Red_F (fst` (?𝒩 ∪ ?ℳ'))"
    using assms by auto
  then have "(C', Passive) ∈ Red_F (?𝒩 ∪ ?ℳ')"
    using no_labels_Red_F_imp_Red_F by auto
  then have ℳ_in_redf: "?ℳ ⊆ Red_F (?𝒩 ∪ ?ℳ')" by auto

  have active_subset_ℳ': "active_subset ?ℳ' = {}"
    using active_subset_of_setOfFormulasWithLabelDiffActive by auto

  have "?𝒩 ∪ ?ℳ ↝GC ?𝒩 ∪ ?ℳ'"
    using ℳ_in_redf active_subset_ℳ' process[of _ _ "?ℳ" _ "?ℳ'"] by auto
  also have "?𝒩 ∪ {(C', Passive)} = state (N, {C}, P ∪ {C'}, {}, A)"
    by force
  also have "?𝒩 ∪ {(C'', New)} = state (N ∪ {C''}, {C}, P, {}, A)"
    using state_add_C_New by blast
  finally show ?thesis
    by auto
qed

lemma deleteBwdA_in_GC:
  assumes "C' ∈ no_labels.Red_F {C} ∨ C ≺⋅ C' "
  shows "state (N, {C}, P, {}, A ∪ {C'}) ↝GC state (N, {C}, P, {}, A) "
  using assms
proof
    let ?𝒩 = "state (N, {C}, P, {}, A)"
    assume c_ls_c': " C ≺⋅ C' "

    have " (C, XX) ∈ state (N, {C}, P, {}, A) "
      by simp
    then have "?𝒩 ∪ {(C', Active)} ↝GC ?𝒩"
      using c_ls_c' remove_succ_F by blast
    also have "?𝒩 ∪ {(C', Active)} = state (N, {C}, P, {}, A ∪ {C'})"
      by auto
    finally show "state (N, {C}, P, {}, A ∪ {C'}) ↝GC state (N, {C}, P, {}, A)"
      by auto
next
    let ?𝒩 = "state (N, {C}, P, {}, A)"
    assume c'_in_redf_c: " C' ∈ no_labels.Red_F_𝒢 {C} "

    have " {C} ⊆ fst` ?𝒩 "
      by (metis Un_commute Un_upper2 le_supI2 prj_state_union_sets)
    then have " no_labels.Red_F {C} ⊆ no_labels.Red_F (fst` ?𝒩) "
      using no_labels.Red_F_of_subset by auto
    then have " C' ∈ no_labels.Red_F (fst` ?𝒩) "
      using c'_in_redf_c by blast
    then have "?𝒩 ∪ {(C', Active)} ↝GC ?𝒩"
      using remove_redundant_no_label by auto
    then show ?thesis
      by (metis state_add_C_Active)
qed

lemma simplifyBwdA_in_GC:
  assumes "C' ∈ no_labels.Red_F {C, C''}"
  shows "state (N, {C}, P, {}, A ∪ {C'}) ↝GC state (N ∪ {C''}, {C}, P, {}, A)"
proof -
  let ?𝒩 = "state (N, {C}, P, {}, A)" and ?ℳ = "{(C', Active)}" and ?ℳ' = "{(C'', New)}"

  have " {C, C''} ⊆ fst` (?𝒩 ∪ ?ℳ') "
    by simp
  then have " no_labels.Red_F {C, C''} ⊆ no_labels.Red_F (fst` (?𝒩 ∪ ?ℳ')) "
    using no_labels.Red_F_of_subset by auto
  then have " C' ∈ no_labels.Red_F (fst` (?𝒩 ∪ ?ℳ')) "
    using assms by auto
  then have " (C', Active) ∈ Red_F (?𝒩 ∪ ?ℳ') "
    using no_labels_Red_F_imp_Red_F by auto
  then have ℳ_included: " ?ℳ ⊆ Red_F (?𝒩 ∪ ?ℳ') "
    by auto

  have "active_subset ?ℳ' = {}"
    using active_subset_of_setOfFormulasWithLabelDiffActive by auto
  then have "state (N, {C}, P, {}, A) ∪ {(C', Active)} ↝GC state (N, {C}, P, {}, A) ∪ {(C'', New)}"
    using ℳ_included process[where ?M="?ℳ" and ?M'="?ℳ'"] by auto
  then show ?thesis
    by (metis state_add_C_New state_add_C_Active)
qed

lemma transfer_in_GC: "state (N, {C}, P, {}, A) ↝GC state (N, {}, P ∪ {C}, {}, A)"
proof -
  let ?𝒩 = "state (N, {}, P, {}, A)"

  have "Passive ⊏L XX"
    by (simp add: OL_Prec_L_def)
  then have "?𝒩 ∪ {(C, XX)} ↝GC ?𝒩 ∪ {(C, Passive)}"
    using relabel_inactive by auto
  then show ?thesis
    by (metis sup_bot_left state_add_C_XX state_add_C_Passive)
qed

lemma chooseP_in_GC: "state ({}, {}, P ∪ {C}, {}, A) ↝GC state ({}, {}, P, {C}, A)"
proof -
  let ?𝒩 = "state ({}, {}, P, {}, A)"

  have "YY ⊏L Passive"
    by (simp add: OL_Prec_L_def)
  moreover have "YY ≠ Active"
    by simp
  ultimately have "?𝒩 ∪ {(C, Passive)} ↝GC ?𝒩 ∪ {(C, YY)}"
    using relabel_inactive by auto
  then show ?thesis
    by (metis sup_bot_left state_add_C_Passive state_add_C_YY)
qed

lemma infer_in_GC:
  assumes "no_labels.Inf_between A {C} ⊆ no_labels.Red_I (A ∪ {C} ∪ M)"
  shows "state ({}, {}, P, {C}, A) ↝GC state (M, {}, P, {}, A ∪ {C})"
proof -
  let ?ℳ = "{(C', New) | C'. C' ∈ M}"
  let ?𝒩 = "state ({}, {}, P, {}, A)"

  have active_subset_of_ℳ: "active_subset ?ℳ = {}"
    using active_subset_def by auto

  have "A ∪ {C} ∪ M ⊆ (fst` ?𝒩) ∪ {C} ∪ (fst` ?ℳ)"
    by fastforce
  then have "no_labels.Red_I (A ∪ {C} ∪ M) ⊆ no_labels.Red_I ((fst` ?𝒩) ∪ {C} ∪ (fst` ?ℳ))"
    using no_labels.empty_ord.Red_I_of_subset by auto
  moreover have "fst` (active_subset ?𝒩) = A"
    using prj_ActiveSubset_of_state by blast
  ultimately have "no_labels.Inf_between (fst` (active_subset ?𝒩)) {C} ⊆
    no_labels.Red_I ((fst` ?𝒩) ∪ {C} ∪ (fst` ?ℳ))"
    using assms by auto

  then have "?𝒩 ∪ {(C, YY)} ↝GC ?𝒩 ∪ {(C, Active)} ∪ ?ℳ"
    using active_subset_of_ℳ prj_fl_set_to_f_set_distr_union step.infer by force
  also have "?𝒩 ∪ {(C, YY)} = state ({}, {}, P, {C}, A)"
    by simp
  also have "?𝒩 ∪ {(C, Active)} ∪ ?ℳ = state (M, {}, P, {}, A ∪ {C})"
    by force
  finally show ?thesis
    by simp
qed

theorem OL_step_imp_GC_step: "M ↝OL M' ⟹ M ↝GC M'"
proof (induction rule: OL.induct)
  case (choose_n N C P A)
  then show ?case
    using chooseN_in_GC by auto
next
  case (delete_fwd C P A N)
  then show ?case
    using deleteFwd_in_GC by auto
next
  case (simplify_fwd C P A C' N)
  then show ?case
    using simplifyFwd_in_GC by auto
next
  case (delete_bwd_p C' C N P A)
  then show ?case
    using deleteBwdP_in_GC by auto
next
  case (simplify_bwd_p C' C C'' N P A)
  then show ?case
    using simplifyBwdP_in_GC by auto
next
  case (delete_bwd_a C' C N P A)
  then show ?case
    using deleteBwdA_in_GC by auto
next
  case (simplify_bwd_a C' C N P A C'')
  then show ?case
    using simplifyBwdA_in_GC by blast
next
  case (transfer N C P A)
  then show ?case
    using transfer_in_GC by auto
next
  case (choose_p P C A)
  then show ?case
    using chooseP_in_GC by auto
next
  case (infer A C M P)
  then show ?case
    using infer_in_GC by auto
qed


subsection ‹Completeness›

theorem
  assumes
    ol_chain: "chain (↝OL) Sts" and
    act: "active_subset (lhd Sts) = {}" and
    pas: "passive_subset (Liminf_llist Sts) = {}"
  shows
    OL_Liminf_saturated: "saturated (Liminf_llist Sts)" and
    OL_complete_Liminf: "B ∈ Bot_F ⟹ fst ` lhd Sts ⊨∩𝒢 {B} ⟹
      ∃BL ∈ Bot_FL. BL ∈ Liminf_llist Sts" and
    OL_complete: "B ∈ Bot_F ⟹ fst ` lhd Sts ⊨∩𝒢 {B} ⟹
      ∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ lnth Sts i)"
proof -
  have gc_chain: "chain (↝GC) Sts"
    using ol_chain OL_step_imp_GC_step chain_mono by blast

  show "saturated (Liminf_llist Sts)"
    using assms(2) gc.fair_implies_Liminf_saturated gc_chain gc_fair gc_to_red pas by blast

  {
    assume
      bot: "B ∈ Bot_F" and
      unsat: "fst ` lhd Sts ⊨∩𝒢 {B}"

    show "∃BL ∈ Bot_FL. BL ∈ Liminf_llist Sts"
      by (rule gc_complete_Liminf[OF gc_chain act pas bot unsat])
    then show "∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ lnth Sts i)"
      unfolding Liminf_llist_def by auto
  }
qed

end

end