[STATEMENT]
lemma InvariantEquivalentZLAfterInitializationStep:
fixes Phi :: Formula
assumes
  "(getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda> c. \<not> clauseTautology c) Phi)) \<or>
   (getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda> c. \<not> clauseTautology c) Phi))"
  "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)"
  "InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))"
  "InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))"
  "InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))"
  "InvariantUniqQ (getQ state)"
  "finite Vbl"
  "InvariantVarsM (getM state) F0 Vbl"
  "InvariantVarsQ (getQ state) F0 Vbl"
  "InvariantVarsF (getF state) F0 Vbl"
  "(getConflictFlag state) \<or> (getQ state) = []"
  "currentLevel (getM state) = 0"
  "F0 = Phi @ Phi'"
shows
  "let state' = initialize Phi' state in
     (getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda> c. \<not> clauseTautology c) F0)) \<or>
     (getSATFlag state' = FALSE \<and> \<not>satisfiable (filter (\<lambda> c. \<not> clauseTautology c) F0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ Phi'

goal (1 subgoal):
 1. let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
proof (induct Phi' arbitrary: state Phi)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ []\<rbrakk> \<Longrightarrow> let state' = initialize [] state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
 2. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ []

goal (2 subgoals):
 1. \<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ []\<rbrakk> \<Longrightarrow> let state' = initialize [] state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
 2. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ []

goal (1 subgoal):
 1. let state' = initialize [] state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
unfolding prefixToLevel_def equivalentFormulae_def
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ []

goal (1 subgoal):
 1. let state' = initialize [] state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
let state' = initialize [] state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)

goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
case (Cons clause Phi'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''

goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
let ?filt = "\<lambda> F. (filter (\<lambda> c. \<not> clauseTautology c) F)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
let ?state' = "addClause clause state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
let ?Phi' = "?filt Phi @ [clause]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
let ?Phi'' = "if clauseTautology clause then ?filt Phi else ?Phi'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''
[PROOF STEP]
have "getSATFlag ?state' = UNDEF \<and> InvariantEquivalentZL (getF ?state') (getM ?state') (?filt ?Phi'') \<or>
        getSATFlag ?state' = FALSE \<and> \<not> satisfiable (?filt ?Phi'')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''

goal (1 subgoal):
 1. getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause]))
[PROOF STEP]
using formulaContainsItsClausesVariables[of "clause" "F0"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''
clause el F0 \<Longrightarrow> vars clause \<subseteq> vars F0

goal (1 subgoal):
 1. getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause]))
[PROOF STEP]
using InvariantEquivalentZLAfterAddClause[of "state" "?filt Phi" "F0" "Vbl" "clause"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''
clause el F0 \<Longrightarrow> vars clause \<subseteq> vars F0
\<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); InvariantConsistent (getM state); InvariantUniq (getM state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); InvariantUniqQ (getQ state); getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; 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; Phi' = filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause]; Phi'' = if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else Phi' in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') Phi'' \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable Phi''

goal (1 subgoal):
 1. getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause]))
[PROOF STEP]
by (simp add:Let_def)
[PROOF STATE]
proof (state)
this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause]))

goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
hence "getSATFlag ?state' = UNDEF \<and> InvariantEquivalentZL (getF ?state') (getM ?state') (?filt (Phi @ [clause])) \<or>
         getSATFlag ?state' = FALSE \<and> \<not> satisfiable (?filt (Phi @ [clause]))"
[PROOF STATE]
proof (prove)
using this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (if clauseTautology clause then filter (\<lambda>c. \<not> clauseTautology c) Phi else filter (\<lambda>c. \<not> clauseTautology c) Phi @ [clause]))

goal (1 subgoal):
 1. getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause]))

goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause]))

goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''
[PROOF STEP]
have "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>
   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 STATE]
proof (prove)
using this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''

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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''
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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>getSATFlag ?state = UNDEF \<and> InvariantEquivalentZL (getF ?state) (getM ?state) (filter (\<lambda>c. \<not> clauseTautology c) ?Phi) \<or> getSATFlag ?state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) ?Phi); 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); InvariantNoDecisionsWhenConflict (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantNoDecisionsWhenUnit (getF ?state) (getM ?state) (currentLevel (getM ?state)); InvariantGetReasonIsReason (getReason ?state) (getF ?state) (getM ?state) (set (getQ ?state)); InvariantUniqQ (getQ ?state); finite Vbl; InvariantVarsM (getM ?state) F0 Vbl; InvariantVarsQ (getQ ?state) F0 Vbl; InvariantVarsF (getF ?state) F0 Vbl; getConflictFlag ?state \<or> getQ ?state = []; currentLevel (getM ?state) = 0; F0 = ?Phi @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' ?state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi)
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)
InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
InvariantUniqQ (getQ state)
finite Vbl
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
getConflictFlag state \<or> getQ state = []
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''
clause el F0 \<Longrightarrow> vars clause \<subseteq> vars 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.0 ?Vbl; InvariantVarsQ (getQ ?state) ?F0.0 ?Vbl; InvariantVarsF (getF ?state) ?F0.0 ?Vbl; finite ?Vbl; vars ?clause \<subseteq> vars ?F0.0\<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.0 ?Vbl \<and> InvariantVarsM (getM state') ?F0.0 ?Vbl \<and> InvariantVarsF (getF state') ?F0.0 ?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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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 Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
moreover
[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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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 Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
hence "InvariantNoDecisionsWhenConflict (getF ?state') (getM ?state') (currentLevel (getM ?state'))"
    "InvariantNoDecisionsWhenUnit (getF ?state') (getM ?state') (currentLevel (getM ?state'))"
[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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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. InvariantNoDecisionsWhenConflict (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state))) &&& InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
[PROOF STEP]
unfolding InvariantNoDecisionsWhenConflict_def
[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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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. \<forall>level'<currentLevel (getM (addClause clause state)). \<not> formulaFalse (getF (addClause clause state)) (elements (prefixToLevel level' (getM (addClause clause state)))) &&& InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
[PROOF STEP]
unfolding InvariantNoDecisionsWhenUnit_def
[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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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. \<forall>level'<currentLevel (getM (addClause clause state)). \<not> formulaFalse (getF (addClause clause state)) (elements (prefixToLevel level' (getM (addClause clause state)))) &&& \<forall>level'<currentLevel (getM (addClause clause state)). \<nexists>clausea literal. clausea el getF (addClause clause state) \<and> isUnitClause clausea literal (elements (prefixToLevel level' (getM (addClause clause state))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
InvariantNoDecisionsWhenConflict (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))

goal (1 subgoal):
 1. \<And>a Phi' state Phi. \<lbrakk>\<And>state Phi. \<lbrakk>getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ Phi'\<rbrakk> \<Longrightarrow> let state' = initialize Phi' state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0); getSATFlag state = UNDEF \<and> InvariantEquivalentZL (getF state) (getM state) (filter (\<lambda>c. \<not> clauseTautology c) Phi) \<or> getSATFlag state = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) Phi); 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); InvariantNoDecisionsWhenConflict (getF state) (getM state) (currentLevel (getM state)); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state)); InvariantUniqQ (getQ state); finite Vbl; InvariantVarsM (getM state) F0 Vbl; InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl; getConflictFlag state \<or> getQ state = []; currentLevel (getM state) = 0; F0 = Phi @ a # Phi'\<rbrakk> \<Longrightarrow> let state' = initialize (a # Phi') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause]))
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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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
InvariantNoDecisionsWhenConflict (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause]))
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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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
InvariantNoDecisionsWhenConflict (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))

goal (1 subgoal):
 1. let state' = initialize (clause # Phi'') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
using Cons(1)[of "?state'" "Phi @ [clause]"] \<open>finite Vbl\<close> Cons(23) Cons(24)
[PROOF STATE]
proof (prove)
using this:
getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause]))
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> InvariantGetReasonIsReason (getReason (addClause clause state)) (getF (addClause clause state)) (getM (addClause clause state)) (set (getQ (addClause clause state))) \<and> InvariantUniqQ (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
InvariantNoDecisionsWhenConflict (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state)))
\<lbrakk>getSATFlag (addClause clause state) = UNDEF \<and> InvariantEquivalentZL (getF (addClause clause state)) (getM (addClause clause state)) (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])) \<or> getSATFlag (addClause clause state) = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) (Phi @ [clause])); 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)); InvariantNoDecisionsWhenConflict (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (getM (addClause clause state))); InvariantNoDecisionsWhenUnit (getF (addClause clause state)) (getM (addClause clause state)) (currentLevel (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)); finite Vbl; InvariantVarsM (getM (addClause clause state)) F0 Vbl; InvariantVarsQ (getQ (addClause clause state)) F0 Vbl; InvariantVarsF (getF (addClause clause state)) F0 Vbl; getConflictFlag (addClause clause state) \<or> getQ (addClause clause state) = []; currentLevel (getM (addClause clause state)) = 0; F0 = (Phi @ [clause]) @ Phi''\<rbrakk> \<Longrightarrow> let state' = initialize Phi'' (addClause clause state) in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
finite Vbl
currentLevel (getM state) = 0
F0 = Phi @ clause # Phi''

goal (1 subgoal):
 1. let state' = initialize (clause # Phi'') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = initialize (clause # Phi'') state in getSATFlag state' = UNDEF \<and> InvariantEquivalentZL (getF state') (getM state') (filter (\<lambda>c. \<not> clauseTautology c) F0) \<or> getSATFlag state' = FALSE \<and> \<not> satisfiable (filter (\<lambda>c. \<not> clauseTautology c) F0)

goal:
No subgoals!
[PROOF STEP]
qed