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

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

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<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')

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))

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

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

goal (1 subgoal):
 1. InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<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')

goal (1 subgoal):
 1. InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConflictFlagCharacterization (getConflictFlag state') (getF state') (getM state')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantConflictClauseCharacterizationAfterApplyUnitPropagate:
assumes
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)"
  "InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsUniq (getWatchList state)"
  "\<not> getConflictFlag state"
shows
   "let state' = applyUnitPropagate state in
    InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
\<not> getConflictFlag state

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
using InvariantConflictClauseCharacterizationAfterAssertLiteral[of "state" "hd (getQ state)" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchListsUniq (getWatchList state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchListsUniq (getWatchList state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
unfolding InvariantWatchesEl_def
[PROOF STATE]
proof (prove)
using this:
\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
\<not> getConflictFlag state
\<lbrakk>\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchListsUniq (getWatchList state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
unfolding InvariantWatchListsContainOnlyClausesFromF_def
[PROOF STATE]
proof (prove)
using this:
\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause)
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsUniq (getWatchList state)
\<not> getConflictFlag state
\<lbrakk>\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause); \<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchListsUniq (getWatchList state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
unfolding InvariantWatchListsCharacterization_def
[PROOF STATE]
proof (prove)
using this:
\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause)
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
\<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c)
InvariantWatchListsUniq (getWatchList state)
\<not> getConflictFlag state
\<lbrakk>\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause); \<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state); \<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c); InvariantWatchListsUniq (getWatchList state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
unfolding InvariantWatchListsUniq_def
[PROOF STATE]
proof (prove)
using this:
\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause)
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
\<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c)
\<forall>l. uniq (getWatchList state l)
\<not> getConflictFlag state
\<lbrakk>\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause); \<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state); \<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c); \<forall>l. uniq (getWatchList state l); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
unfolding InvariantConflictClauseCharacterization_def
[PROOF STATE]
proof (prove)
using this:
\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause)
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
\<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c)
\<forall>l. uniq (getWatchList state l)
\<not> getConflictFlag state
\<lbrakk>\<forall>clause. 0 \<le> clause \<and> clause < length (getF state) \<longrightarrow> (\<exists>w1 w2. getWatch1 state clause = Some w1 \<and> getWatch2 state clause = Some w2 \<and> w1 el getF state ! clause \<and> w2 el getF state ! clause); \<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state); \<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c); \<forall>l. uniq (getWatchList state l); getConflictFlag state \<longrightarrow> getConflictClause state < length (getF state) \<and> clauseFalse (getF state ! getConflictClause state) (elements (getM state))\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in getConflictFlag state' \<longrightarrow> getConflictClause state' < length (getF state') \<and> clauseFalse (getF state' ! getConflictClause state') (elements (getM state'))

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in getConflictFlag state' \<longrightarrow> getConflictClause state' < length (getF state') \<and> clauseFalse (getF state' ! getConflictClause state') (elements (getM state'))
[PROOF STEP]
by (simp add: Let_def)


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

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

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<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')

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
[PROOF STEP]
hence "InvariantQCharacterization (getConflictFlag ?state') (removeAll ?uLiteral (getQ ?state')) (getF ?state') (getM ?state')"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using InvariantQCharacterizationAfterAssertLiteral[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantQCharacterization (getConflictFlag state') (removeAll (hd (getQ state)) (getQ state')) (getF state') (getM state')

goal (1 subgoal):
 1. InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using assertLiteralEffect[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (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); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantQCharacterization (getConflictFlag state') (removeAll (hd (getQ state)) (getQ state')) (getF state') (getM state')
\<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. InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))

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

goal (1 subgoal):
 1. InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using InvariantUniqQAfterAssertLiteral[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantUniqQ (getQ state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantUniqQ (getQ state')

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

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
[PROOF STEP]
have "?uLiteral = (hd (getQ ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
obtain s
      where "(getQ state) @ s = getQ ?state'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assertLiteralEffect[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<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. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding isPrefix_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<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)

goal (1 subgoal):
 1. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state)

goal (1 subgoal):
 1. hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
hence "getQ ?state' = (getQ state) @ s"
[PROOF STATE]
proof (prove)
using this:
getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state)

goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s
[PROOF STEP]
by (rule sym)
[PROOF STATE]
proof (state)
this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s

goal (1 subgoal):
 1. hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s

goal (1 subgoal):
 1. hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using \<open>getQ state \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s
getQ state \<noteq> []

goal (1 subgoal):
 1. hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using hd_append[of "getQ state" "s"]
[PROOF STATE]
proof (prove)
using this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s
getQ state \<noteq> []
hd (getQ state @ s) = (if getQ state = [] then hd s else hd (getQ state))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
[PROOF STEP]
hence "set (getQ ?state'') = set (removeAll ?uLiteral (getQ ?state'))"
[PROOF STATE]
proof (prove)
using this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
using \<open>InvariantUniqQ (getQ ?state')\<close>
[PROOF STATE]
proof (prove)
using this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
unfolding InvariantUniqQ_def
[PROOF STATE]
proof (prove)
using this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
uniq (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
uniq (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
using uniqHeadTailSet[of "getQ ?state'"]
[PROOF STATE]
proof (prove)
using this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
uniq (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
uniq (getQ (assertLiteral (hd (getQ state)) False state))
uniq (getQ (assertLiteral (hd (getQ state)) False state)) \<Longrightarrow> set (tl (getQ (assertLiteral (hd (getQ state)) False state))) = set (getQ (assertLiteral (hd (getQ state)) False state)) - {hd (getQ (assertLiteral (hd (getQ state)) False state))}

goal (1 subgoal):
 1. set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
hd (getQ state) = hd (getQ (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
uniq (getQ state)
getQ state \<noteq> []
\<not> getConflictFlag state
uniq (getQ (assertLiteral (hd (getQ state)) False state))
uniq (getQ (assertLiteral (hd (getQ state)) False state)) \<Longrightarrow> set (tl (getQ (assertLiteral (hd (getQ state)) False state))) = set (getQ (assertLiteral (hd (getQ state)) False state)) - {hd (getQ (assertLiteral (hd (getQ state)) False state))}

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

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantQCharacterization (getConflictFlag (assertLiteral (hd (getQ state)) False state)) (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state))) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state))
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')
[PROOF STEP]
unfolding InvariantQCharacterization_def
[PROOF STATE]
proof (prove)
using this:
\<not> getConflictFlag (assertLiteral (hd (getQ state)) False state) \<longrightarrow> (\<forall>l. l el removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)) = (\<exists>c. c el getF (assertLiteral (hd (getQ state)) False state) \<and> isUnitClause c l (elements (getM (assertLiteral (hd (getQ state)) False state)))))
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in \<not> getConflictFlag state'' \<longrightarrow> (\<forall>l. l el getQ state'' = (\<exists>c. c el getF state'' \<and> isUnitClause c l (elements (getM state''))))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
\<not> getConflictFlag (assertLiteral (hd (getQ state)) False state) \<longrightarrow> (\<forall>l. l el removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)) = (\<exists>c. c el getF (assertLiteral (hd (getQ state)) False state) \<and> isUnitClause c l (elements (getM (assertLiteral (hd (getQ state)) False state)))))
set (getQ (let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr>)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))

goal (1 subgoal):
 1. let state'' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in \<not> getConflictFlag state'' \<longrightarrow> (\<forall>l. l el getQ state'' = (\<exists>c. c el getF state'' \<and> isUnitClause c l (elements (getM state''))))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state'' = applyUnitPropagate state in InvariantQCharacterization (getConflictFlag state'') (getQ state'') (getF state'') (getM state'')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantUniqQAfterApplyUnitPropagate:
assumes
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)"
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)"
  "InvariantUniqQ (getQ state)"
  "getQ state \<noteq> []"
shows
  "let state'' = applyUnitPropagate state in
      InvariantUniqQ (getQ state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
let ?uLiteral = "hd (getQ state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
let ?state' = "assertLiteral ?uLiteral False state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
let ?state'' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
have "InvariantUniqQ (getQ ?state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []

goal (1 subgoal):
 1. InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using InvariantUniqQAfterAssertLiteral[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantUniqQ (getQ state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantUniqQ (getQ state')

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

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
obtain s
    where "getQ state @ s = getQ ?state'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []

goal (1 subgoal):
 1. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assertLiteralEffect[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<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. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding isPrefix_def
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantUniqQ (getQ state)
getQ state \<noteq> []
\<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)

goal (1 subgoal):
 1. (\<And>s. getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state)

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
hence "getQ ?state' = getQ state @ s"
[PROOF STATE]
proof (prove)
using this:
getQ state @ s = getQ (assertLiteral (hd (getQ state)) False state)

goal (1 subgoal):
 1. getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s
[PROOF STEP]
by (rule sym)
[PROOF STATE]
proof (state)
this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
with \<open>getQ state \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
getQ state \<noteq> []
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s
[PROOF STEP]
have "getQ ?state' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s

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

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
using \<open>getQ state \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantUniqQ (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
getQ state \<noteq> []

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in InvariantUniqQ (getQ state'')
[PROOF STEP]
unfolding InvariantUniqQ_def
[PROOF STATE]
proof (prove)
using this:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
getQ state \<noteq> []

goal (1 subgoal):
 1. let state'' = applyUnitPropagate state in uniq (getQ state'')
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
getQ state \<noteq> []

goal (1 subgoal):
 1. let state'' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in uniq (getQ state'')
[PROOF STEP]
using hd_Cons_tl[of "getQ ?state'"]
[PROOF STATE]
proof (prove)
using this:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
getQ state \<noteq> []
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> [] \<Longrightarrow> hd (getQ (assertLiteral (hd (getQ state)) False state)) # tl (getQ (assertLiteral (hd (getQ state)) False state)) = getQ (assertLiteral (hd (getQ state)) False state)

goal (1 subgoal):
 1. let state'' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in uniq (getQ state'')
[PROOF STEP]
using uniqAppendIff[of "[hd (getQ ?state')]" "tl (getQ ?state')"]
[PROOF STATE]
proof (prove)
using this:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> []
getQ state \<noteq> []
getQ (assertLiteral (hd (getQ state)) False state) \<noteq> [] \<Longrightarrow> hd (getQ (assertLiteral (hd (getQ state)) False state)) # tl (getQ (assertLiteral (hd (getQ state)) False state)) = getQ (assertLiteral (hd (getQ state)) False state)
uniq ([hd (getQ (assertLiteral (hd (getQ state)) False state))] @ tl (getQ (assertLiteral (hd (getQ state)) False state))) = (uniq [hd (getQ (assertLiteral (hd (getQ state)) False state))] \<and> uniq (tl (getQ (assertLiteral (hd (getQ state)) False state))) \<and> set [hd (getQ (assertLiteral (hd (getQ state)) False state))] \<inter> set (tl (getQ (assertLiteral (hd (getQ state)) False state))) = {})

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantNoDecisionsWhenConflictNorUnitAfterUnitPropagate:
assumes
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)"
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)"
  "InvariantConflictFlagCharacterization (getConflictFlag 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))"
shows
  "let state' = applyUnitPropagate state in
     InvariantNoDecisionsWhenConflict (getF state') (getM state') (currentLevel (getM state')) \<and>
     InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantNoDecisionsWhenConflict (getF state') (getM state') (currentLevel (getM state')) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantConflictFlagCharacterization (getConflictFlag 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))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantNoDecisionsWhenConflict (getF state') (getM state') (currentLevel (getM state')) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantConflictFlagCharacterization (getConflictFlag 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))

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantNoDecisionsWhenConflict (getF state') (getM state') (currentLevel (getM state')) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))
[PROOF STEP]
using InvariantsNoDecisionsWhenConflictNorUnitAfterAssertLiteral[of "state" "False" "hd (getQ state)"]
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantConflictFlagCharacterization (getConflictFlag 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))
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantConflictFlagCharacterization (getConflictFlag 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)); False \<longrightarrow> \<not> getConflictFlag state \<and> getQ state = []\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantNoDecisionsWhenConflict (getF state') (getM state') (currentLevel (getM state')) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantNoDecisionsWhenConflict (getF state') (getM state') (currentLevel (getM state')) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))
[PROOF STEP]
unfolding InvariantNoDecisionsWhenConflict_def
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<forall>level'<currentLevel (getM state). \<not> formulaFalse (getF state) (elements (prefixToLevel level' (getM state)))
InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state))
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); \<forall>level'<currentLevel (getM state). \<not> formulaFalse (getF state) (elements (prefixToLevel level' (getM state))); InvariantNoDecisionsWhenUnit (getF state) (getM state) (currentLevel (getM state)); False \<longrightarrow> \<not> getConflictFlag state \<and> getQ state = []\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in (\<forall>level'<currentLevel (getM state'). \<not> formulaFalse (getF state') (elements (prefixToLevel level' (getM state')))) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in (\<forall>level'<currentLevel (getM state'). \<not> formulaFalse (getF state') (elements (prefixToLevel level' (getM state')))) \<and> InvariantNoDecisionsWhenUnit (getF state') (getM state') (currentLevel (getM state'))
[PROOF STEP]
by (simp add: Let_def)