[STATEMENT]
lemma InvariantEquivalentZLAfterApplyUnitPropagate:
assumes
  "InvariantEquivalentZL (getF state) (getM state) Phi"
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"

  "\<not> (getConflictFlag state)"
  "getQ state \<noteq> []"
shows
  "let state' = applyUnitPropagate state in
      InvariantEquivalentZL (getF state') (getM state') Phi
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
let ?uLiteral = "hd (getQ state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
let ?state' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
let ?FM = "getF state @ val2form (elements (prefixToLevel 0 (getM state)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
let ?FM' = "getF ?state' @ val2form (elements (prefixToLevel 0 (getM ?state')))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
obtain uClause
    where "formulaEntailsClause (getF state) uClause" and
    "isUnitClause uClause ?uLiteral (elements (getM state))" and
    "(getM ?state') = (getM state) @ [(?uLiteral, False)]"
    "(getF ?state') = (getF state)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>formulaEntailsClause (getF state) uClause; isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]; getF (applyUnitPropagate state) = getF state\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>formulaEntailsClause (getF state) uClause; isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]; getF (applyUnitPropagate state) = getF state\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using applyUnitPropagateEffect[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); \<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>formulaEntailsClause (getF state) uClause; isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]; getF (applyUnitPropagate state) = getF state\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); \<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let uLiteral = hd (getQ state); state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>formulaEntailsClause (getF state) uClause; isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getM state @ [(hd (getQ state), False)]; getF (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getF state\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assertLiteralEffect
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); \<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let uLiteral = hd (getQ state); state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getM (assertLiteral ?l ?d ?state) = getM ?state @ [(?l, ?d)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getF (assertLiteral ?l ?d ?state) = getF ?state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral ?l ?d ?state) = getSATFlag ?state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> isPrefix (getQ ?state) (getQ (assertLiteral ?l ?d ?state))

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>formulaEntailsClause (getF state) uClause; isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getM state @ [(hd (getQ state), False)]; getF (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>) = getF state\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
proof (cases "currentLevel (getM state) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. currentLevel (getM state) = 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
 2. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
currentLevel (getM state) = 0

goal (2 subgoals):
 1. currentLevel (getM state) = 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
 2. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
hence "getM state = prefixToLevel 0 (getM state)"
[PROOF STATE]
proof (prove)
using this:
currentLevel (getM state) = 0

goal (1 subgoal):
 1. getM state = prefixToLevel 0 (getM state)
[PROOF STEP]
by (rule currentLevelZeroTrailEqualsItsPrefixToLevelZero)
[PROOF STATE]
proof (state)
this:
getM state = prefixToLevel 0 (getM state)

goal (2 subgoals):
 1. currentLevel (getM state) = 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
 2. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
have "?FM' = ?FM @ [[?uLiteral]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state

goal (1 subgoal):
 1. getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
[PROOF STEP]
using \<open>(getM ?state') = (getM state) @ [(?uLiteral, False)]\<close>
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]

goal (1 subgoal):
 1. getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
[PROOF STEP]
using prefixToLevelAppend[of "0" "getM state" "[(?uLiteral, False)]"]
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
prefixToLevel 0 (getM state @ [(hd (getQ state), False)]) = (if 0 < currentLevel (getM state) then prefixToLevel 0 (getM state) else getM state @ prefixToLevel_aux [(hd (getQ state), False)] 0 (currentLevel (getM state)))

goal (1 subgoal):
 1. getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
[PROOF STEP]
using \<open>currentLevel (getM state) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
prefixToLevel 0 (getM state @ [(hd (getQ state), False)]) = (if 0 < currentLevel (getM state) then prefixToLevel 0 (getM state) else getM state @ prefixToLevel_aux [(hd (getQ state), False)] 0 (currentLevel (getM state)))
currentLevel (getM state) = 0

goal (1 subgoal):
 1. getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
[PROOF STEP]
using \<open>getM state = prefixToLevel 0 (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
prefixToLevel 0 (getM state @ [(hd (getQ state), False)]) = (if 0 < currentLevel (getM state) then prefixToLevel 0 (getM state) else getM state @ prefixToLevel_aux [(hd (getQ state), False)] 0 (currentLevel (getM state)))
currentLevel (getM state) = 0
getM state = prefixToLevel 0 (getM state)

goal (1 subgoal):
 1. getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
[PROOF STEP]
by (auto simp add: val2formAppend)
[PROOF STATE]
proof (state)
this:
getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]

goal (2 subgoals):
 1. currentLevel (getM state) = 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
 2. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
have "formulaEntailsLiteral ?FM ?uLiteral"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state

goal (1 subgoal):
 1. formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))
[PROOF STEP]
using unitLiteralIsEntailed [of "uClause" "?uLiteral" "elements (getM state)" "(getF state)"]
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
\<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); formulaEntailsClause (getF state) uClause\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (getF state @ val2form (elements (getM state))) (hd (getQ state))

goal (1 subgoal):
 1. formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))
[PROOF STEP]
using \<open>InvariantEquivalentZL (getF state) (getM state) Phi\<close>
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
\<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); formulaEntailsClause (getF state) uClause\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (getF state @ val2form (elements (getM state))) (hd (getQ state))
InvariantEquivalentZL (getF state) (getM state) Phi

goal (1 subgoal):
 1. formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))
[PROOF STEP]
using \<open>getM state = prefixToLevel 0 (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
\<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); formulaEntailsClause (getF state) uClause\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (getF state @ val2form (elements (getM state))) (hd (getQ state))
InvariantEquivalentZL (getF state) (getM state) Phi
getM state = prefixToLevel 0 (getM state)

goal (1 subgoal):
 1. formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))
[PROOF STEP]
unfolding InvariantEquivalentZL_def
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
\<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); formulaEntailsClause (getF state) uClause\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (getF state @ val2form (elements (getM state))) (hd (getQ state))
equivalentFormulae (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) Phi
getM state = prefixToLevel 0 (getM state)

goal (1 subgoal):
 1. formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))

goal (2 subgoals):
 1. currentLevel (getM state) = 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
 2. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
hence "formulaEntailsClause ?FM [?uLiteral]"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) (hd (getQ state))

goal (1 subgoal):
 1. formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]
[PROOF STEP]
unfolding formulaEntailsLiteral_def
[PROOF STATE]
proof (prove)
using this:
\<forall>valuation. model valuation (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) \<longrightarrow> literalTrue (hd (getQ state)) valuation

goal (1 subgoal):
 1. formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]
[PROOF STEP]
unfolding formulaEntailsClause_def
[PROOF STATE]
proof (prove)
using this:
\<forall>valuation. model valuation (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) \<longrightarrow> literalTrue (hd (getQ state)) valuation

goal (1 subgoal):
 1. \<forall>valuation. model valuation (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) \<longrightarrow> model valuation [hd (getQ state)]
[PROOF STEP]
by (auto simp add: clauseTrueIffContainsTrueLiteral)
[PROOF STATE]
proof (state)
this:
formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]

goal (2 subgoals):
 1. currentLevel (getM state) = 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
 2. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
using \<open>InvariantEquivalentZL (getF state) (getM state) Phi\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
using \<open>?FM' = ?FM @ [[?uLiteral]]\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi
getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
using \<open>formulaEntailsClause ?FM [?uLiteral]\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalentZL (getF state) (getM state) Phi
getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
unfolding InvariantEquivalentZL_def
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) Phi
getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in equivalentFormulae (getF state' @ val2form (elements (prefixToLevel 0 (getM state')))) Phi
[PROOF STEP]
using extendEquivalentFormulaWithEntailedClause[of "Phi" "?FM" "[?uLiteral]"]
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) Phi
getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state)))) = (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]]
formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]
\<lbrakk>equivalentFormulae Phi (getF state @ val2form (elements (prefixToLevel 0 (getM state)))); formulaEntailsClause (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) [hd (getQ state)]\<rbrakk> \<Longrightarrow> equivalentFormulae Phi ((getF state @ val2form (elements (prefixToLevel 0 (getM state)))) @ [[hd (getQ state)]])

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in equivalentFormulae (getF state' @ val2form (elements (prefixToLevel 0 (getM state')))) Phi
[PROOF STEP]
by (simp add: equivalentFormulaeSymmetry)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi

goal (1 subgoal):
 1. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
currentLevel (getM state) \<noteq> 0

goal (1 subgoal):
 1. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
hence "?FM = ?FM'"
[PROOF STATE]
proof (prove)
using this:
currentLevel (getM state) \<noteq> 0

goal (1 subgoal):
 1. getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
currentLevel (getM state) \<noteq> 0
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state

goal (1 subgoal):
 1. getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))
[PROOF STEP]
using prefixToLevelAppend[of "0" "getM state" "[(?uLiteral, False)]"]
[PROOF STATE]
proof (prove)
using this:
currentLevel (getM state) \<noteq> 0
formulaEntailsClause (getF state) uClause
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
getF (applyUnitPropagate state) = getF state
prefixToLevel 0 (getM state @ [(hd (getQ state), False)]) = (if 0 < currentLevel (getM state) then prefixToLevel 0 (getM state) else getM state @ prefixToLevel_aux [(hd (getQ state), False)] 0 (currentLevel (getM state)))

goal (1 subgoal):
 1. getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))

goal (1 subgoal):
 1. currentLevel (getM state) \<noteq> 0 \<Longrightarrow> let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
using \<open>InvariantEquivalentZL (getF state) (getM state) Phi\<close>
[PROOF STATE]
proof (prove)
using this:
getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))
InvariantEquivalentZL (getF state) (getM state) Phi

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi
[PROOF STEP]
unfolding InvariantEquivalentZL_def
[PROOF STATE]
proof (prove)
using this:
getF state @ val2form (elements (prefixToLevel 0 (getM state))) = getF (applyUnitPropagate state) @ val2form (elements (prefixToLevel 0 (getM (applyUnitPropagate state))))
equivalentFormulae (getF state @ val2form (elements (prefixToLevel 0 (getM state)))) Phi

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in equivalentFormulae (getF state' @ val2form (elements (prefixToLevel 0 (getM state')))) Phi
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantEquivalentZL (getF state') (getM state') Phi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantVarsQTl:
assumes
  "InvariantVarsQ Q F0 Vbl"
  "Q \<noteq> []"
shows
  "InvariantVarsQ (tl Q) F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsQ (tl Q) F0 Vbl
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantVarsQ (tl Q) F0 Vbl
[PROOF STEP]
have "InvariantVarsQ ((hd Q) # (tl Q)) F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsQ (hd Q # tl Q) F0 Vbl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantVarsQ Q F0 Vbl
Q \<noteq> []

goal (1 subgoal):
 1. InvariantVarsQ (hd Q # tl Q) F0 Vbl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InvariantVarsQ (hd Q # tl Q) F0 Vbl

goal (1 subgoal):
 1. InvariantVarsQ (tl Q) F0 Vbl
[PROOF STEP]
hence "{var (hd Q)} \<union> vars (tl Q) \<subseteq> vars F0 \<union> Vbl"
[PROOF STATE]
proof (prove)
using this:
InvariantVarsQ (hd Q # tl Q) F0 Vbl

goal (1 subgoal):
 1. {var (hd Q)} \<union> vars (tl Q) \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
unfolding InvariantVarsQ_def
[PROOF STATE]
proof (prove)
using this:
vars (hd Q # tl Q) \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. {var (hd Q)} \<union> vars (tl Q) \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{var (hd Q)} \<union> vars (tl Q) \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. InvariantVarsQ (tl Q) F0 Vbl
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{var (hd Q)} \<union> vars (tl Q) \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. InvariantVarsQ (tl Q) F0 Vbl
[PROOF STEP]
unfolding InvariantVarsQ_def
[PROOF STATE]
proof (prove)
using this:
{var (hd Q)} \<union> vars (tl Q) \<subseteq> vars F0 \<union> Vbl

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantsVarsAfterApplyUnitPropagate:
assumes
  "InvariantConsistent (getM state)"
  "InvariantUniq (getM state)"
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsUniq (getWatchList state)" and
  "InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)" and
  "InvariantQCharacterization False (getQ state) (getF state) (getM state)" and
  "getQ state \<noteq> []"
  "\<not> getConflictFlag state"
  "InvariantVarsM (getM state) F0 Vbl" and
  "InvariantVarsQ (getQ state) F0 Vbl" and
  "InvariantVarsF (getF state) F0 Vbl"
shows
  "let state' = applyUnitPropagate state in
     InvariantVarsM (getM state') F0 Vbl \<and>
     InvariantVarsQ (getQ state') F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
let ?state' = "assertLiteral (hd (getQ state)) False state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
let ?state'' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
have "InvariantVarsQ (getQ ?state') F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl

goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
using InvariantConsistentAfterApplyUnitPropagate[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantConsistent (getM state')

goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
using InvariantUniqAfterApplyUnitPropagate[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantConsistent (getM state')
\<lbrakk>InvariantUniq (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantUniq (getM state')

goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
using InvariantVarsQAfterAssertLiteral[of "state" "hd (getQ state)" "False" "F0" "Vbl"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantConsistent (getM state')
\<lbrakk>InvariantUniq (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantUniq (getM state')
\<lbrakk>InvariantConsistent (getM state @ [(hd (getQ state), False)]); InvariantUniq (getM state @ [(hd (getQ state), False)]); 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); InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantVarsQ (getQ state') F0 Vbl

goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
using assertLiteralEffect[of "state" "hd (getQ state)" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantConsistent (getM state')
\<lbrakk>InvariantUniq (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantUniq (getM state')
\<lbrakk>InvariantConsistent (getM state @ [(hd (getQ state), False)]); InvariantUniq (getM state @ [(hd (getQ state), False)]); 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); InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantVarsQ (getQ state') F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConsistent (getM state')
\<lbrakk>InvariantUniq (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantUniq (getM state')
\<lbrakk>InvariantConsistent (getM state @ [(hd (getQ state), False)]); InvariantUniq (getM state @ [(hd (getQ state), False)]); 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); InvariantVarsQ (getQ state) F0 Vbl; InvariantVarsF (getF state) F0 Vbl\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantVarsQ (getQ state') F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
have "(getQ ?state') \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl

goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
using assertLiteralEffect[of "state" "hd (getQ state)" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
using \<open>getQ state \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))
getQ state \<noteq> []

goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
unfolding isPrefix_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> \<exists>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state)
getQ state \<noteq> []

goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
have "InvariantVarsQ (getQ ?state'') F0 Vbl"
[PROOF STATE]
proof (prove)
using this:
InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []

goal (1 subgoal):
 1. InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []

goal (1 subgoal):
 1. InvariantVarsQ (getQ (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl
[PROOF STEP]
using InvariantVarsQTl[of "getQ ?state'" F0 Vbl]
[PROOF STATE]
proof (prove)
using this:
InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
\<lbrakk>InvariantVarsQ (getQ (assertLiteral (hd (getQ state)) False state)) F0 Vbl; getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []\<rbrakk> \<Longrightarrow> InvariantVarsQ (tl (getQ (assertLiteral (hd (getQ state)) False state))) F0 Vbl

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

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
have "var (hd (getQ state)) \<in> vars F0 \<union> Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (hd (getQ state)) \<in> vars F0 \<union> Vbl
[PROOF STEP]
using \<open>getQ state \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []

goal (1 subgoal):
 1. var (hd (getQ state)) \<in> vars F0 \<union> Vbl
[PROOF STEP]
using \<open>InvariantVarsQ (getQ state) F0 Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []
InvariantVarsQ (getQ state) F0 Vbl

goal (1 subgoal):
 1. var (hd (getQ state)) \<in> vars F0 \<union> Vbl
[PROOF STEP]
using hd_in_set[of "getQ state"]
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []
InvariantVarsQ (getQ state) F0 Vbl
getQ state \<noteq> [] \<Longrightarrow> hd (getQ state) \<in> set (getQ state)

goal (1 subgoal):
 1. var (hd (getQ state)) \<in> vars F0 \<union> Vbl
[PROOF STEP]
using clauseContainsItsLiteralsVariable[of "hd (getQ state)" "getQ state"]
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []
InvariantVarsQ (getQ state) F0 Vbl
getQ state \<noteq> [] \<Longrightarrow> hd (getQ state) \<in> set (getQ state)
hd (getQ state) el getQ state \<Longrightarrow> var (hd (getQ state)) \<in> vars (getQ state)

goal (1 subgoal):
 1. var (hd (getQ state)) \<in> vars F0 \<union> Vbl
[PROOF STEP]
unfolding InvariantVarsQ_def
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []
vars (getQ state) \<subseteq> vars F0 \<union> Vbl
getQ state \<noteq> [] \<Longrightarrow> hd (getQ state) \<in> set (getQ state)
hd (getQ state) el getQ state \<Longrightarrow> var (hd (getQ state)) \<in> vars (getQ state)

goal (1 subgoal):
 1. var (hd (getQ state)) \<in> vars F0 \<union> Vbl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
hence "InvariantVarsM (getM ?state'') F0 Vbl"
[PROOF STATE]
proof (prove)
using this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl
[PROOF STEP]
using assertLiteralEffect[of "state" "hd (getQ state)" "False"]
[PROOF STATE]
proof (prove)
using this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl
[PROOF STEP]
using varsAppendValuation[of "elements (getM state)" "[hd (getQ state)]"]
[PROOF STATE]
proof (prove)
using this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))
vars (elements (getM state) @ [hd (getQ state)]) = vars (elements (getM state)) \<union> vars [hd (getQ state)]

goal (1 subgoal):
 1. InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantVarsM (getM state) F0 Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))
vars (elements (getM state) @ [hd (getQ state)]) = vars (elements (getM state)) \<union> vars [hd (getQ state)]

goal (1 subgoal):
 1. InvariantVarsM (getM (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>)) F0 Vbl
[PROOF STEP]
unfolding InvariantVarsM_def
[PROOF STATE]
proof (prove)
using this:
var (hd (getQ state)) \<in> vars F0 \<union> Vbl
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization False (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
vars (elements (getM state)) \<subseteq> vars F0 \<union> Vbl
InvariantVarsQ (getQ state) F0 Vbl
InvariantVarsF (getF state) F0 Vbl
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))
vars (elements (getM state) @ [hd (getQ state)]) = vars (elements (getM state)) \<union> vars [hd (getQ state)]

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

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl
InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantVarsQ (getQ (applyUnitPropagate state)) F0 Vbl
InvariantVarsM (getM (applyUnitPropagate state)) F0 Vbl

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantVarsM (getM state') F0 Vbl \<and> InvariantVarsQ (getQ state') F0 Vbl

goal:
No subgoals!
[PROOF STEP]
qed