# Theory Non_Redundancy

```theory Non_Redundancy
imports
SCL_FOL
Trail_Induced_Ordering
Initial_Literals_Generalize_Learned_Literals
Multiset_Order_Extra
begin

context scl_fol_calculus begin

section ‹Reasonable Steps›

lemma reasonable_scl_sound_state:
"reasonable_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
using scl_preserves_sound_state reasonable_scl_def by blast

lemma reasonable_run_sound_state:
"(reasonable_scl N β)⇧*⇧* S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
by (smt (verit, best) reasonable_scl_sound_state rtranclp_induct)

subsection ‹Invariants›

subsubsection ‹No Conflict After Decide›

inductive no_conflict_after_decide for N β U where
Nil[simp]: "no_conflict_after_decide N β U []" |
Cons: "(is_decision_lit Ln ⟶ (∄S'. conflict N β (Ln # Γ, U, None) S')) ⟹
no_conflict_after_decide N β U Γ ⟹ no_conflict_after_decide N β U (Ln # Γ)"

definition no_conflict_after_decide' where
"no_conflict_after_decide' N β S = no_conflict_after_decide N β (state_learned S) (state_trail S)"

lemma no_conflict_after_decide'_initial_state[simp]: "no_conflict_after_decide' N β initial_state"

lemma propagate_preserves_no_conflict_after_decide':
assumes "propagate N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def propagate_lit_def is_decision_lit_def
elim!: propagate.cases intro!: no_conflict_after_decide.Cons)

lemma decide_preserves_no_conflict_after_decide':
assumes "decide N β S S'" and "∄S''. conflict N β S' S''" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def decide_lit_def is_decision_lit_def
elim!: decide.cases intro!: no_conflict_after_decide.Cons)

lemma conflict_preserves_no_conflict_after_decide':
assumes "conflict N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def elim: conflict.cases)

lemma skip_preserves_no_conflict_after_decide':
assumes "skip N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def
elim!: skip.cases elim: no_conflict_after_decide.cases)

lemma factorize_preserves_no_conflict_after_decide':
assumes "factorize N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def elim: factorize.cases)

lemma resolve_preserves_no_conflict_after_decide':
assumes "resolve N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def elim: resolve.cases)

lemma learning_clause_without_conflict_preserves_nex_conflict:
fixes N :: "('f, 'v) Term.term clause fset"
assumes "∄γ. is_ground_cls (C ⋅ γ) ∧ trail_false_cls Γ (C ⋅ γ)"
shows "∄S'. conflict N β (Γ, U, None) S' ⟹ ∄S'. conflict N β (Γ, finsert C U, None) S'"
proof (elim contrapos_nn exE)
fix S'
assume "conflict N β (Γ, finsert C U, None :: ('f, 'v) closure option) S'"
then show "∃S'. conflict N β (Γ, U, None) S'"
proof (cases N β "(Γ, finsert C U, None :: ('f, 'v) closure option)" S' rule: conflict.cases)
case (conflictI D γ)
then show ?thesis
using assms conflict.intros by blast
qed
qed

lemma backtrack_preserves_no_conflict_after_decide':
assumes step: "backtrack N β S S'" and invar: "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using step
proof (cases N β S S' rule: backtrack.cases)
case (backtrackI Γ Γ' Γ'' K L σ D U)
have "no_conflict_after_decide N β U (Γ' @ Γ'')"
using invar
unfolding backtrackI(1,2,3) no_conflict_after_decide'_def
by (auto simp: decide_lit_def elim: no_conflict_after_decide.cases)
hence "no_conflict_after_decide N β U Γ''"
by (induction Γ') (auto elim: no_conflict_after_decide.cases)
hence "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
using backtrackI(5)
proof (induction Γ'')
case Nil
show ?case
by (auto intro: no_conflict_after_decide.Nil)
next
case (Cons Ln Γ'')
hence "∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls (Ln # Γ'') (add_mset L D ⋅ γ)"
by metis
hence "∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls Γ'' (add_mset L D ⋅ γ)"
by (metis (no_types, opaque_lifting) image_insert insert_iff list.set(2) trail_false_cls_def
trail_false_lit_def)
hence 1: "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
by (rule Cons.IH)

show ?case
proof (intro no_conflict_after_decide.Cons impI)
assume "is_decision_lit Ln"
with Cons.hyps have "∄S'. conflict N β (Ln # Γ'', U, None) S'"
by simp
then show "∄S'. conflict N β (Ln # Γ'', finsert (add_mset L D) U, None) S'"
using learning_clause_without_conflict_preserves_nex_conflict
using ‹∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls (Ln # Γ'') (add_mset L D ⋅ γ)›
by blast
next
show "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
using 1 .
qed
qed
thus ?thesis
unfolding backtrackI(1,2) no_conflict_after_decide'_def by simp
qed

lemma reasonable_scl_preserves_no_conflict_after_decide':
assumes "reasonable_scl N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms unfolding reasonable_scl_def scl_def
using propagate_preserves_no_conflict_after_decide' decide_preserves_no_conflict_after_decide'
conflict_preserves_no_conflict_after_decide' skip_preserves_no_conflict_after_decide'
factorize_preserves_no_conflict_after_decide' resolve_preserves_no_conflict_after_decide'
backtrack_preserves_no_conflict_after_decide'
by metis

subsection ‹Miscellaneous Lemmas›

lemma before_reasonable_conflict:
assumes conf: "conflict N β S1 S2" and
invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1"
"no_conflict_after_decide' N β S1"
shows "{#} |∈| N ∨ (∃S0. propagate N β S0 S1)"
using before_conflict[OF conf invars(1,2)]
proof (elim disjE exE)
fix S0 assume "decide N β S0 S1"
hence False
proof (cases N β S0 S1 rule: decide.cases)
case (decideI L γ Γ U)
with invars(3) have "no_conflict_after_decide N β U (trail_decide Γ (L ⋅l γ))"
hence "∄S'. conflict N β (trail_decide Γ (L ⋅l γ), U, None) S'"
by (rule no_conflict_after_decide.cases) (simp_all add: decide_lit_def is_decision_lit_def)
then show ?thesis
using conf unfolding decideI(1,2) by metis
qed
thus ?thesis ..
qed auto

section ‹Regular Steps›

lemma regular_scl_if_conflict[simp]: "conflict N β S S' ⟹ regular_scl N β S S'"

lemma regular_scl_if_skip[simp]: "skip N β S S' ⟹ regular_scl N β S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases skip.cases)

lemma regular_scl_if_factorize[simp]: "factorize N β S S' ⟹ regular_scl N β S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases factorize.cases)

lemma regular_scl_if_resolve[simp]: "resolve N β S S' ⟹ regular_scl N β S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases resolve.cases)

lemma regular_scl_if_backtrack[simp]: "backtrack N β S S' ⟹ regular_scl N β S S'"
by (smt (verit) backtrack.cases decide_well_defined(6) option.discI regular_scl_def conflict.simps
reasonable_scl_def scl_def state_conflict_simp)

lemma regular_scl_sound_state: "regular_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
by (rule reasonable_scl_sound_state[OF reasonable_if_regular])

lemma regular_run_sound_state:
"(regular_scl N β)⇧*⇧* S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
by (smt (verit, best) regular_scl_sound_state rtranclp_induct)

subsection ‹Invariants›

subsubsection ‹Almost No Conflict With Trail›

inductive no_conflict_with_trail for N β U where
Nil: "(∄S'. conflict N β ([], U, None) S') ⟹ no_conflict_with_trail N β U []" |
Cons: "(∄S'. conflict N β (Ln # Γ, U, None) S') ⟹
no_conflict_with_trail N β U Γ ⟹ no_conflict_with_trail N β U (Ln # Γ)"

lemma nex_conflict_if_no_conflict_with_trail:
assumes "no_conflict_with_trail N β U Γ"
shows "∄S'. conflict N β (Γ, U, None) S'"
using assms by (auto elim: no_conflict_with_trail.cases)

lemma nex_conflict_if_no_conflict_with_trail':
assumes "no_conflict_with_trail N β U Γ"
shows "∄S'. conflict N β ([], U, None) S'"
using assms
by (induction Γ rule: no_conflict_with_trail.induct) simp_all

lemma no_conflict_after_decide_if_no_conflict_with_trail:
"no_conflict_with_trail N β U Γ ⟹ no_conflict_after_decide N β U Γ"
by (induction Γ rule: no_conflict_with_trail.induct)

lemma not_trail_false_cls_if_no_conflict_with_trail:
"no_conflict_with_trail N β U Γ ⟹ D |∈| N |∪| U ⟹ D ≠ {#} ⟹ is_ground_cls (D ⋅ γ) ⟹
¬ trail_false_cls Γ (D ⋅ γ)"
proof (induction Γ rule: no_conflict_with_trail.induct)
case Nil
thus ?case by simp
next
case (Cons Ln Γ)
hence "¬ trail_false_cls (Ln # Γ) (D ⋅ γ)"
by (metis fst_conv not_trail_false_ground_cls_if_no_conflict state_conflict_simp
state_learned_simp state_trail_def)
thus ?case
by simp
qed

definition almost_no_conflict_with_trail where
"almost_no_conflict_with_trail N β S ⟷
{#} |∈| N ∧ state_trail S = [] ∨
no_conflict_with_trail N β (state_learned S)
(case state_trail S of [] ⇒ [] | Ln # Γ ⇒ if is_decision_lit Ln then Ln # Γ else Γ)"

lemma nex_conflict_if_no_conflict_with_trail'':
assumes no_conf: "state_conflict S = None" and "{#} |∉| N" and "learned_nonempty S"
"no_conflict_with_trail N β (state_learned S) (state_trail S)"
shows "∄S'. conflict N β S S'"
proof -
from no_conf obtain Γ U where S_def: "S = (Γ, U, None)"
by (metis state_simp)

from ‹learned_nonempty S› have "{#} |∉| U"

show ?thesis
using assms(4)
unfolding S_def state_proj_simp
proof (cases N β U Γ rule: no_conflict_with_trail.cases)
case Nil
then show "∄S'. conflict N β (Γ, U, None) S'"
using ‹{#} |∉| N› ‹{#} |∉| U›
by (auto simp: trail_false_cls_def elim: conflict.cases)
next
case (Cons Ln Γ')
then show "∄S'. conflict N β (Γ, U, None) S'"
by (auto intro: no_conflict_tail_trail)
qed
qed

lemma no_conflict_with_trail_if_nex_conflict:
assumes no_conf: "∄S'. conflict N β S S'" "state_conflict S = None"
shows "no_conflict_with_trail N β (state_learned S) (state_trail S)"
proof -
from no_conf(2) obtain Γ U where S_def: "S = (Γ, U, None)"
by (metis state_simp)

show ?thesis
using no_conf(1)
unfolding S_def state_proj_simp
proof (induction Γ)
case Nil
thus ?case by (simp add: no_conflict_with_trail.Nil)
next
case (Cons Ln Γ)
have "∄a. conflict N β (Γ, U, None) a"
by (rule no_conflict_tail_trail[OF Cons.prems])
hence "no_conflict_with_trail N β U Γ"
by (rule Cons.IH)
then show ?case
using Cons.prems
by (auto intro: no_conflict_with_trail.Cons)
qed
qed

lemma almost_no_conflict_with_trail_if_no_conflict_with_trail:
"no_conflict_with_trail N β U Γ ⟹ almost_no_conflict_with_trail N β (Γ, U, Cl)"
by (cases Γ) (auto simp: almost_no_conflict_with_trail_def elim: no_conflict_with_trail.cases)

lemma almost_no_conflict_with_trail_initial_state[simp]:
"almost_no_conflict_with_trail N β initial_state"
by (cases "{#} |∈| N") (auto simp: almost_no_conflict_with_trail_def trail_false_cls_def
elim!: conflict.cases intro: no_conflict_with_trail.Nil)

lemma propagate_preserves_almost_no_conflict_with_trail:
assumes step: "propagate N β S S'" and reg_step: "regular_scl N β S S'"
shows "almost_no_conflict_with_trail N β S'"
using reg_step[unfolded regular_scl_def]
proof (elim disjE conjE)
assume "conflict N β S S'"
with step have False
using conflict_well_defined by blast
thus ?thesis ..
next
assume no_conf: "∄S'. conflict N β S S'" and "reasonable_scl N β S S'"
from step show ?thesis
proof (cases N β S S' rule: propagate.cases)
case step_hyps: (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
have "no_conflict_with_trail N β U Γ"
by (rule no_conflict_with_trail_if_nex_conflict[OF no_conf,
unfolded step_hyps state_proj_simp, OF refl])
thus ?thesis
unfolding step_hyps(1,2)
by (simp add: almost_no_conflict_with_trail_def propagate_lit_def is_decision_lit_def)
qed
qed

lemma decide_preserves_almost_no_conflict_with_trail:
assumes step: "decide N β S S'" and reg_step: "regular_scl N β S S'"
shows "almost_no_conflict_with_trail N β S'"
proof -
from reg_step have res_step: "reasonable_scl N β S S'"
by (rule reasonable_if_regular)

from step obtain Γ U where S'_def: "S' = (Γ, U, None)"
by (auto elim: decide.cases)

have "no_conflict_with_trail N β (state_learned S') (state_trail S')"
proof (rule no_conflict_with_trail_if_nex_conflict)
show "∄S''. conflict N β S' S''"
using step res_step[unfolded reasonable_scl_def] by argo
next
show "state_conflict S' = None"
qed
thus ?thesis
unfolding S'_def
qed

lemma almost_no_conflict_with_trail_conflict_not_relevant:
"almost_no_conflict_with_trail N β (Γ, U, Cl1) ⟷
almost_no_conflict_with_trail N β (Γ, U, Cl2)"

lemma conflict_preserves_almost_no_conflict_with_trail:
assumes step: "conflict N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
proof -
from step obtain Γ U Cl where "S = (Γ, U, None)" and "S' = (Γ, U, Some Cl)"
by (auto elim: conflict.cases)
with invar show ?thesis
using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed

lemma skip_preserves_almost_no_conflict_with_trail:
assumes step: "skip N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
using step
proof (cases N β S S' rule: skip.cases)
case step_hyps: (skipI L D σ n Γ U)
have "no_conflict_with_trail N β U (if is_decision_lit (L, n) then (L, n) # Γ else Γ)"
using invar unfolding step_hyps(1,2) by (simp add: almost_no_conflict_with_trail_def)
hence "no_conflict_with_trail N β U Γ"
by (cases "is_decision_lit (L, n)") (auto elim: no_conflict_with_trail.cases)
then show ?thesis
unfolding step_hyps(1,2)
by (rule almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed

lemma factorize_preserves_almost_no_conflict_with_trail:
assumes step: "factorize N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
proof -
from step obtain Γ U Cl1 Cl2 where "S = (Γ, U, Some Cl1)" and "S' = (Γ, U, Some Cl2)"
by (auto elim: factorize.cases)
with invar show ?thesis
using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed

lemma resolve_preserves_almost_no_conflict_with_trail:
assumes step: "resolve N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
proof -
from step obtain Γ U Cl1 Cl2 where "S = (Γ, U, Some Cl1)" and "S' = (Γ, U, Some Cl2)"
by (auto elim: resolve.cases)
with invar show ?thesis
using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed

lemma backtrack_preserves_almost_no_conflict_with_trail:
assumes step: "backtrack N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
using step
proof (cases N β S S' rule: backtrack.cases)
case step_hyps: (backtrackI Γ Γ' Γ'' K L σ D U)
from invar have "no_conflict_with_trail N β U ((- (L ⋅l σ), None) # Γ' @ Γ'')"
by (simp add: step_hyps almost_no_conflict_with_trail_def decide_lit_def is_decision_lit_def)
hence "no_conflict_with_trail N β U (Γ' @ Γ'')"
by (auto elim: no_conflict_with_trail.cases)
hence "no_conflict_with_trail N β U Γ''"
by (induction Γ') (auto elim: no_conflict_with_trail.cases)
then have "no_conflict_with_trail N β (finsert (add_mset L D) U) Γ''"
by (metis learning_clause_without_conflict_preserves_nex_conflict
nex_conflict_if_no_conflict_with_trail no_conflict_with_trail_if_nex_conflict
state_conflict_simp state_learned_simp state_trail_simp step_hyps(5))
thus ?thesis
unfolding step_hyps(1,2)
by (rule almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed

lemma regular_scl_preserves_almost_no_conflict_with_trail:
assumes "regular_scl N β S S'" and "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
using assms
using propagate_preserves_almost_no_conflict_with_trail decide_preserves_almost_no_conflict_with_trail
conflict_preserves_almost_no_conflict_with_trail skip_preserves_almost_no_conflict_with_trail
factorize_preserves_almost_no_conflict_with_trail resolve_preserves_almost_no_conflict_with_trail
backtrack_preserves_almost_no_conflict_with_trail
by (metis scl_def reasonable_if_regular scl_if_reasonable)

subsubsection ‹Backtrack Follows Regular Conflict Resolution›

lemma before_conflict_in_regular_run:
assumes
reg_run: "(regular_scl N β)⇧*⇧* initial_state S1" and
conf: "conflict N β S1 S2" and
"{#} |∉| N"
shows "∃S0. (regular_scl N β)⇧*⇧* initial_state S0 ∧ regular_scl N β S0 S1 ∧ (propagate N β S0 S1)"
proof -
from reg_run conf show ?thesis
proof (induction S1 arbitrary: S2 rule: rtranclp_induct)
case base
with ‹{#} |∉| N› have False
by (meson fempty_iff funion_iff mempty_in_iff_ex_conflict)
thus ?case ..
next
case (step S0 S1)
from step.hyps(1) have "learned_nonempty S0"
by (induction S0 rule: rtranclp_induct)
reasonable_if_regular]])
with step.hyps(2) have "learned_nonempty S1"
by (simp add: scl_preserves_learned_nonempty[OF scl_if_reasonable[OF reasonable_if_regular]])

from step.hyps(1) have "trail_propagated_or_decided' N β S0"
by (induction S0 rule: rtranclp_induct)
reasonable_if_regular]])
with step.hyps(2) have "trail_propagated_or_decided' N β S1"
reasonable_if_regular]])

from step.hyps(1) have "almost_no_conflict_with_trail N β S0"
by (induction S0 rule: rtranclp_induct)
with step.hyps(2) have "almost_no_conflict_with_trail N β S1"

show ?case
proof (intro exI conjI)
show "(regular_scl N β)⇧*⇧* initial_state S0"
using step.hyps by simp
next
show "regular_scl N β S0 S1"
using step.hyps by simp
next
from step.prems obtain Γ U C γ where
S1_def: "S1 = (Γ, U, None)" and
S2_def: "S2 = (Γ, U, Some (C, γ))" and
C_in: "C |∈| N |∪| U" and
ground_conf: "is_ground_cls (C ⋅ γ)" and
tr_false_conf: "trail_false_cls Γ (C ⋅ γ)"
unfolding conflict.simps by auto
with step.hyps have "¬ conflict N β S0 S1" and "reasonable_scl N β S0 S1"
unfolding regular_scl_def by (simp_all add: conflict.simps)
with step.prems have "scl N β S0 S1" and "¬ decide N β S0 S1"
unfolding reasonable_scl_def by blast+
moreover from step.prems have "¬ backtrack N β S0 S1"
proof (cases Γ)
case Nil
then show ?thesis
using ‹{#} |∉| N› ‹almost_no_conflict_with_trail N β S1› step.prems
by (auto simp: S1_def almost_no_conflict_with_trail_def elim: no_conflict_with_trail.cases)
next
case (Cons Ln Γ')
have "C ≠ {#}"
using ‹{#} |∉| N›
by (metis C_in S1_def ‹learned_nonempty S1› funionE learned_nonempty_def state_proj_simp(2))

from Cons have "¬ is_decision_lit Ln"
using ‹¬ decide N β S0 S1›[unfolded S1_def]
by (metis (mono_tags, lifting) S1_def ‹almost_no_conflict_with_trail N β S1›
almost_no_conflict_with_trail_def list.discI list.simps(5)
nex_conflict_if_no_conflict_with_trail state_learned_simp state_trail_simp step.prems)
with ‹{#} |∉| N› have "no_conflict_with_trail N β U Γ'"
using ‹almost_no_conflict_with_trail N β S1›
by (simp add: Cons S1_def almost_no_conflict_with_trail_def)
with Cons show ?thesis
unfolding S1_def
using ‹{#} |∉| N›
by (smt (verit) S2_def ‹almost_no_conflict_with_trail N β S0› ‹learned_nonempty S1›
almost_no_conflict_with_trail_def backtrack.simps conflict.cases finsert_iff funionE
funion_finsert_right learned_nonempty_def list.case(2) list.sel(3) list.simps(3)
no_conflict_with_trail.simps not_trail_false_cls_if_no_conflict_with_trail
state_learned_simp state_trail_simp step.prems suffixI decide_lit_def
trail_false_cls_if_trail_false_suffix)
qed
ultimately show "propagate N β S0 S1"
by (simp add: scl_def S1_def skip.simps conflict.simps factorize.simps resolve.simps)
qed
qed
qed

definition regular_conflict_resolution where
"regular_conflict_resolution N β S ⟷ {#} |∉| N ⟶
(case state_conflict S of
None ⇒ (regular_scl N β)⇧*⇧* initial_state S |
Some _ ⇒ (∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S))))"

lemma regular_conflict_resolution_initial_state[simp]:
"regular_conflict_resolution N β initial_state"

lemma propagate_preserves_regular_conflict_resolution:
assumes step: "propagate N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step have "state_conflict S = None" and "state_conflict S' = None"
by (auto elim: propagate.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = None›
unfolding option.case
proof (rule impI)
assume "{#} |∉| N"
with invar have "(regular_scl N β)⇧*⇧* initial_state S"
unfolding regular_conflict_resolution_def ‹state_conflict S = None› by simp
thus "(regular_scl N β)⇧*⇧* initial_state S'"
using reg_step by (rule rtranclp.rtrancl_into_rtrancl)
qed
qed

lemma decide_preserves_regular_conflict_resolution:
assumes step: "decide N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step have "state_conflict S = None" and "state_conflict S' = None"
by (auto elim: decide.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = None›
unfolding option.case
proof (rule impI)
assume "{#} |∉| N"
with invar have "(regular_scl N β)⇧*⇧* initial_state S"
unfolding regular_conflict_resolution_def ‹state_conflict S = None› by simp
thus "(regular_scl N β)⇧*⇧* initial_state S'"
using reg_step by (rule rtranclp.rtrancl_into_rtrancl)
qed
qed

lemma conflict_preserves_regular_conflict_resolution:
assumes step: "conflict N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ where "state_conflict S = None" and "state_conflict S' = Some (C, γ)"
by (auto elim!: conflict.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C, γ)›
unfolding option.cases
proof (rule impI)
assume "{#} |∉| N"
with invar have reg_run: "(regular_scl N β)⇧*⇧* initial_state S"
unfolding regular_conflict_resolution_def ‹state_conflict S = None› by simp

from ‹{#} |∉| N› obtain S0 where
"(regular_scl N β)⇧*⇧* initial_state S0" "propagate N β S0 S" "regular_scl N β S0 S"
using before_conflict_in_regular_run[OF reg_run step] by metis

with step show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
using regular_scl_if_conflict
by blast
qed
qed

lemma
assumes "almost_no_conflict_with_trail N β S" and "{#} |∉| N"
shows "no_conflict_after_decide' N β S"
proof -
obtain U Γ Cl where S_def: "S = (Γ, U, Cl)"
by (metis state_simp)

show ?thesis
proof (cases Γ)
case Nil
thus ?thesis
next
case (Cons Ln Γ')
with assms have no_conf_with_trail:
"no_conflict_with_trail N β U (if is_decision_lit Ln then Ln # Γ' else Γ')"

show ?thesis
using no_conf_with_trail
by (cases "is_decision_lit Ln")
(simp_all add: S_def Cons no_conflict_after_decide'_def no_conflict_after_decide.Cons
no_conflict_after_decide_if_no_conflict_with_trail)
qed
qed

lemma mempty_not_in_learned_if_almost_no_conflict_with_trail:
"almost_no_conflict_with_trail N β S ⟹ {#} |∉| N ⟹ {#} |∉| state_learned S"
unfolding almost_no_conflict_with_trail_def
using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict]
by simp

lemma skip_preserves_regular_conflict_resolution:
assumes step: "skip N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ where
"state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C, γ)"
by (auto elim!: skip.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C, γ)›
unfolding option.cases
proof (intro impI)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis

from reg_run have "(regular_scl N β)⇧*⇧* initial_state S1"
using ‹regular_scl N β S0 S1› by simp
hence "(regular_scl N β)⇧*⇧* initial_state S2"
using ‹regular_scl N β S1 S2› by simp
hence "(regular_scl N β)⇧*⇧* initial_state S3"
using ‹(regular_scl N β)⇧*⇧* S2 S3› by simp

from ‹(factorize N β)⇧*⇧* S2 S3› have "state_trail S3 = state_trail S2"
by (induction S3 rule: rtranclp_induct) (auto elim: factorize.cases)
also from ‹conflict N β S1 S2› have "… = state_trail S1"
by (auto elim: conflict.cases)
finally have "state_trail S3 = state_trail S1"
by assumption

from ‹(factorize N β)⇧*⇧* S2 S3› have "state_learned S3 = state_learned S2"
proof (induction S3 rule: rtranclp_induct)
case base
show ?case by simp
next
case (step y z)
thus ?case
by (elim factorize.cases) simp
qed
also from ‹conflict N β S1 S2› have "… = state_learned S1"
by (auto elim: conflict.cases)
finally have "state_learned S3 = state_learned S1"
by assumption

from ‹propagate N β S0 S1› have "state_learned S1 = state_learned S0"
by (auto elim: propagate.cases)

from ‹propagate N β S0 S1› obtain L C γ where
"state_trail S1 = trail_propagate (state_trail S0) L C γ"
by (auto elim: propagate.cases)

from ‹(regular_scl N β)⇧*⇧* initial_state S3› have "almost_no_conflict_with_trail N β S3"
using regular_scl_preserves_almost_no_conflict_with_trail
by (induction S3 rule: rtranclp_induct) simp_all

show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
using reg_run propa confl facto
proof (intro impI exI conjI)
show "S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
using maybe_reso
proof (elim disjE exE conjE)
fix S4 assume "resolve N β S3 S4" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
with step have "∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'"
by (meson rtranclp.rtrancl_into_rtrancl sup2CI)
thus ?thesis ..
next
assume "S3 = S"
with ‹almost_no_conflict_with_trail N β S3› ‹{#} |∉| N›
have no_conf_with_trail: "no_conflict_with_trail N β (state_learned S)
(case state_trail S of [] ⇒ [] | Ln # Γ ⇒ if is_decision_lit Ln then Ln # Γ else Γ)"
hence "{#} |∉| state_learned S"
using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict]
by simp

from no_conf_with_trail
have no_conf_with_trail': "no_conflict_with_trail N β (state_learned S1) (state_trail S0)"
using ‹S3 = S› ‹state_trail S3 = state_trail S1›
‹state_learned S3 = state_learned S1›
‹state_trail S1 = trail_propagate (state_trail S0) L C γ›

have "∃D γ⇩D. state_conflict S2 = Some (D, γ⇩D) ∧ - (L ⋅l γ) ∈# D ⋅ γ⇩D"
using ‹conflict N β S1 S2›
proof (cases N β S1 S2 rule: conflict.cases)
case (conflictI D U γ⇩D Γ)
hence "trail_false_cls (trail_propagate (state_trail S0) L C γ) (D ⋅ γ⇩D)"
using ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by simp

moreover from no_conf_with_trail' have "¬ trail_false_cls (state_trail S0) (D ⋅ γ⇩D)"
unfolding ‹state_learned S1 = state_learned S0›
proof (rule not_trail_false_cls_if_no_conflict_with_trail)
show "D |∈| N |∪| state_learned S0"
using ‹state_learned S1 = state_learned S0› local.conflictI(1) local.conflictI(3)
by fastforce
next
have "{#} |∉| U"
using ‹{#} |∉| state_learned S› ‹S3 = S› ‹state_learned S3 = state_learned S1›
unfolding conflictI(1,2)
by simp
thus "D ≠ {#}"
using ‹{#} |∉| N› ‹D |∈| N |∪| U›
by auto
next
show "is_ground_cls (D ⋅ γ⇩D)"
by (rule ‹is_ground_cls (D ⋅ γ⇩D)›)
qed

ultimately have "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by (metis subtrail_falseI propagate_lit_def)

moreover have "state_conflict S2 = Some (D, γ⇩D)"
unfolding conflictI(1,2) by simp

ultimately show ?thesis
by metis
qed
then obtain D γ⇩D where "state_conflict S2 = Some (D, γ⇩D)" and "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by metis

with ‹(factorize N β)⇧*⇧* S2 S3›
have "∃D' γ⇩D'. state_conflict S3 = Some (D', γ⇩D') ∧ - (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
proof (induction S3 arbitrary: rule: rtranclp_induct)
case base
thus ?case by simp
next
case (step y z)
then obtain D' γ⇩D' where "state_conflict y = Some (D', γ⇩D')" and "- (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
by auto
then show ?case
using step.hyps(2)
by (metis conflict_set_after_factorization)
qed
with step have False
using ‹state_trail S3 = state_trail S1›
unfolding ‹S3 = S› ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by (auto simp add: propagate_lit_def elim!: skip.cases)
thus ?thesis ..
qed
qed
qed
qed

lemma factorize_preserves_regular_conflict_resolution:
assumes step: "factorize N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ C' γ' where
"state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C', γ')"
by (auto elim!: factorize.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C', γ')›
unfolding option.cases
proof (intro impI)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis

show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
using maybe_reso
proof (elim disjE exE conjE)
assume "S3 = S"
show ?thesis
using reg_run propa confl
proof (intro exI conjI)
show "(factorize N β)⇧*⇧* S2 S'"
using ‹(factorize N β)⇧*⇧* S2 S3› step
by (simp add: ‹S3 = S›)
next
show "(regular_scl N β)⇧*⇧* S2 S'"
using ‹(regular_scl N β)⇧*⇧* S2 S3› reg_step
by (simp add: ‹S3 = S›)
next
show "S' = S' ∨ (∃S4. resolve N β S' S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
by simp
qed
next
fix S4 assume hyps: "resolve N β S3 S4" "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
show ?thesis
using reg_run propa confl facto
proof (intro exI conjI)
show "S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
using hyps step
by (meson rtranclp.rtrancl_into_rtrancl sup2CI)
qed
qed
qed
qed

lemma resolve_preserves_regular_conflict_resolution:
assumes step: "resolve N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ C' γ' where
"state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C', γ')"
by (auto elim!: resolve.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C', γ')›
unfolding option.cases
proof (intro impI)
from step have "state_conflict S ≠ None"
by (auto elim: resolve.cases)

assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
"propagate N β S0 S1" "regular_scl N β S0 S1" and
"conflict N β S1 S2" "regular_scl N β S1 S2" and
"(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis

then show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
proof (intro exI conjI)
show "S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
using maybe_reso step
by (metis (no_types, opaque_lifting) rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl
sup2I2)
qed
qed
qed

lemma backtrack_preserves_regular_conflict_resolution:
assumes step: "backtrack N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ where
"state_conflict S = Some (C, γ)" and "state_conflict S' = None"
by (auto elim!: backtrack.cases)

show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = None›
unfolding option.case
proof (rule impI)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis

from reg_run propa(2) confl(2) facto(2) have reg_run_S3: "(regular_scl N β)⇧*⇧* initial_state S3"
by simp

show "(regular_scl N β)⇧*⇧* initial_state S'"
using maybe_reso
proof (elim disjE exE conjE)
show "S3 = S ⟹ (regular_scl N β)⇧*⇧* initial_state S'"
using reg_run_S3 reg_step by simp
next
fix S4 assume hyps: "resolve N β S3 S4" "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
have "(regular_scl N β)⇧*⇧* initial_state S4"
using reg_run_S3 regular_scl_if_resolve[OF hyps(1)]
by (rule rtranclp.rtrancl_into_rtrancl)
also have "(regular_scl N β)⇧*⇧* S4 S"
using hyps(2)
by (rule mono_rtranclp[rule_format, rotated]) auto
also have "(regular_scl N β)⇧*⇧* S S'"
using reg_step by simp
finally show "(regular_scl N β)⇧*⇧* initial_state S'"
by assumption
qed
qed
qed

lemma regular_scl_preserves_regular_conflict_resolution:
assumes reg_step: "regular_scl N β S S'" and
invars: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
using assms
using propagate_preserves_regular_conflict_resolution decide_preserves_regular_conflict_resolution
conflict_preserves_regular_conflict_resolution skip_preserves_regular_conflict_resolution
factorize_preserves_regular_conflict_resolution resolve_preserves_regular_conflict_resolution
backtrack_preserves_regular_conflict_resolution
by (metis regular_scl_def reasonable_scl_def scl_def)

subsection ‹Miscellaneous Lemmas›

lemma mempty_not_in_initial_clauses_if_non_empty_regular_conflict:
assumes "state_conflict S = Some (C, γ)" and "C ≠ {#}" and
invars: "almost_no_conflict_with_trail N β S" "sound_state N β S" "ground_false_closures S"
shows "{#} |∉| N"
proof -
from assms(1) obtain Γ U where S_def: "S = (Γ, U, Some (C, γ))"
by (metis state_simp)

from assms(2) obtain L C' where C_def: "C = add_mset L C'"
using multi_nonempty_split by metis

from invars(3) have "trail_false_cls Γ (C ⋅ γ)"
then obtain Ln Γ' where "Γ = Ln # Γ'"
by (metis assms(2) neq_Nil_conv not_trail_false_Nil(2) subst_cls_empty_iff)
with invars(1) have "no_conflict_with_trail N β U (if is_decision_lit Ln then Ln # Γ' else Γ')"
hence "∄S'. conflict N β ([], U, None) S'"
by (rule nex_conflict_if_no_conflict_with_trail')
hence "{#} |∉| N |∪| U"
unfolding mempty_in_iff_ex_conflict[symmetric] by assumption
thus ?thesis
by simp
qed

lemma mempty_not_in_initial_clauses_if_regular_run_reaches_non_empty_conflict:
assumes "(regular_scl N β)⇧*⇧* initial_state S" and "state_conflict S = Some (C, γ)" and "C ≠ {#}"
shows "{#} |∉| N"
proof (rule notI)
from assms(2) have "initial_state ≠ S" by fastforce
then obtain S' where
reg_scl_init_S': "regular_scl N β initial_state S'" and "(regular_scl N β)⇧*⇧* S' S"
by (metis assms(1) converse_rtranclpE)

assume "{#} |∈| N"
hence "conflict N β initial_state ([], {||}, Some ({#}, Var))"
by (rule conflict_initial_state_if_mempty_in_intial_clauses)
hence conf_init: "regular_scl N β initial_state ([], {||}, Some ({#}, Var))"
using regular_scl_def by blast
then obtain γ where S'_def: "S' = ([], {||}, Some ({#}, γ))"
using reg_scl_init_S'
unfolding regular_scl_def
using ‹conflict N β initial_state ([], {||}, Some ({#}, Var))›
conflict_initial_state_only_with_mempty
by blast

have "∄S'. scl N β ([], {||}, Some ({#}, γ)) S'" for γ
using no_more_step_if_conflict_mempty by simp
hence "∄S'. regular_scl N β ([], {||}, Some ({#}, γ)) S'" for γ
using scl_if_reasonable[OF reasonable_if_regular] by blast
hence "S = S'"
using ‹(regular_scl N β)⇧*⇧* S' S›
unfolding S'_def
by (metis converse_rtranclpE)
with assms(2,3) show False by (simp add: S'_def)
qed

lemma before_regular_backtrack:
assumes
backt: "backtrack N β S S'" and
invars: "sound_state N β S" "almost_no_conflict_with_trail N β S"
"regular_conflict_resolution N β S" "ground_false_closures S"
shows "∃S0 S1 S2 S3 S4. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ (factorize N β)⇧*⇧* S2 S3 ∧ resolve N β S3 S4 ∧
(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
proof -
from backt obtain L C γ where conflict_S: "state_conflict S = Some (add_mset L C, γ)"
by (auto elim: backtrack.cases)

have "{#} |∉| N"
proof (rule mempty_not_in_initial_clauses_if_non_empty_regular_conflict)
show "state_conflict S = Some (add_mset L C, γ)"
by (rule ‹state_conflict S = Some (add_mset L C, γ)›)
next
show "add_mset L C ≠ {#}"
by simp
next
show "almost_no_conflict_with_trail N β S"
by (rule ‹almost_no_conflict_with_trail N β S›)
next
show "sound_state N β S"
by (rule ‹sound_state N β S›)
next
show "ground_false_closures S"
by (rule ‹ground_false_closures S›)
qed

then obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" and
fact: "(factorize N β)⇧*⇧* S2 S3" and
maybe_resolution: "S3 = S ∨
(∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
using ‹regular_conflict_resolution N β S› ‹state_conflict S = Some (add_mset L C, γ)›
unfolding regular_conflict_resolution_def conflict_S option.case
by metis

have "S3 ≠ S"
proof (rule notI)
from ‹(factorize N β)⇧*⇧* S2 S3› have "state_trail S3 = state_trail S2"
by (induction S3 rule: rtranclp_induct) (auto elim: factorize.cases)
also from ‹conflict N β S1 S2› have "… = state_trail S1"
by (auto elim: conflict.cases)
finally have "state_trail S3 = state_trail S1"
by assumption
from ‹propagate N β S0 S1› obtain L C γ where
"state_trail S1 = trail_propagate (state_trail S0) L C γ"
by (auto elim: propagate.cases)

from ‹(factorize N β)⇧*⇧* S2 S3› have "state_learned S3 = state_learned S2"
proof (induction S3 rule: rtranclp_induct)
case base
show ?case by simp
next
case (step y z)
thus ?case
by (elim factorize.cases) simp
qed
also from ‹conflict N β S1 S2› have "… = state_learned S1"
by (auto elim: conflict.cases)
finally have "state_learned S3 = state_learned S1"
by assumption

from ‹propagate N β S0 S1› have "state_learned S1 = state_learned S0"
by (auto elim: propagate.cases)

assume "S3 = S"
hence no_conf_with_trail: "no_conflict_with_trail N β (state_learned S0) (state_trail S0)"
using ‹almost_no_conflict_with_trail N β S› ‹{#} |∉| N›
‹state_trail S1 = trail_propagate (state_trail S0) L C γ› ‹state_trail S3 = state_trail S1›
‹state_learned S3 = state_learned S1› ‹state_learned S1 = state_learned S0›
by (simp add: almost_no_conflict_with_trail_def propagate_lit_def is_decision_lit_def)
hence "{#} |∉| state_learned S0"
using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict] by simp

have "∃D γ⇩D. state_conflict S2 = Some (D, γ⇩D) ∧ - (L ⋅l γ) ∈# D ⋅ γ⇩D"
using ‹conflict N β S1 S2›
proof (cases N β S1 S2 rule: conflict.cases)
case (conflictI D U γ⇩D Γ)
hence "trail_false_cls (trail_propagate (state_trail S0) L C γ) (D ⋅ γ⇩D)"
using ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by simp

moreover from no_conf_with_trail have "¬ trail_false_cls (state_trail S0) (D ⋅ γ⇩D)"
proof (rule not_trail_false_cls_if_no_conflict_with_trail)
show "D |∈| N |∪| state_learned S0"
using ‹state_learned S1 = state_learned S0› local.conflictI(1) local.conflictI(3)
by fastforce
next
have "{#} |∉| U"
using ‹{#} |∉| state_learned S0› ‹S3 = S› ‹state_learned S3 = state_learned S1›
‹state_learned S1 = state_learned S0›
unfolding conflictI(1,2)
by simp
thus "D ≠ {#}"
using ‹{#} |∉| N› ‹D |∈| N |∪| U›
by auto
next
show "is_ground_cls (D ⋅ γ⇩D)"
by (rule ‹is_ground_cls (D ⋅ γ⇩D)›)
qed

ultimately have "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by (metis subtrail_falseI propagate_lit_def)

moreover have "state_conflict S2 = Some (D, γ⇩D)"
unfolding conflictI(1,2) by simp

ultimately show ?thesis
by metis
qed
then obtain D γ⇩D where "state_conflict S2 = Some (D, γ⇩D)" and "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by metis
with ‹(factorize N β)⇧*⇧* S2 S3›
have "∃D' γ⇩D'. state_conflict S3 = Some (D', γ⇩D') ∧ - (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
proof (induction S3 arbitrary: rule: rtranclp_induct)
case base
thus ?case by simp
next
case (step y z)
then obtain D' γ⇩D' where "state_conflict y = Some (D', γ⇩D')" and "- (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
by auto
then show ?case
using step.hyps(2)
by (metis conflict_set_after_factorization)
qed
with backt ‹S3 = S› show False
using ‹state_trail S3 = state_trail S1›
unfolding ‹S3 = S› ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by (auto simp add: decide_lit_def propagate_lit_def elim!: backtrack.cases)
qed
with maybe_resolution obtain S4 where
"resolve N β S3 S4" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
by metis
show ?thesis
proof (intro exI conjI)
show "(regular_scl N β)⇧*⇧* initial_state S0"
by (rule ‹(regular_scl N β)⇧*⇧* initial_state S0›)
next
show "propagate N β S0 S1"
by (rule ‹propagate N β S0 S1›)
next
show "regular_scl N β S0 S1"
by (rule propa(2))
next
show "conflict N β S1 S2"
by (rule ‹conflict N β S1 S2›)
next
show "(factorize N β)⇧*⇧* S2 S3"
by (rule ‹(factorize N β)⇧*⇧* S2 S3›)
next
show "resolve N β S3 S4"
by (rule ‹resolve N β S3 S4›)
next
show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
by (rule ‹(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S›)
qed
qed

section ‹Resolve in Regular Runs›

lemma resolve_if_conflict_follows_propagate:
assumes
no_conf: "∄S⇩1. conflict N β S⇩0 S⇩1" and
propa: "propagate N β S⇩0 S⇩1" and
conf: "conflict N β S⇩1 S⇩2"
shows "∃S⇩3. resolve N β S⇩2 S⇩3"
using propa
proof (cases N β S⇩0 S⇩1 rule: propagate.cases)
case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
hence S⇩0_def: "S⇩0 = (Γ, U, None)"
by simp

from conf obtain γ⇩D D where
S⇩2_def: "S⇩2 = (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ, U, Some (D, γ⇩D))" and
D_in: "D |∈| N |∪| U" and
gr_D_γ⇩D: "is_ground_cls (D ⋅ γ⇩D)" and
tr_false_Γ_L_μ: "trail_false_cls (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ) (D ⋅ γ⇩D)"
by (elim conflict.cases) (unfold propagateI(1,2), blast)

from no_conf have "¬ trail_false_cls Γ (D ⋅ γ⇩D)"
using gr_D_γ⇩D D_in not_trail_false_ground_cls_if_no_conflict[of N β _ D γ⇩D]
using S⇩0_def by force
with tr_false_Γ_L_μ have "- (L ⋅l μ ⋅l γ) ∈# D ⋅ γ⇩D"
unfolding propagate_lit_def by (metis subtrail_falseI)
then obtain D' L' where D_def: "D = add_mset L' D'" and 1: "L ⋅l μ ⋅l γ = - (L' ⋅l γ⇩D)"
by (metis Melem_subst_cls multi_member_split uminus_of_uminus_id)

define ρ where
"ρ = renaming_wrt {add_mset L C⇩0 ⋅ μ}"

have "is_renaming ρ"
by (metis ρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
hence "∀x. is_Var (ρ x)" and "inj ρ"

have disjoint_vars: "⋀C. vars_cls (C ⋅ ρ) ∩ vars_cls (add_mset L C⇩0 ⋅ μ) = {}"

have "∃μ'. Unification.mgu (atm_of L' ⋅a ρ) (atm_of L ⋅a μ) = Some μ'"
proof (rule ex_mgu_if_subst_eq_subst_and_disj_vars)
have "vars_lit L' ⊆ subst_domain γ⇩D"
using gr_D_γ⇩D[unfolded D_def]
hence "atm_of L' ⋅a ρ ⋅a rename_subst_domain ρ γ⇩D = atm_of L' ⋅a γ⇩D"
by (rule renaming_cancels_rename_subst_domain[OF ‹∀x. is_Var (ρ x)› ‹inj ρ›])
then show "atm_of L' ⋅a ρ ⋅a rename_subst_domain ρ γ⇩D = atm_of L ⋅a μ ⋅a γ"
using 1 by (metis atm_of_subst_lit atm_of_uminus)
next
show "vars_term (atm_of L' ⋅a ρ) ∩ vars_term (atm_of L ⋅a μ) = {}"
using disjoint_vars[of "{#L'#}"] by auto
qed
then obtain μ' where imgu_μ': "is_imgu μ' {{atm_of L' ⋅a ρ, atm_of (L ⋅l μ)}}"
using is_imgu_if_mgu_eq_Some by auto

let ?Γprop = "trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ"
let ?γreso = "λx. if x ∈ vars_cls (add_mset L' D' ⋅ ρ) then rename_subst_domain ρ γ⇩D x else γ x"

have "resolve N β
(?Γprop, U, Some (add_mset L' D', γ⇩D))
(?Γprop, U, Some ((D' ⋅ ρ + C⇩0 ⋅ μ ⋅ Var) ⋅ μ', ?γreso))"
proof (rule resolveI[OF refl])
show "L ⋅l μ ⋅l γ = - (L' ⋅l γ⇩D)"
by (rule 1)
next
show "is_renaming ρ"
by (metis ρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
next
show "vars_cls (add_mset L' D' ⋅ ρ) ∩ vars_cls (add_mset (L ⋅l μ) (C⇩0 ⋅ μ) ⋅ Var) = {}"
using disjoint_vars[of "add_mset L' D'"] by simp
next
show "is_imgu μ' {{atm_of L' ⋅a ρ, atm_of (L ⋅l μ) ⋅a Var}}"
using imgu_μ' by simp
next
show "is_grounding_merge ?γreso
(vars_cls (add_mset L' D' ⋅ ρ)) (rename_subst_domain ρ γ⇩D)
(vars_cls (add_mset (L ⋅l μ) (C⇩0 ⋅ μ) ⋅ Var)) (rename_subst_domain Var γ)"
using is_grounding_merge_if_mem_then_else
by (metis rename_subst_domain_Var_lhs)
qed simp_all
thus ?thesis
unfolding S⇩2_def D_def by metis
qed

lemma factorize_preserves_resolvability:
assumes reso: "resolve N β S⇩1 S⇩2" and fact: "factorize N β S⇩1 S⇩3" and
invar: "ground_closures S⇩1"
shows "∃S⇩4. resolve N β S⇩3 S⇩4"
using reso
proof (cases N β S⇩1 S⇩2 rule: resolve.cases)
case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)

from fact[unfolded resolveI(1,2)] obtain LL' LL CC μ⇩L where
S⇩1_def: "S⇩1 = (Γ, U, Some (add_mset LL' (add_mset LL CC), γ⇩C))" and
S⇩3_def: "S⇩3 = (Γ, U, Some (add_mset LL CC ⋅ μ⇩L, γ⇩C))" and
"LL ⋅l γ⇩C = LL' ⋅l γ⇩C" and
imgu_μ⇩L: "is_imgu μ⇩L {{atm_of LL, atm_of LL'}}"
by (auto simp: ‹S⇩1 = (Γ, U, Some (add_mset L C, γ⇩C))› elim: factorize.cases)

from invar have
ground_conf: "is_ground_cls (add_mset L C ⋅ γ⇩C)"
unfolding resolveI(1,2)

using resolveI(1) S⇩1_def by simp

from imgu_μ⇩L have "μ⇩L ⊙ γ⇩C = γ⇩C"
using ‹LL ⋅l γ⇩C = LL' ⋅l γ⇩C›
by (auto simp: is_imgu_def is_unifiers_def is_unifier_alt intro!: subst_atm_of_eqI)

have "L ⋅l μ⇩L ∈# add_mset LL CC ⋅ μ⇩L"
proof (cases "L = LL ∨ L = LL'")
case True
moreover have "LL ⋅l μ⇩L = LL' ⋅l μ⇩L"
using imgu_μ⇩L[unfolded is_imgu_def, THEN conjunct1, unfolded is_unifiers_def, simplified]
using ‹LL ⋅l γ⇩C = LL' ⋅l γ⇩C›
by (metis (no_types, opaque_lifting) atm_of_subst_lit finite.emptyI finite.insertI insertCI
is_unifier_alt literal.expand subst_lit_is_neg)
ultimately have "L ⋅l μ⇩L = LL ⋅l μ⇩L"
by presburger
thus ?thesis
by simp
next
case False
hence "L ∈# CC"
thus ?thesis
by auto
qed
then obtain CCC where "add_mset LL CC ⋅ μ⇩L = add_mset L CCC ⋅ μ⇩L"

define ρρ where
"ρρ = renaming_wrt {add_mset K D}"

have ren_ρρ: "is_renaming ρρ"
by (metis ρρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)

have disjoint_vars: "⋀C. vars_cls (C ⋅ ρρ) ∩ vars_cls (add_mset K D) = {}"

have "K ⋅l γ⇩D = - (L ⋅l μ⇩L ⋅l γ⇩C)"
proof -
have "L ⋅l μ⇩L ⋅l γ⇩C = L ⋅l γ⇩C"
using ‹μ⇩L ⊙ γ⇩C = γ⇩C›
by (metis subst_lit_comp_subst)
thus ?thesis
using resolveI by simp
qed

have "∃μ. Unification.mgu (atm_of L ⋅a μ⇩L ⋅a ρρ) (atm_of K) = Some μ"
proof (rule ex_mgu_if_subst_eq_subst_and_disj_vars)
show "vars_term (atm_of L ⋅a μ⇩L ⋅a ρρ) ∩ vars_lit K = {}"
using disjoint_vars[of "{#L ⋅l μ⇩L#}"] by auto
next
have "vars_term (atm_of L ⋅a μ⇩L) ⊆ subst_domain γ⇩C"
by (metis ‹μ⇩L ⊙ γ⇩C = γ⇩C› atm_of_subst_lit ground_conf is_ground_cls_add_mset
hence "atm_of L ⋅a μ⇩L ⋅a ρρ ⋅a rename_subst_domain ρρ γ⇩C = atm_of L ⋅a μ⇩L ⋅a γ⇩C"
using ren_ρρ
thus "atm_of L ⋅a μ⇩L ⋅a ρρ ⋅a rename_subst_domain ρρ γ⇩C = atm_of K ⋅a γ⇩D"
using ‹K ⋅l γ⇩D = - (L ⋅l μ⇩L ⋅l γ⇩C)›
by (metis atm_of_subst_lit atm_of_uminus)
qed
then obtain μμ where imgu_μμ: "is_imgu μμ {{atm_of L ⋅a μ⇩L ⋅a ρρ, atm_of K}}"
using is_imgu_if_mgu_eq_Some by auto

show ?thesis
unfolding S⇩3_def ‹add_mset LL CC ⋅ μ⇩L = add_mset L CCC ⋅ μ⇩L›
using resolve.resolveI[OF ‹Γ = trail_propagate Γ' K D γ⇩D› ‹K ⋅l γ⇩D = - (L ⋅l μ⇩L ⋅l γ⇩C)› ren_ρρ
is_renaming_id_subst, unfolded subst_atm_id_subst subst_cls_id_subst atm_of_subst_lit,
OF disjoint_vars imgu_μμ is_grounding_merge_if_mem_then_else, of N β U  "CCC ⋅ μ⇩L"]
by auto
qed

text ‹The following lemma corresponds to Lemma 7 in the paper.›

lemma no_backtrack_after_conflict_if:
assumes conf: "conflict N β S1 S2" and trail_S2: "state_trail S1 = trail_propagate Γ L C γ"
shows "∄S4. backtrack N β S2 S4"
proof -
from trail_S2 conf have "state_trail S2 = trail_propagate Γ L C γ"
unfolding conflict.simps by auto
then show ?thesis
unfolding backtrack.simps propagate_lit_def decide_lit_def
by auto
qed

lemma skip_state_trail: "skip N β S S' ⟹ suffix (state_trail S') (state_trail S)"
by (auto simp: suffix_def elim: skip.cases)

lemma factorize_state_trail: "factorize N β S S' ⟹ state_trail S' = state_trail S"
by (auto elim: factorize.cases)

lemma resolve_state_trail: "resolve N β S S' ⟹ state_trail S' = state_trail S"
by (auto elim: resolve.cases)

assumes
reg_run: "(regular_scl N β)⇧*⇧* initial_state S1" and
trail_lit: "state_trail S1 = Lc # Γ"
shows "{#} |∉| N"
proof (rule notI)
assume "{#} |∈| N"
then obtain γ where "conflict N β initial_state ([], {||}, Some ({#}, γ))"
using conflict_initial_state_if_mempty_in_intial_clauses by auto
moreover hence "∄S'. local.scl N β ([], {||}, Some ({#}, γ)) S'" for γ
using no_more_step_if_conflict_mempty by simp
ultimately show False
using trail_lit
by (metis (no_types, opaque_lifting) conflict_initial_state_only_with_mempty converse_rtranclpE
list.discI prod.sel(1) reasonable_if_regular reg_run regular_scl_def scl_if_reasonable
state_trail_def)
qed

(*
after conflict, one can apply factorize arbitrarily often,
but resolve must be applied at least once.

Prove this lemma!
conflict in reg run ⟹ ALL following runs have the following shape:
factorize* then resolve then (skip or factorize or resolve)*
*)

lemma conflict_with_literal_gets_resolved:
assumes
trail_lit: "state_trail S1 = Lc # Γ" and
conf: "conflict N β S1 S2" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S2 Sn" and
backtrack: "∃Sn'. backtrack N β Sn Sn'" and
mempty_not_in_init_clss: "{#} |∉| N" and
invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1" "no_conflict_after_decide' N β S1"
shows "¬ is_decision_lit Lc ∧ strict_suffix (state_trail Sn) (state_trail S1)"
proof -
obtain S0 where propa: "propagate N β S0 S1"
using mempty_not_in_init_clss before_reasonable_conflict[OF conf ‹learned_nonempty S1›
‹trail_propagated_or_decided' N β S1› ‹no_conflict_after_decide' N β S1›] by metis

from trail_lit propa have "¬ is_decision_lit Lc"
by (auto simp: propagate_lit_def is_decision_lit_def elim!: propagate.cases)

show ?thesis
proof (rule conjI)
show "¬ is_decision_lit Lc"
by (rule ‹¬ is_decision_lit Lc›)
next
show "strict_suffix (state_trail Sn) (state_trail S1)"
unfolding strict_suffix_def
proof (rule conjI)
from conf have "state_trail S2 = state_trail S1"
by (auto elim: conflict.cases)
moreover from resolution have "suffix (state_trail Sn) (state_trail S2)"
proof (induction Sn rule: rtranclp_induct)
case base
thus ?case
by simp
next
case (step y z)
from step.hyps(2) have "suffix (state_trail z) (state_trail y)"
by (auto simp: suffix_def factorize_state_trail resolve_state_trail
dest: skip_state_trail)
with step.IH show ?case
by (auto simp: suffix_def)
qed
ultimately show "suffix (state_trail Sn) (state_trail S1)"
by simp
next
from backtrack ‹¬ is_decision_lit Lc› show "state_trail Sn ≠ state_trail S1"
unfolding trail_lit
by (auto simp: decide_lit_def is_decision_lit_def elim!: backtrack.cases)
qed
qed
qed

section ‹Clause Redundancy›

definition ground_redundant where
"ground_redundant lt N C ⟷ {D ∈ N. lt D C} ⊫e {C}"

definition redundant where
"redundant lt N C ⟷
(∀C' ∈ grounding_of_cls C. ground_redundant lt (grounding_of_clss N) C')"

lemma "redundant lt N C ⟷ (∀C'∈ grounding_of_cls C. {D' ∈ grounding_of_clss N. lt D' C'} ⊫e {C'})"

lemma ground_redundant_iff:
"ground_redundant lt N C ⟷ (∃M ⊆ N. M ⊫e {C} ∧ (∀D ∈ M. lt D C))"
proof (rule iffI)
assume red: "ground_redundant lt N C"
show "∃M⊆N. M ⊫e {C} ∧ (∀D∈M. lt D C)"
proof (intro exI conjI)
show "{D ∈ N. lt D C} ⊆ N"
by simp
next
show "{D ∈ N. lt D C} ⊫e {C}"
using red by (simp add: ground_redundant_def)
next
show "∀D∈{D ∈ N. lt D C}. lt D C"
by simp
qed
next
assume "∃M⊆N. M ⊫e {C} ∧ (∀D∈M. lt D C)"
then show "ground_redundant lt N C"
unfolding ground_redundant_def
by (smt (verit, ccfv_SIG) mem_Collect_eq subset_iff true_clss_mono)
qed

lemma ground_redundant_is_ground_standard_redundancy:
fixes lt
defines "Red_F⇩𝒢 ≡ λN. {C. ground_redundant lt N C}"
shows "Red_F⇩𝒢 N = {C. ∃M ⊆ N. M ⊫e {C} ∧ (∀D ∈ M. lt D C)}"
by (auto simp: Red_F⇩𝒢_def ground_redundant_iff)

lemma redundant_is_standard_redundancy:
fixes lt 𝒢⇩F 𝒢⇩F⇩s Red_F⇩𝒢 Red_F
defines
"𝒢⇩F ≡ grounding_of_cls" and
"𝒢⇩F⇩s ≡ grounding_of_clss" and
"Red_F⇩𝒢 ≡ λN. {C. ground_redundant lt N C}" and
"Red_F ≡ λN. {C. redundant lt N C}"
shows "Red_F N = {C. ∀D ∈ 𝒢⇩F C. D ∈ Red_F⇩𝒢 (𝒢⇩F⇩s N)}"
using Red_F_def Red_F⇩𝒢_def 𝒢⇩F⇩s_def 𝒢⇩F_def redundant_def by auto

lemma ground_redundant_if_strict_subset:
assumes "D ∈ N" and "D ⊂# C"
shows "ground_redundant (multp⇩H⇩O R) N C"
using assms
unfolding ground_redundant_def
by (metis (mono_tags, lifting) CollectI strict_subset_implies_multp⇩H⇩O subset_mset.less_le
true_clss_def true_clss_singleton true_clss_subclause)

lemma redundant_if_strict_subset:
assumes "D ∈ N" and "D ⊂# C"
shows "redundant (multp⇩H⇩O R) N C"
unfolding redundant_def
proof (rule ballI)
fix C' assume "C' ∈ grounding_of_cls C"
then obtain γ where "C' = C ⋅ γ" and "is_ground_subst γ"
by (auto simp: grounding_of_cls_def)

show "ground_redundant (multp⇩H⇩O R) (grounding_of_clss N) C'"
proof (rule ground_redundant_if_strict_subset)
from ‹D ∈ N› show "D ⋅ γ ∈ grounding_of_clss N"
using ‹is_ground_subst γ›
by (auto simp: grounding_of_clss_def grounding_of_cls_def)
next
from ‹D ⊂# C› show "D ⋅ γ ⊂# C'"
by (simp add: ‹C' = C ⋅ γ› subst_subset_mono)
qed
qed

lemma redundant_if_strict_subsumes:
assumes "D ⋅ σ ⊂# C" and "D ∈ N"
shows "redundant (multp⇩H⇩O R) N C"
unfolding redundant_def
proof (rule ballI)
fix C' assume "C' ∈ grounding_of_cls C"
then obtain γ where "C' = C ⋅ γ" and "is_ground_subst γ"
by (auto simp: grounding_of_cls_def)

show "ground_redundant (multp⇩H⇩O R) (grounding_of_clss N) C'"
proof (rule ground_redundant_if_strict_subset)
from ‹D ∈ N› show "D ⋅ σ ⋅ γ ∈ grounding_of_clss N"
using ‹is_ground_subst γ›
by (metis (no_types, lifting) UN_iff ground_subst_ground_cls grounding_of_cls_ground
grounding_of_clss_def insert_subset subst_cls_comp_subst
subst_cls_eq_grounding_of_cls_subset_eq)
next
from ‹D ⋅ σ ⊂# C› show "D ⋅ σ ⋅ γ ⊂# C'"
by (simp add: ‹C' = C ⋅ γ› subst_subset_mono)
qed
qed

lemma ground_redundant_mono_strong:
"ground_redundant R N C ⟹ (⋀x. x ∈ N ⟹ R x C ⟹ S x C) ⟹ ground_redundant S N C"
unfolding ground_redundant_def

lemma redundant_mono_strong:
"redundant R N C ⟹
(⋀x y. x ∈ grounding_of_clss N ⟹ y ∈ grounding_of_cls C ⟹ R x y ⟹ S x y) ⟹
redundant S N C"
by (auto simp: redundant_def
intro: ground_redundant_mono_strong[of R "grounding_of_clss N" _ S])

lemma redundant_multp_if_redundant_strict_subset:
"redundant (⊂#) N C ⟹ redundant (multp⇩H⇩O R) N C"
by (auto intro: strict_subset_implies_multp⇩H⇩O elim!: redundant_mono_strong)

lemma redundant_multp_if_redundant_subset:
"redundant (⊂#) N C ⟹ redundant (multp (trail_less_ex lt Ls)) N C"
by (auto intro: subset_implies_multp elim!: redundant_mono_strong)

lemma not_bex_subset_mset_if_not_ground_redundant:
assumes "is_ground_cls C" and "is_ground_clss N"
shows "¬ ground_redundant (⊂#) N C ⟹ ¬ (∃D ∈ N. D ⊂# C)"
using assms unfolding ground_redundant_def
apply (elim exE conjE)
apply (rule ballI)
subgoal premises prems for I D
using prems(3)[rule_format, of D] prems(1,2,4-)
apply simp
by (meson mset_subset_eqD subset_mset.nless_le)
done

section ‹Trail-Induced Ordering›

subsection ‹Miscellaneous Lemmas›

lemma pairwise_distinct_if_trail_consistent:
fixes Γ
defines "Ls ≡ (map fst Γ)"
shows "trail_consistent Γ ⟹
∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
unfolding Ls_def
proof (induction Γ rule: trail_consistent.induct)
case Nil
show ?case by simp
next
case (Cons Γ L u)
from Cons.hyps have L_distinct:
"∀x < length (map fst Γ). map fst Γ ! x ≠ L"
"∀x < length (map fst Γ). map fst Γ ! x ≠ - L"
unfolding trail_defined_lit_def de_Morgan_disj
unfolding image_set in_set_conv_nth not_ex de_Morgan_conj disj_not1
by simp_all
show ?case
unfolding list.map prod.sel
proof (intro allI impI)
fix i j :: nat
assume i_lt: "i < length (L # map fst Γ)" and j_lt: "j < length (L # map fst Γ)" and "i ≠ j"
show
"(L # map fst Γ) ! i ≠ (L # map fst Γ) ! j ∧
(L # map fst Γ) ! i ≠ - (L # map fst Γ) ! j"
proof (cases i)
case 0
thus ?thesis
using L_distinct ‹i ≠ j› ‹j < length (L # map fst Γ)›
using gr0_conv_Suc by auto
next
case (Suc k)
then show ?thesis
apply simp
using i_lt j_lt ‹i ≠ j› L_distinct Cons.IH[rule_format]
using less_Suc_eq_0_disj by force
qed
qed
qed

subsection ‹Strict Partial Order›

lemma irreflp_trail_less_if_trail_consistant:
"trail_consistent Γ ⟹ irreflp (trail_less (map fst Γ))"
using irreflp_trail_less[OF
Clausal_Logic.uminus_not_id'
Clausal_Logic.uminus_of_uminus_id
pairwise_distinct_if_trail_consistent]
by assumption

lemma transp_trail_less_if_trail_consistant:
"trail_consistent Γ ⟹ transp (trail_less (map fst Γ))"
using transp_trail_less[OF
Clausal_Logic.uminus_not_id'
Clausal_Logic.uminus_of_uminus_id
pairwise_distinct_if_trail_consistent]
by assumption

lemma asymp_trail_less_if_trail_consistant:
"trail_consistent Γ ⟹ asymp (trail_less (map fst Γ))"
using asymp_trail_less[OF
Clausal_Logic.uminus_not_id'
Clausal_Logic.uminus_of_uminus_id
pairwise_distinct_if_trail_consistent]
by assumption

subsection ‹Properties›

lemma trail_defined_lit_if_trail_term_less:
assumes "trail_term_less (map (atm_of o fst) Γ) (atm_of L) (atm_of K)"
shows "trail_defined_lit Γ L" "trail_defined_lit Γ K"
proof -
from assms have "atm_of L ∈ set (map (atm_of o fst) Γ)" and "atm_of K ∈ set (map (atm_of o fst) Γ)"
by (auto simp: trail_term_less_def)
hence "atm_of L ∈ atm_of ` fst ` set Γ" and "atm_of K ∈ atm_of ` fst ` set Γ"
by auto
hence "L ∈ fst ` set Γ ∨ - L ∈ fst ` set Γ" and "K ∈ fst ` set Γ ∨ - K ∈ fst ` set Γ"
thus "trail_defined_lit Γ L" and "trail_defined_lit Γ K"
qed

lemma trail_defined_cls_if_lt_defined:
assumes consistent_Γ: "trail_consistent Γ" and
C_lt_D: "multp⇩H⇩O (lit_less (trail_term_less (map (atm_of o fst) Γ))) C D" and
tr_def_D: "trail_defined_cls Γ D" and
lit_less_preserves_term_order: "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
shows "trail_defined_cls Γ C"
proof -
from multp⇩H⇩O_implies_one_step[OF C_lt_D]
obtain I J K where D_def: "D = I + J" and C_def: "C = I + K" and "J ≠ {#}" and
*: "∀k∈#K. ∃x∈#J. lit_less (trail_term_less (map (atm_of o fst) Γ)) k x"
by auto

show ?thesis
unfolding trail_defined_cls_def
proof (rule ballI)
fix L assume L_in: "L ∈# C"
show "trail_defined_lit Γ L"
proof (cases "L ∈# I")
case True
then show ?thesis
using tr_def_D D_def
next
case False
with C_def L_in have "L ∈# K" by fastforce
then obtain L' where L'_in: "L'∈#J" and "lit_less (trail_term_less (map (atm_of o fst) Γ)) L L'"
using * by blast
hence "(trail_term_less (map (atm_of o fst) Γ))⇧=⇧= (atm_of L) (atm_of L')"
using lit_less_preserves_term_order by metis
thus ?thesis
using trail_defined_lit_if_trail_term_less(1)
by (metis (mono_tags, lifting) D_def L'_in atm_of_eq_atm_of sup2E tr_def_D
trail_defined_cls_def trail_defined_lit_iff_defined_uminus union_iff)
qed
qed
qed

section ‹Dynamic Non-Redundancy›

lemma regular_run_if_skip_factorize_resolve_run:
assumes "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S S'"
shows "(regular_scl N β)⇧*⇧* S S'"
using assms
proof (induction S' rule: rtranclp_induct)
case base
show ?case by simp
next
case (step S' S'')
from step.hyps(2) have "scl N β S' S''"
unfolding scl_def by blast
with step.hyps(2) have "reasonable_scl N β S' S''"
using reasonable_scl_def decide_well_defined(4) decide_well_defined(5) skip_well_defined(2)
by fast
moreover from step.hyps(2) have "¬ Ex (conflict N β S')"
apply simp
by (smt (verit, best) conflict.cases factorize.simps option.distinct(1) resolve.simps skip.simps
state_conflict_simp)
ultimately have "regular_scl N β S' S''"
with step.IH show ?case
by simp
qed

lemma not_trail_true_and_false_lit:
"trail_consistent Γ ⟹ ¬ (trail_true_lit Γ L ∧ trail_false_lit Γ L)"
by (metis (no_types, lifting) in_set_conv_nth list.set_map pairwise_distinct_if_trail_consistent
uminus_not_id')

lemma not_trail_true_and_false_cls:
"trail_consistent Γ ⟹ ¬ (trail_true_cls Γ C ∧ trail_false_cls Γ C)"
using not_trail_true_and_false_lit
by (metis trail_false_cls_def trail_true_cls_def)

fun standard_lit_less where
"standard_lit_less R (Pos t1) (Pos t2) = R t1 t2" |
"standard_lit_less R (Pos t1) (Neg t2) = R⇧=⇧= t1 t2" |
"standard_lit_less R (Neg t1) (Pos t2) = R t1 t2" |
"standard_lit_less R (Neg t1) (Neg t2) = R t1 t2"

lemma ```