[STATEMENT]
lemma InvariantsAfterInitializationStep:
fixes
  state :: State and Phi :: Formula and Vbl::"Variable set"
assumes
  "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)"
  "InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)"
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"
  "InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))"
  "InvariantUniqQ (getQ state)"
  "(getConflictFlag state) \<or> (getQ state) = []"
  "currentLevel (getM state) = 0"
  "finite Vbl"
  "InvariantVarsM (getM state) F0 Vbl"
  "InvariantVarsQ (getQ state) F0 Vbl"
  "InvariantVarsF (getF state) F0 Vbl"
  "state' = initialize Phi state"
  "set Phi \<subseteq> set F0"
shows
  "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>
   InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and>
   InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and>
   InvariantUniqQ (getQ state') \<and>
   InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and>
   InvariantVarsM (getM state') F0 Vbl \<and>
   InvariantVarsQ (getQ state') F0 Vbl \<and>
   InvariantVarsF (getF state') F0 Vbl \<and>
   ((getConflictFlag state') \<or> (getQ state') = []) \<and>
   currentLevel (getM state') = 0" (is "?Inv state'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize Phi state
set Phi \<subseteq> set F0

goal (1 subgoal):
 1. 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
proof (induct Phi arbitrary: state)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize [] state; set [] \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
 2. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize [] state
set [] \<subseteq> set F0

goal (2 subgoals):
 1. \<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize [] state; set [] \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
 2. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize [] state
set [] \<subseteq> set F0

goal (1 subgoal):
 1. 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0

goal (1 subgoal):
 1. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
case (Cons clause Phi')
[PROOF STATE]
proof (state)
this:
\<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); InvariantConflictFlagCharacterization (getConflictFlag ?state) (getF ?state) (getM ?state); InvariantConflictClauseCharacterization (getConflictFlag ?state) (getConflictClause ?state) (getF ?state) (getM ?state); InvariantQCharacterization (getConflictFlag ?state) (getQ ?state) (getF ?state) (getM ?state); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; state' = initialize Phi' ?state; set Phi' \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize (clause # Phi') state
set (clause # Phi') \<subseteq> set F0

goal (1 subgoal):
 1. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
let ?state' = "addClause clause state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
have "?Inv ?state'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<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); InvariantConflictFlagCharacterization (getConflictFlag ?state) (getF ?state) (getM ?state); InvariantConflictClauseCharacterization (getConflictFlag ?state) (getConflictClause ?state) (getF ?state) (getM ?state); InvariantQCharacterization (getConflictFlag ?state) (getQ ?state) (getF ?state) (getM ?state); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; state' = initialize Phi' ?state; set Phi' \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize (clause # Phi') state
set (clause # Phi') \<subseteq> set F0

goal (1 subgoal):
 1. InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0
[PROOF STEP]
using InvariantsAfterAddClause[of "state" "F0" "Vbl" "clause"]
[PROOF STATE]
proof (prove)
using this:
\<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); InvariantConflictFlagCharacterization (getConflictFlag ?state) (getF ?state) (getM ?state); InvariantConflictClauseCharacterization (getConflictFlag ?state) (getConflictClause ?state) (getF ?state) (getM ?state); InvariantQCharacterization (getConflictFlag ?state) (getQ ?state) (getF ?state) (getM ?state); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; state' = initialize Phi' ?state; set Phi' \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize (clause # Phi') state
set (clause # Phi') \<subseteq> set F0
\<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantUniqQ (getQ state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); currentLevel (getM state) = 0; getConflictFlag state \<or> getQ state = []; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; finite Vbl; vars clause \<subseteq> vars F0\<rbrakk> \<Longrightarrow> let state' = addClause clause 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> currentLevel (getM state') = 0 \<and> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0
[PROOF STEP]
using formulaContainsItsClausesVariables[of "clause" "F0"]
[PROOF STATE]
proof (prove)
using this:
\<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); InvariantConflictFlagCharacterization (getConflictFlag ?state) (getF ?state) (getM ?state); InvariantConflictClauseCharacterization (getConflictFlag ?state) (getConflictClause ?state) (getF ?state) (getM ?state); InvariantQCharacterization (getConflictFlag ?state) (getQ ?state) (getF ?state) (getM ?state); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; state' = initialize Phi' ?state; set Phi' \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
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)
InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize (clause # Phi') state
set (clause # Phi') \<subseteq> set F0
\<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantUniqQ (getQ state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); currentLevel (getM state) = 0; getConflictFlag state \<or> getQ state = []; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; finite Vbl; vars clause \<subseteq> vars F0\<rbrakk> \<Longrightarrow> let state' = addClause clause 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantUniqQ (getQ state') \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> currentLevel (getM state') = 0 \<and> (getConflictFlag state' \<or> getQ state' = [])
clause el F0 \<Longrightarrow> vars clause \<subseteq> vars F0

goal (1 subgoal):
 1. InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0

goal (1 subgoal):
 1. \<And>a Phi state. \<lbrakk>\<And>state. \<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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize Phi state; set Phi \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0; 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); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; state' = initialize (a # Phi) state; set (a # Phi) \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0

goal (1 subgoal):
 1. 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
using Cons(1)[of "?state'"] \<open>finite Vbl\<close> Cons(18) Cons(19) Cons(20) Cons(21) Cons(22)
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (addClause clause state)) \<and> InvariantUniq (getM (addClause clause state)) \<and> InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)) \<and> InvariantWatchListsUniq (getWatchList (addClause clause state)) \<and> InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) \<and> InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) \<and> InvariantUniqQ (getQ (addClause clause state)) \<and> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantVarsM (getM (addClause clause state)) F0 Vbl \<and> InvariantVarsQ (getQ (addClause clause state)) F0 Vbl \<and> InvariantVarsF (getF (addClause clause state)) F0 Vbl \<and> (getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []) \<and> currentLevel (getM (addClause clause state)) = 0
\<lbrakk>InvariantConsistent (getM (addClause clause state)); InvariantUniq (getM (addClause clause state)); InvariantWatchListsContainOnlyClausesFromF (getWatchList (addClause clause state)) (getF (addClause clause state)); InvariantWatchListsUniq (getWatchList (addClause clause state)); InvariantWatchListsCharacterization (getWatchList (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)); InvariantWatchesEl (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)); InvariantWatchesDiffer (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)); InvariantWatchCharacterization (getF (addClause clause state)) (getWatch1 (addClause clause state)) (getWatch2 (addClause clause state)) (getM (addClause clause state)); InvariantConflictFlagCharacterization (getConflictFlag (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)); InvariantConflictClauseCharacterization (getConflictFlag (addClause clause state)) (getConflictClause (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)); InvariantQCharacterization (getConflictFlag (addClause clause state)) (getQ (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)); InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))); InvariantUniqQ (getQ (addClause clause state)); getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []; currentLevel (getM (addClause clause state)) = 0; finite Vbl; InvariantVarsM (getM (addClause clause state)) F0 Vbl; InvariantVarsQ (getQ (addClause clause state)) F0 Vbl; InvariantVarsF (getF (addClause clause state)) F0 Vbl; state' = initialize Phi' (addClause clause state); set Phi' \<subseteq> set F0\<rbrakk> \<Longrightarrow> 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
state' = initialize (clause # Phi') state
set (clause # Phi') \<subseteq> set F0

goal (1 subgoal):
 1. 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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
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> InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state') \<and> InvariantQCharacterization (getConflictFlag state') (getQ state') (getF state') (getM state') \<and> InvariantUniqQ (getQ state') \<and> InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state')) \<and> InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl \<and> InvariantVarsF (getF state') F0 Vbl \<and> (getConflictFlag state' \<or> getQ state' = []) \<and> currentLevel (getM state') = 0

goal:
No subgoals!
[PROOF STEP]
qed