[STATEMENT]
lemma exhaustiveUnitPropagateTermination:
fixes
  state::State and Vbl::"Variable set"
assumes
  "InvariantUniq (getM state)"
  "InvariantConsistent (getM state)"
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantWatchListsUniq (getWatchList state)" and
  "InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)"
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)"
  "InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)"
  "InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)"
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"
  "InvariantUniqQ (getQ state)"
  "InvariantVarsM (getM state) F0 Vbl"
  "InvariantVarsQ (getQ state) F0 Vbl"
  "InvariantVarsF (getF state) F0 Vbl"
  "finite Vbl"
shows
  "exhaustiveUnitPropagate_dom state"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantUniq (getM state)
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
finite Vbl

goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state
[PROOF STEP]
proof (induct rule: wf_induct[of "lexLessState (vars F0 \<union> Vbl)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf (lexLessState (vars F0 \<union> Vbl))
 2. \<And>x. \<lbrakk>\<forall>y. (y, x) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y; InvariantUniq (getM x); InvariantConsistent (getM x); InvariantWatchListsContainOnlyClausesFromF (getWatchList x) (getF x); InvariantWatchListsUniq (getWatchList x); InvariantWatchListsCharacterization (getWatchList x) (getWatch1 x) (getWatch2 x); InvariantWatchesEl (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchesDiffer (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchCharacterization (getF x) (getWatch1 x) (getWatch2 x) (getM x); InvariantConflictFlagCharacterization (getConflictFlag x) (getF x) (getM x); InvariantQCharacterization (getConflictFlag x) (getQ x) (getF x) (getM x); InvariantUniqQ (getQ x); InvariantVarsM (getM x) F0 Vbl; InvariantVarsQ (getQ x) F0 Vbl; InvariantVarsF (getF x) F0 Vbl; finite Vbl\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. wf (lexLessState (vars F0 \<union> Vbl))
 2. \<And>x. \<lbrakk>\<forall>y. (y, x) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y; InvariantUniq (getM x); InvariantConsistent (getM x); InvariantWatchListsContainOnlyClausesFromF (getWatchList x) (getF x); InvariantWatchListsUniq (getWatchList x); InvariantWatchListsCharacterization (getWatchList x) (getWatch1 x) (getWatch2 x); InvariantWatchesEl (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchesDiffer (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchCharacterization (getF x) (getWatch1 x) (getWatch2 x) (getM x); InvariantConflictFlagCharacterization (getConflictFlag x) (getF x) (getM x); InvariantQCharacterization (getConflictFlag x) (getQ x) (getF x) (getM x); InvariantUniqQ (getQ x); InvariantVarsM (getM x) F0 Vbl; InvariantVarsQ (getQ x) F0 Vbl; InvariantVarsF (getF x) F0 Vbl; finite Vbl\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (lexLessState (vars F0 \<union> Vbl))
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> y \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> y \<notin> Q)
[PROOF STEP]
show "\<forall>Q (state::State). state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
fix Q :: "State set" and state :: State
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
assume "state \<in> Q"
[PROOF STATE]
proof (state)
this:
state \<in> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
let ?Q1 = "{M::LiteralTrail. \<exists> state. state \<in> Q \<and> (getM state) = M}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
from \<open>state \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
state \<in> Q
[PROOF STEP]
have "getM state \<in> ?Q1"
[PROOF STATE]
proof (prove)
using this:
state \<in> Q

goal (1 subgoal):
 1. getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
have "wf (lexLessRestricted (vars F0 \<union> Vbl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (lexLessRestricted (vars F0 \<union> Vbl))
[PROOF STEP]
using \<open>finite Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
finite Vbl

goal (1 subgoal):
 1. wf (lexLessRestricted (vars F0 \<union> Vbl))
[PROOF STEP]
using finiteVarsFormula[of "F0"]
[PROOF STATE]
proof (prove)
using this:
finite Vbl
finite (vars F0)

goal (1 subgoal):
 1. wf (lexLessRestricted (vars F0 \<union> Vbl))
[PROOF STEP]
using  wfLexLessRestricted[of "vars F0 \<union> Vbl"]
[PROOF STATE]
proof (prove)
using this:
finite Vbl
finite (vars F0)
finite (vars F0 \<union> Vbl) \<Longrightarrow> wf (lexLessRestricted (vars F0 \<union> Vbl))

goal (1 subgoal):
 1. wf (lexLessRestricted (vars F0 \<union> Vbl))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf (lexLessRestricted (vars F0 \<union> Vbl))

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
with \<open>getM state \<in> ?Q1\<close>
[PROOF STATE]
proof (chain)
picking this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}
wf (lexLessRestricted (vars F0 \<union> Vbl))
[PROOF STEP]
obtain Mmin where "Mmin \<in> ?Q1" "\<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> ?Q1"
[PROOF STATE]
proof (prove)
using this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}
wf (lexLessRestricted (vars F0 \<union> Vbl))

goal (1 subgoal):
 1. (\<And>Mmin. \<lbrakk>Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}; \<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
using this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}
\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> y \<notin> Q)

goal (1 subgoal):
 1. (\<And>Mmin. \<lbrakk>Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}; \<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (erule_tac x="?Q1" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>Mmin. \<lbrakk>Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}; \<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis; getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}; \<forall>x. x \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M} \<longrightarrow> (\<exists>z\<in>{M. \<exists>state. state \<in> Q \<and> getM state = M}. \<forall>y. (y, z) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> y \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M})\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule_tac x="getM state" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>Mmin. \<lbrakk>Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}; \<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis; getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}; getM state \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M} \<longrightarrow> (\<exists>z\<in>{M. \<exists>state. state \<in> Q \<and> getM state = M}. \<forall>y. (y, z) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> y \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M})\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}
\<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
from \<open>Mmin \<in> ?Q1\<close>
[PROOF STATE]
proof (chain)
picking this:
Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}
[PROOF STEP]
obtain stateMin
          where "stateMin \<in> Q" "(getM stateMin) = Mmin"
[PROOF STATE]
proof (prove)
using this:
Mmin \<in> {M. \<exists>state. state \<in> Q \<and> getM state = M}

goal (1 subgoal):
 1. (\<And>stateMin. \<lbrakk>stateMin \<in> Q; getM stateMin = Mmin\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stateMin \<in> Q
getM stateMin = Mmin

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
have "\<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q
[PROOF STEP]
fix state'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q
[PROOF STEP]
show "(state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
assume "(state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl)"
[PROOF STATE]
proof (state)
this:
(state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl)

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "(getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)"
[PROOF STATE]
proof (prove)
using this:
(state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl)

goal (1 subgoal):
 1. (getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)
[PROOF STEP]
unfolding lexLessState_def
[PROOF STATE]
proof (prove)
using this:
(state', stateMin) \<in> {(state1, state2). (getM state1, getM state2) \<in> lexLessRestricted (vars F0 \<union> Vbl)}

goal (1 subgoal):
 1. (getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
from \<open>\<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> ?Q1\<close>
              \<open>(getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)\<close> \<open>getM stateMin = Mmin\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}
(getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)
getM stateMin = Mmin
[PROOF STEP]
have "getM state' \<notin> ?Q1"
[PROOF STATE]
proof (prove)
using this:
\<forall>M'. (M', Mmin) \<in> lexLessRestricted (vars F0 \<union> Vbl) \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}
(getM state', getM stateMin) \<in> lexLessRestricted (vars F0 \<union> Vbl)
getM stateMin = Mmin

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
with \<open>getM stateMin = Mmin\<close>
[PROOF STATE]
proof (chain)
picking this:
getM stateMin = Mmin
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}
[PROOF STEP]
show "state' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
getM stateMin = Mmin
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getM state = M}

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
with \<open>stateMin \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
stateMin \<in> Q
\<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q
[PROOF STEP]
have "\<exists> stateMin \<in> Q. (\<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)"
[PROOF STATE]
proof (prove)
using this:
stateMin \<in> Q
\<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?statea2 \<in> ?Q2 \<Longrightarrow> \<exists>stateMin\<in>?Q2. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?statea2 \<in> ?Q2 \<Longrightarrow> \<exists>stateMin\<in>?Q2. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> state' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf (lexLessState (vars F0 \<union> Vbl))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (y, x) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y; InvariantUniq (getM x); InvariantConsistent (getM x); InvariantWatchListsContainOnlyClausesFromF (getWatchList x) (getF x); InvariantWatchListsUniq (getWatchList x); InvariantWatchListsCharacterization (getWatchList x) (getWatch1 x) (getWatch2 x); InvariantWatchesEl (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchesDiffer (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchCharacterization (getF x) (getWatch1 x) (getWatch2 x) (getM x); InvariantConflictFlagCharacterization (getConflictFlag x) (getF x) (getM x); InvariantQCharacterization (getConflictFlag x) (getQ x) (getF x) (getM x); InvariantUniqQ (getQ x); InvariantVarsM (getM x) F0 Vbl; InvariantVarsQ (getQ x) F0 Vbl; InvariantVarsF (getF x) F0 Vbl; finite Vbl\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (y, x) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y; InvariantUniq (getM x); InvariantConsistent (getM x); InvariantWatchListsContainOnlyClausesFromF (getWatchList x) (getF x); InvariantWatchListsUniq (getWatchList x); InvariantWatchListsCharacterization (getWatchList x) (getWatch1 x) (getWatch2 x); InvariantWatchesEl (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchesDiffer (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchCharacterization (getF x) (getWatch1 x) (getWatch2 x) (getM x); InvariantConflictFlagCharacterization (getConflictFlag x) (getF x) (getM x); InvariantQCharacterization (getConflictFlag x) (getQ x) (getF x) (getM x); InvariantUniqQ (getQ x); InvariantVarsM (getM x) F0 Vbl; InvariantVarsQ (getQ x) F0 Vbl; InvariantVarsF (getF x) F0 Vbl; finite Vbl\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom x
[PROOF STEP]
case (2 state')
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (y, x) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y; InvariantUniq (getM x); InvariantConsistent (getM x); InvariantWatchListsContainOnlyClausesFromF (getWatchList x) (getF x); InvariantWatchListsUniq (getWatchList x); InvariantWatchListsCharacterization (getWatchList x) (getWatch1 x) (getWatch2 x); InvariantWatchesEl (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchesDiffer (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchCharacterization (getF x) (getWatch1 x) (getWatch2 x) (getM x); InvariantConflictFlagCharacterization (getConflictFlag x) (getF x) (getM x); InvariantQCharacterization (getConflictFlag x) (getQ x) (getF x) (getM x); InvariantUniqQ (getQ x); InvariantVarsM (getM x) F0 Vbl; InvariantVarsQ (getQ x) F0 Vbl; InvariantVarsF (getF x) F0 Vbl; finite Vbl\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom x
[PROOF STEP]
note ih = this
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (y, x) \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y; InvariantUniq (getM x); InvariantConsistent (getM x); InvariantWatchListsContainOnlyClausesFromF (getWatchList x) (getF x); InvariantWatchListsUniq (getWatchList x); InvariantWatchListsCharacterization (getWatchList x) (getWatch1 x) (getWatch2 x); InvariantWatchesEl (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchesDiffer (getF x) (getWatch1 x) (getWatch2 x); InvariantWatchCharacterization (getF x) (getWatch1 x) (getWatch2 x) (getM x); InvariantConflictFlagCharacterization (getConflictFlag x) (getF x) (getM x); InvariantQCharacterization (getConflictFlag x) (getQ x) (getF x) (getM x); InvariantUniqQ (getQ x); InvariantVarsM (getM x) F0 Vbl; InvariantVarsQ (getQ x) F0 Vbl; InvariantVarsF (getF x) F0 Vbl; finite Vbl\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state'
[PROOF STEP]
proof (cases "getQ state' = [] \<or> getConflictFlag state'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
let ?state'' = "applyUnitPropagate state'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state'') (getF ?state'')" and
      "InvariantWatchListsUniq (getWatchList ?state'')" and
      "InvariantWatchListsCharacterization (getWatchList ?state'') (getWatch1 ?state'') (getWatch2 ?state'')"
      "InvariantWatchesEl (getF ?state'') (getWatch1 ?state'') (getWatch2 ?state'')" and
      "InvariantWatchesDiffer (getF ?state'') (getWatch1 ?state'') (getWatch2 ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')) &&& InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))) &&& (InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) &&& InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))) &&& InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. (InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')) &&& InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))) &&& (InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) &&& InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))) &&& InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
[PROOF STEP]
using WatchInvariantsAfterAssertLiteral[of "state'" "hd (getQ state')" "False"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state')) False state' in InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state') \<and> InvariantWatchListsUniq (getWatchList state') \<and> InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state') \<and> InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state') \<and> InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')

goal (1 subgoal):
 1. (InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')) &&& InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))) &&& (InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) &&& InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))) &&& InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state')) False state' in InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state') \<and> InvariantWatchListsUniq (getWatchList state') \<and> InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state') \<and> InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state') \<and> InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')

goal (1 subgoal):
 1. (InvariantWatchListsContainOnlyClausesFromF (getWatchList (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) &&& InvariantWatchListsUniq (getWatchList (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>))) &&& (InvariantWatchListsCharacterization (getWatchList (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch1 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch2 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) &&& InvariantWatchesEl (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch1 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch2 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>))) &&& InvariantWatchesDiffer (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch1 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch2 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantWatchCharacterization (getF ?state'') (getWatch1 ?state'') (getWatch2 ?state'') (getM ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantWatchCharacterizationAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantUniq (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')

goal (1 subgoal):
 1. InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
unfolding InvariantQCharacterization_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> (\<not> getConflictFlag y \<longrightarrow> (\<forall>l. l el getQ y = (\<exists>c. c el getF y \<and> isUnitClause c l (elements (getM y))))) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
\<not> getConflictFlag state' \<longrightarrow> (\<forall>l. l el getQ state' = (\<exists>c. c el getF state' \<and> isUnitClause c l (elements (getM state'))))
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantUniq (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); \<not> getConflictFlag state' \<longrightarrow> (\<forall>l. l el getQ state' = (\<exists>c. c el getF state' \<and> isUnitClause c l (elements (getM state')))); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')

goal (1 subgoal):
 1. InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> (\<not> getConflictFlag y \<longrightarrow> (\<forall>l. l el getQ y = (\<exists>c. c el getF y \<and> isUnitClause c l (elements (getM y))))) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
\<not> getConflictFlag state' \<longrightarrow> (\<forall>l. l el getQ state' = (\<exists>c. c el getF state' \<and> isUnitClause c l (elements (getM state'))))
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantUniq (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); \<not> getConflictFlag state' \<longrightarrow> (\<forall>l. l el getQ state' = (\<exists>c. c el getF state' \<and> isUnitClause c l (elements (getM state')))); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantQCharacterization (getConflictFlag ?state'') (getQ ?state'') (getF ?state'') (getM ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantQCharacterizationAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); InvariantUniqQ (getQ state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state'' = applyUnitPropagate state' in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')

goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); InvariantUniqQ (getQ state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state'' = applyUnitPropagate state' in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantConflictFlagCharacterization (getConflictFlag ?state'') (getF ?state'') (getM ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantConflictFlagCharacterizationAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantUniq (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state'); \<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')

goal (1 subgoal):
 1. InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantUniq (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state'); \<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantUniqQ (getQ ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniqQ (getQ (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantUniqQ (getQ (applyUnitPropagate state'))
[PROOF STEP]
using InvariantUniqQAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantUniqQ (getQ state'); getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state'' = applyUnitPropagate state' in InvariantUniqQ (getQ state'')

goal (1 subgoal):
 1. InvariantUniqQ (getQ (applyUnitPropagate state'))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantUniqQ (getQ state'); getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state'' = applyUnitPropagate state' in InvariantUniqQ (getQ state'')
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantUniqQ (getQ (applyUnitPropagate state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantUniqQ (getQ (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantUniqQ (getQ (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantConsistent (getM ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConsistent (getM (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantConsistent (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantConsistentAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantConsistent (getM state')

goal (1 subgoal):
 1. InvariantConsistent (getM (applyUnitPropagate state'))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantConsistent (getM state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantConsistent (getM state')
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantConsistent (getM (applyUnitPropagate state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantUniq (getM ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniq (getM (applyUnitPropagate state'))
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantUniq (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantUniqAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantUniq (getM state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantUniq (getM state')

goal (1 subgoal):
 1. InvariantUniq (getM (applyUnitPropagate state'))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantUniq (getM state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state'); getQ state' \<noteq> []; \<not> getConflictFlag state'\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantUniq (getM state')
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantUniq (getM (applyUnitPropagate state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantUniq (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantUniq (getM (applyUnitPropagate state'))

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantVarsM (getM ?state'') F0 Vbl" "InvariantVarsQ (getQ ?state'') F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl &&& InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl &&& InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
[PROOF STEP]
using \<open>\<not> (getQ state' = [] \<or> getConflictFlag state')\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl &&& InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
[PROOF STEP]
using InvariantsVarsAfterApplyUnitPropagate[of "state'" "F0" "Vbl"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<not> (getQ state' = [] \<or> getConflictFlag state')
\<lbrakk>InvariantConsistent (getM state'); InvariantUniq (getM state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state'); InvariantWatchListsUniq (getWatchList state'); InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state'); InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state'); InvariantQCharacterization False (getQ state') (getF state') (getM state'); getQ state' \<noteq> []; \<not> getConflictFlag state'; InvariantVarsM (getM state') F0 Vbl; InvariantVarsQ (getQ state') F0 Vbl; InvariantVarsF (getF state') F0 Vbl\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state' in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl &&& InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "InvariantVarsF (getF ?state'') F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsF (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl
[PROOF STEP]
using assertLiteralEffect[of "state'" "hd (getQ state')" "False"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state')) False state') = getM state' @ [(hd (getQ state'), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state')) False state') = getF state'
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state')) False state') = getSATFlag state'
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> isPrefix (getQ state') (getQ (assertLiteral (hd (getQ state')) False state'))

goal (1 subgoal):
 1. InvariantVarsF (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state')) False state') = getM state' @ [(hd (getQ state'), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state')) False state') = getF state'
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state')) False state') = getSATFlag state'
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> isPrefix (getQ state') (getQ (assertLiteral (hd (getQ state')) False state'))
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. InvariantVarsF (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
have "(?state'', state') \<in> lexLessState (vars F0 \<union> Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)
[PROOF STEP]
have "getM ?state'' = getM state' @ [(hd (getQ state'), False)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getM state' @ [(hd (getQ state'), False)]
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getM state' @ [(hd (getQ state'), False)]
[PROOF STEP]
using assertLiteralEffect[of "state'" "hd (getQ state')" "False"]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state')) False state') = getM state' @ [(hd (getQ state'), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state')) False state') = getF state'
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state')) False state') = getSATFlag state'
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state'); InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')\<rbrakk> \<Longrightarrow> isPrefix (getQ state') (getQ (assertLiteral (hd (getQ state')) False state'))

goal (1 subgoal):
 1. getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getM state' @ [(hd (getQ state'), False)]
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)
[PROOF STEP]
unfolding lexLessState_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> lexLessRestricted (vars F0 \<union> Vbl)}
[PROOF STEP]
unfolding lexLessRestricted_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using lexLessAppend[of "[(hd (getQ state'), False)]" "getM state'"]
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using \<open>InvariantConsistent (getM ?state'')\<close>
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
InvariantConsistent (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using \<open>InvariantConsistent (getM state')\<close>
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
InvariantConsistent (getM state')

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using \<open>InvariantUniq (getM ?state'')\<close>
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
InvariantUniq (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
uniq (elements (getM (applyUnitPropagate state')))

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using \<open>InvariantUniq (getM state')\<close>
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
uniq (elements (getM (applyUnitPropagate state')))
InvariantUniq (getM state')

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
uniq (elements (getM (applyUnitPropagate state')))
uniq (elements (getM state'))

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using \<open>InvariantVarsM (getM ?state'') F0 Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
uniq (elements (getM (applyUnitPropagate state')))
uniq (elements (getM state'))
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
using \<open>InvariantVarsM (getM state') F0 Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
uniq (elements (getM (applyUnitPropagate state')))
uniq (elements (getM state'))
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsM (getM state') F0 Vbl

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
unfolding InvariantVarsM_def
[PROOF STATE]
proof (prove)
using this:
getM (applyUnitPropagate state') = getM state' @ [(hd (getQ state'), False)]
[(hd (getQ state'), False)] \<noteq> [] \<Longrightarrow> (getM state' @ [(hd (getQ state'), False)], getM state') \<in> lexLess
consistent (elements (getM (applyUnitPropagate state')))
consistent (elements (getM state'))
uniq (elements (getM (applyUnitPropagate state')))
uniq (elements (getM state'))
vars (elements (getM (applyUnitPropagate state'))) \<subseteq> vars F0 \<union> Vbl
vars (elements (getM state')) \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. (applyUnitPropagate state', state') \<in> {(state1, state2). (getM state1, getM state2) \<in> {(M1, M2). vars (elements M1) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> vars F0 \<union> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantUniqQ (getQ (applyUnitPropagate state'))
InvariantConsistent (getM (applyUnitPropagate state'))
InvariantUniq (getM (applyUnitPropagate state'))
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl
(applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)
[PROOF STEP]
have "exhaustiveUnitPropagate_dom ?state''"
[PROOF STATE]
proof (prove)
using this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantUniqQ (getQ (applyUnitPropagate state'))
InvariantConsistent (getM (applyUnitPropagate state'))
InvariantUniq (getM (applyUnitPropagate state'))
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl
(applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)

goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom (applyUnitPropagate state')
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
InvariantUniqQ (getQ (applyUnitPropagate state'))
InvariantConsistent (getM (applyUnitPropagate state'))
InvariantUniq (getM (applyUnitPropagate state'))
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl
(applyUnitPropagate state', state') \<in> lexLessState (vars F0 \<union> Vbl)
\<forall>y. (y, state') \<in> lexLessState (vars F0 \<union> Vbl) \<longrightarrow> InvariantUniq (getM y) \<longrightarrow> InvariantConsistent (getM y) \<longrightarrow> InvariantWatchListsContainOnlyClausesFromF (getWatchList y) (getF y) \<longrightarrow> InvariantWatchListsUniq (getWatchList y) \<longrightarrow> InvariantWatchListsCharacterization (getWatchList y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesEl (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchesDiffer (getF y) (getWatch1 y) (getWatch2 y) \<longrightarrow> InvariantWatchCharacterization (getF y) (getWatch1 y) (getWatch2 y) (getM y) \<longrightarrow> InvariantConflictFlagCharacterization (getConflictFlag y) (getF y) (getM y) \<longrightarrow> InvariantQCharacterization (getConflictFlag y) (getQ y) (getF y) (getM y) \<longrightarrow> InvariantUniqQ (getQ y) \<longrightarrow> InvariantVarsM (getM y) F0 Vbl \<longrightarrow> InvariantVarsQ (getQ y) F0 Vbl \<longrightarrow> InvariantVarsF (getF y) F0 Vbl \<longrightarrow> finite Vbl \<longrightarrow> exhaustiveUnitPropagate_dom y
InvariantUniq (getM state')
InvariantConsistent (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsM (getM state') F0 Vbl
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
finite Vbl

goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom (applyUnitPropagate state')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate_dom (applyUnitPropagate state')

goal (2 subgoals):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
 2. \<not> (getQ state' = [] \<or> getConflictFlag state') \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate_dom (applyUnitPropagate state')

goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state'
[PROOF STEP]
using exhaustiveUnitPropagate_dom.intros[of "state'"]
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate_dom (applyUnitPropagate state')
(\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')) \<Longrightarrow> exhaustiveUnitPropagate_dom state'

goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state'
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate_dom (applyUnitPropagate state')
(\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')) \<Longrightarrow> exhaustiveUnitPropagate_dom state'
\<not> (getQ state' = [] \<or> getConflictFlag state')

goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate_dom state'

goal (1 subgoal):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
getQ state' = [] \<or> getConflictFlag state'

goal (1 subgoal):
 1. getQ state' = [] \<or> getConflictFlag state' \<Longrightarrow> exhaustiveUnitPropagate_dom state'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustiveUnitPropagate_dom state'
[PROOF STEP]
apply (rule exhaustiveUnitPropagate_dom.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
getQ state' = [] \<or> getConflictFlag state'

goal (1 subgoal):
 1. \<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate_dom state'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate_dom state'

goal:
No subgoals!
[PROOF STEP]
qed