[STATEMENT]
lemma InvariantsAfterExhaustiveUnitPropagate:
assumes
  "exhaustiveUnitPropagate_dom state"
  "InvariantConsistent (getM state)"
  "InvariantUniq (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)" and
  "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)"
  "InvariantVarsQ (getQ state) F0 Vbl"
  "InvariantVarsM (getM state) F0 Vbl"
  "InvariantVarsF (getF state) F0 Vbl"
shows
  "let state' = exhaustiveUnitPropagate state in
       InvariantConsistent (getM state') \<and>
       InvariantUniq (getM state') \<and>
       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') \<and>
       InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and>
       InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and>
       InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and>
       InvariantUniqQ (getQ state') \<and>
       InvariantVarsQ (getQ state') F0 Vbl \<and>
       InvariantVarsM (getM state') F0 Vbl \<and>
       InvariantVarsF (getF state') F0 Vbl
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate_dom state
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)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
proof (induct state rule: exhaustiveUnitPropagate_dom.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state)); InvariantUniq (getM (applyUnitPropagate state)); 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)); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state)); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state)) (getQ (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state)); InvariantUniqQ (getQ (applyUnitPropagate state)); InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state)) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl; 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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantUniqQ (getQ state); InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
case (step state')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state)); InvariantUniq (getM (applyUnitPropagate state)); 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)); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state)); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state)) (getQ (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state)); InvariantUniqQ (getQ (applyUnitPropagate state)); InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state)) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl; 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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantUniqQ (getQ state); InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
note ih = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state)); InvariantUniq (getM (applyUnitPropagate state)); 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)); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state)); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state)) (getQ (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state)); InvariantUniqQ (getQ (applyUnitPropagate state)); InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state)) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl; 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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantUniqQ (getQ state); InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
proof (cases "(getConflictFlag state') \<or> (getQ state') = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
getConflictFlag state' \<or> getQ state' = []

goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
with exhaustiveUnitPropagate.simps[of "state'"]
[PROOF STATE]
proof (chain)
picking this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
have "exhaustiveUnitPropagate state' = state'"
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
getConflictFlag state' \<or> getQ state' = []

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

goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = state'

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = state'
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
by (auto simp only: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
let ?state'' = "applyUnitPropagate state'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
have "exhaustiveUnitPropagate state' = exhaustiveUnitPropagate ?state''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
using exhaustiveUnitPropagate.simps[of "state'"]
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
\<not> (getConflictFlag state' \<or> getQ state' = [])

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

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)); InvariantUniq (getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)); 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>)); InvariantWatchCharacterization (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>)) (getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)); InvariantConflictFlagCharacterization (getConflictFlag (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>)) (getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)); InvariantQCharacterization (getConflictFlag (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getQ (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>)) (getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)); InvariantUniqQ (getQ (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)); InvariantVarsQ (getQ (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl; InvariantVarsM (getM (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl; InvariantVarsF (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>) in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); \<not> getConflictFlag (applyUnitPropagate state') \<longrightarrow> (\<forall>l. l el getQ (applyUnitPropagate state') = (\<exists>c. c el getF (applyUnitPropagate state') \<and> isUnitClause c l (elements (getM (applyUnitPropagate state'))))); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> (\<not> getConflictFlag state' \<longrightarrow> (\<forall>l. l el getQ state' = (\<exists>c. c el getF state' \<and> isUnitClause c l (elements (getM state'))))) \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
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')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); \<not> getConflictFlag (applyUnitPropagate state') \<longrightarrow> (\<forall>l. l el getQ (applyUnitPropagate state') = (\<exists>c. c el getF (applyUnitPropagate state') \<and> isUnitClause c l (elements (getM (applyUnitPropagate state'))))); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> (\<not> getConflictFlag state' \<longrightarrow> (\<forall>l. l el getQ state' = (\<exists>c. c el getF state' \<and> isUnitClause c l (elements (getM state'))))) \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
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')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantWatchCharacterization (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. InvariantUniqQ (getQ (applyUnitPropagate state'))
[PROOF STEP]
using InvariantUniqQAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantUniqQ (getQ (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. InvariantConsistent (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantConsistentAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. InvariantUniq (getM (applyUnitPropagate state'))
[PROOF STEP]
using InvariantUniqAfterApplyUnitPropagate[of "state'"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantUniq (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl &&& InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl
[PROOF STEP]
using \<open>\<not> (getConflictFlag state' \<or> getQ state' = [])\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
\<not> (getConflictFlag state' \<or> getQ 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:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
\<not> (getConflictFlag state' \<or> getQ 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl
InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[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'))
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 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 (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
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
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
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

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
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
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
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
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantConsistent (getM (applyUnitPropagate state')); InvariantUniq (getM (applyUnitPropagate state')); 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')); InvariantConflictFlagCharacterization (getConflictFlag (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantQCharacterization (getConflictFlag (applyUnitPropagate state')) (getQ (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state')); InvariantUniqQ (getQ (applyUnitPropagate state')); InvariantVarsQ (getQ (applyUnitPropagate state')) F0 Vbl; InvariantVarsM (getM (applyUnitPropagate state')) F0 Vbl; InvariantVarsF (getF (applyUnitPropagate state')) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
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')
InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state')
InvariantUniqQ (getQ state')
InvariantVarsQ (getQ state') F0 Vbl
InvariantVarsM (getM state') F0 Vbl
InvariantVarsF (getF state') F0 Vbl
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in InvariantConsistent (getM state') \<and> InvariantUniq (getM state') \<and> 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') \<and> InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state') \<and> InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl

goal:
No subgoals!
[PROOF STEP]
qed