[STATEMENT]
lemma InvariantGetReasonIsReasonAfterApplyUnitPropagate:
assumes
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantWatchListsUniq (getWatchList state)" and
  "InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)" and
  "InvariantUniqQ (getQ state)" and
  "InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))" and
  "getQ state \<noteq> []" and
  "\<not> getConflictFlag state"
shows
  "let state' = applyUnitPropagate state in
     InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
let ?state0 = "state \<lparr> getM := getM state @ [(hd (getQ state), False)]\<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
let ?state' = "assertLiteral (hd (getQ state)) False state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
let ?state'' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
have "InvariantGetReasonIsReason (getReason ?state0) (getF ?state0) (getM ?state0) (set (removeAll (hd (getQ ?state0)) (getQ ?state0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
fix l::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
assume *: "l el (elements (getM ?state0)) \<and> \<not> l el (decisions (getM ?state0)) \<and> elementLevel l (getM ?state0) > 0"
[PROOF STATE]
proof (state)
this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
hence "\<exists> reason. getReason ?state0 l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF ?state0) \<and>
               isReason (nth (getF ?state0) reason) l (elements (getM ?state0))"
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
proof (cases "l el (elements (getM state))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
 2. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l el elements (getM state)

goal (2 subgoals):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
 2. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
[PROOF STEP]
have "\<not> l el (decisions (getM state))"
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. \<not> l el decisions (getM state)
[PROOF STEP]
by (auto simp add: markedElementsAppend)
[PROOF STATE]
proof (state)
this:
\<not> l el decisions (getM state)

goal (2 subgoals):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
 2. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
[PROOF STEP]
have "elementLevel l (getM state) > 0"
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. 0 < elementLevel l (getM state)
[PROOF STEP]
using elementLevelAppend[of "l" "getM state" "[(hd (getQ state), False)]"]
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
l \<in> set (elements (getM state)) \<Longrightarrow> elementLevel l (getM state) = elementLevel l (getM state @ [(hd (getQ state), False)])

goal (1 subgoal):
 1. 0 < elementLevel l (getM state)
[PROOF STEP]
using \<open>l el (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
l \<in> set (elements (getM state)) \<Longrightarrow> elementLevel l (getM state) = elementLevel l (getM state @ [(hd (getQ state), False)])
l el elements (getM state)

goal (1 subgoal):
 1. 0 < elementLevel l (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < elementLevel l (getM state)

goal (2 subgoals):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
 2. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using \<open>InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using \<open>l el (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
l el elements (getM state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using \<open>\<not> l el (decisions (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
l el elements (getM state)
\<not> l el decisions (getM state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using \<open>elementLevel l (getM state) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
l el elements (getM state)
\<not> l el decisions (getM state)
0 < elementLevel l (getM state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
unfolding InvariantGetReasonIsReason_def
[PROOF STATE]
proof (prove)
using this:
\<forall>literal. (literal el elements (getM state) \<and> \<not> literal el decisions (getM state) \<and> 0 < elementLevel literal (getM state) \<longrightarrow> (\<exists>reason. getReason state literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF state) \<and> isReason (getF state ! reason) literal (elements (getM state)))) \<and> (0 < currentLevel (getM state) \<and> literal \<in> set (getQ state) \<longrightarrow> (\<exists>reason. getReason state literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF state) \<and> (isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)))))
l el elements (getM state)
\<not> l el decisions (getM state)
0 < elementLevel l (getM state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
by (auto simp add: isReasonAppend)
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> l el elements (getM state)

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
\<not> l el elements (getM state)
[PROOF STEP]
have "l = hd (getQ state)"
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
\<not> l el elements (getM state)

goal (1 subgoal):
 1. l = hd (getQ state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l = hd (getQ state)

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
have "currentLevel (getM ?state0) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. 0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
[PROOF STEP]
using elementLevelLeqCurrentLevel[of "l" "getM ?state0"]
[PROOF STATE]
proof (prove)
using this:
l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<le> currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. 0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
hence "currentLevel (getM state) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. 0 < currentLevel (getM state)
[PROOF STEP]
unfolding currentLevel_def
[PROOF STATE]
proof (prove)
using this:
0 < length (decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. 0 < length (decisions (getM state))
[PROOF STEP]
by (simp add: markedElementsAppend)
[PROOF STATE]
proof (state)
this:
0 < currentLevel (getM state)

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < currentLevel (getM state)

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
have "hd (getQ ?state0) el (getQ state)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state
[PROOF STEP]
using \<open>getQ state \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
getQ state \<noteq> []

goal (1 subgoal):
 1. hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < currentLevel (getM state)
hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state
[PROOF STEP]
obtain reason
          where "getReason state (hd (getQ state)) = Some reason" "0 \<le> reason \<and> reason < length (getF state)"
          "isUnitClause (nth (getF state) reason) (hd (getQ state)) (elements (getM state)) \<or>
           clauseFalse (nth (getF state) reason) (elements (getM state))"
[PROOF STATE]
proof (prove)
using this:
0 < currentLevel (getM state)
hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state (hd (getQ state)) = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))\<close>
[PROOF STATE]
proof (prove)
using this:
0 < currentLevel (getM state)
hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state (hd (getQ state)) = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding InvariantGetReasonIsReason_def
[PROOF STATE]
proof (prove)
using this:
0 < currentLevel (getM state)
hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) el getQ state
\<forall>literal. (literal el elements (getM state) \<and> \<not> literal el decisions (getM state) \<and> 0 < elementLevel literal (getM state) \<longrightarrow> (\<exists>reason. getReason state literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF state) \<and> isReason (getF state ! reason) literal (elements (getM state)))) \<and> (0 < currentLevel (getM state) \<and> literal \<in> set (getQ state) \<longrightarrow> (\<exists>reason. getReason state literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF state) \<and> (isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)))))

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state (hd (getQ state)) = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
hence "isUnitClause (nth (getF state) reason) (hd (getQ state)) (elements (getM state))"
[PROOF STATE]
proof (prove)
using this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))

goal (1 subgoal):
 1. isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
[PROOF STEP]
using \<open>\<not> getConflictFlag state\<close>
[PROOF STATE]
proof (prove)
using this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> getConflictFlag state

goal (1 subgoal):
 1. isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
[PROOF STEP]
using \<open>InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> getConflictFlag state
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)

goal (1 subgoal):
 1. isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
[PROOF STEP]
unfolding InvariantConflictFlagCharacterization_def
[PROOF STATE]
proof (prove)
using this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> getConflictFlag state
getConflictFlag state = formulaFalse (getF state) (elements (getM state))

goal (1 subgoal):
 1. isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
[PROOF STEP]
using nth_mem[of "reason" "getF state"]
[PROOF STATE]
proof (prove)
using this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> getConflictFlag state
getConflictFlag state = formulaFalse (getF state) (elements (getM state))
reason < length (getF state) \<Longrightarrow> getF state ! reason \<in> set (getF state)

goal (1 subgoal):
 1. isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
[PROOF STEP]
using formulaFalseIffContainsFalseClause[of "getF state" "elements (getM state)"]
[PROOF STATE]
proof (prove)
using this:
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> getConflictFlag state
getConflictFlag state = formulaFalse (getF state) (elements (getM state))
reason < length (getF state) \<Longrightarrow> getF state ! reason \<in> set (getF state)
formulaFalse (getF state) (elements (getM state)) = (\<exists>clause. clause el getF state \<and> clauseFalse clause (elements (getM state)))

goal (1 subgoal):
 1. isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))

goal (1 subgoal):
 1. \<lbrakk>l el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> l el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel l (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<not> l el elements (getM state)\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using \<open>getReason state (hd (getQ state)) = Some reason\<close> \<open>0 \<le> reason \<and> reason < length (getF state)\<close>
[PROOF STATE]
proof (prove)
using this:
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using isUnitClauseIsReason[of "nth (getF state) reason" "hd (getQ state)" "elements (getM state)" "[hd (getQ state)]"]
[PROOF STATE]
proof (prove)
using this:
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
\<lbrakk>isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)); hd (getQ state) el [hd (getQ state)]\<rbrakk> \<Longrightarrow> isReason (getF state ! reason) (hd (getQ state)) (elements (getM state) @ [hd (getQ state)])

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
using \<open>l = hd (getQ state)\<close>
[PROOF STATE]
proof (prove)
using this:
isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state))
getReason state (hd (getQ state)) = Some reason
0 \<le> reason \<and> reason < length (getF state)
\<lbrakk>isUnitClause (getF state ! reason) (hd (getQ state)) (elements (getM state)); hd (getQ state) el [hd (getQ state)]\<rbrakk> \<Longrightarrow> isReason (getF state ! reason) (hd (getQ state)) (elements (getM state) @ [hd (getQ state)])
l = hd (getQ state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) l = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) l (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l2 el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> ?l2 el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel ?l2 (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?l2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?l2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?l2 el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> ?l2 el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel ?l2 (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?l2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?l2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?l2 el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> ?l2 el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel ?l2 (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?l2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?l2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
fix literal::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
assume "currentLevel (getM ?state0) > 0"
[PROOF STATE]
proof (state)
this:
0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
hence "currentLevel (getM state) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. 0 < currentLevel (getM state)
[PROOF STEP]
unfolding currentLevel_def
[PROOF STATE]
proof (prove)
using this:
0 < length (decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))

goal (1 subgoal):
 1. 0 < length (decisions (getM state))
[PROOF STEP]
by (simp add: markedElementsAppend)
[PROOF STATE]
proof (state)
this:
0 < currentLevel (getM state)

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
assume"literal el removeAll (hd (getQ ?state0)) (getQ ?state0)"
[PROOF STATE]
proof (state)
this:
literal el removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
hence "literal \<noteq> hd (getQ state)" "literal el getQ state"
[PROOF STATE]
proof (prove)
using this:
literal el removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))

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

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
literal \<noteq> hd (getQ state)
literal el getQ state
[PROOF STEP]
obtain reason
        where "getReason state literal = Some reason" "0 \<le> reason \<and> reason < length (getF state)" and
        *: "isUnitClause (nth (getF state) reason) literal (elements (getM state)) \<or>
            clauseFalse (nth (getF state) reason) (elements (getM state))"
[PROOF STATE]
proof (prove)
using this:
literal \<noteq> hd (getQ state)
literal el getQ state

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>currentLevel (getM state) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
literal \<noteq> hd (getQ state)
literal el getQ state
0 < currentLevel (getM state)

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))\<close>
[PROOF STATE]
proof (prove)
using this:
literal \<noteq> hd (getQ state)
literal el getQ state
0 < currentLevel (getM state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding InvariantGetReasonIsReason_def
[PROOF STATE]
proof (prove)
using this:
literal \<noteq> hd (getQ state)
literal el getQ state
0 < currentLevel (getM state)
\<forall>literal. (literal el elements (getM state) \<and> \<not> literal el decisions (getM state) \<and> 0 < elementLevel literal (getM state) \<longrightarrow> (\<exists>reason. getReason state literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF state) \<and> isReason (getF state ! reason) literal (elements (getM state)))) \<and> (0 < currentLevel (getM state) \<and> literal \<in> set (getQ state) \<longrightarrow> (\<exists>reason. getReason state literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF state) \<and> (isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)))))

goal (1 subgoal):
 1. (\<And>reason. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getReason state literal = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
hence "\<exists> reason. getReason ?state0 literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF ?state0) \<and>
              (isUnitClause (nth (getF ?state0) reason) literal (elements (getM ?state0)) \<or>
               clauseFalse (nth (getF ?state0) reason) (elements (getM ?state0)))"
[PROOF STATE]
proof (prove)
using this:
getReason state literal = Some reason
0 \<le> reason \<and> reason < length (getF state)
isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
proof (cases "isUnitClause (nth (getF state) reason) literal (elements (getM state))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
 2. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); \<not> isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isUnitClause (getF state ! reason) literal (elements (getM state))

goal (2 subgoals):
 1. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
 2. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); \<not> isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
proof (cases "opposite literal = hd (getQ state)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. opposite literal = hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
 2. opposite literal \<noteq> hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
opposite literal = hd (getQ state)

goal (2 subgoals):
 1. opposite literal = hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
 2. opposite literal \<noteq> hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
opposite literal = hd (getQ state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>isUnitClause (nth (getF state) reason) literal (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal = hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>getReason state literal = Some reason\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal = hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))
getReason state literal = Some reason

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>literal \<noteq> hd (getQ state)\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal = hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))
getReason state literal = Some reason
literal \<noteq> hd (getQ state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>0 \<le> reason \<and> reason < length (getF state)\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal = hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))
getReason state literal = Some reason
literal \<noteq> hd (getQ state)
0 \<le> reason \<and> reason < length (getF state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
opposite literal = hd (getQ state)
literal el getF state ! reason \<and> \<not> literalTrue literal (elements (getM state)) \<and> \<not> literalFalse literal (elements (getM state)) \<and> (\<forall>literala. literala el getF state ! reason \<and> literala \<noteq> literal \<longrightarrow> literalFalse literala (elements (getM state)))
getReason state literal = Some reason
literal \<noteq> hd (getQ state)
0 \<le> reason \<and> reason < length (getF state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (literal el getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason \<and> \<not> literalTrue literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<and> \<not> literalFalse literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<and> (\<forall>literala. literala el getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason \<and> literala \<noteq> literal \<longrightarrow> literalFalse literala (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
by (auto simp add: clauseFalseIffAllLiteralsAreFalse)
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. opposite literal \<noteq> hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. opposite literal \<noteq> hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
opposite literal \<noteq> hd (getQ state)

goal (1 subgoal):
 1. opposite literal \<noteq> hd (getQ state) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
opposite literal \<noteq> hd (getQ state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>isUnitClause (nth (getF state) reason) literal (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal \<noteq> hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>getReason state literal = Some reason\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal \<noteq> hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))
getReason state literal = Some reason

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>literal \<noteq> hd (getQ state)\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal \<noteq> hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))
getReason state literal = Some reason
literal \<noteq> hd (getQ state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>0 \<le> reason \<and> reason < length (getF state)\<close>
[PROOF STATE]
proof (prove)
using this:
opposite literal \<noteq> hd (getQ state)
isUnitClause (getF state ! reason) literal (elements (getM state))
getReason state literal = Some reason
literal \<noteq> hd (getQ state)
0 \<le> reason \<and> reason < length (getF state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
opposite literal \<noteq> hd (getQ state)
literal el getF state ! reason \<and> \<not> literalTrue literal (elements (getM state)) \<and> \<not> literalFalse literal (elements (getM state)) \<and> (\<forall>literala. literala el getF state ! reason \<and> literala \<noteq> literal \<longrightarrow> literalFalse literala (elements (getM state)))
getReason state literal = Some reason
literal \<noteq> hd (getQ state)
0 \<le> reason \<and> reason < length (getF state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (literal el getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason \<and> \<not> literalTrue literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<and> \<not> literalFalse literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<and> (\<forall>literala. literala el getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason \<and> literala \<noteq> literal \<longrightarrow> literalFalse literala (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); \<not> isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); \<not> isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> isUnitClause (getF state ! reason) literal (elements (getM state))

goal (1 subgoal):
 1. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); \<not> isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> isUnitClause (getF state ! reason) literal (elements (getM state))
[PROOF STEP]
have "clauseFalse (nth (getF state) reason) (elements (getM state))"
[PROOF STATE]
proof (prove)
using this:
isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state))
\<not> isUnitClause (getF state ! reason) literal (elements (getM state))

goal (1 subgoal):
 1. clauseFalse (getF state ! reason) (elements (getM state))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
clauseFalse (getF state ! reason) (elements (getM state))

goal (1 subgoal):
 1. \<lbrakk>getReason state literal = Some reason; 0 \<le> reason \<and> reason < length (getF state); isUnitClause (getF state ! reason) literal (elements (getM state)) \<or> clauseFalse (getF state ! reason) (elements (getM state)); \<not> isUnitClause (getF state ! reason) literal (elements (getM state))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
clauseFalse (getF state ! reason) (elements (getM state))

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>getReason state literal = Some reason\<close>
[PROOF STATE]
proof (prove)
using this:
clauseFalse (getF state ! reason) (elements (getM state))
getReason state literal = Some reason

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using \<open>0 \<le> reason \<and> reason < length (getF state)\<close>
[PROOF STATE]
proof (prove)
using this:
clauseFalse (getF state ! reason) (elements (getM state))
getReason state literal = Some reason
0 \<le> reason \<and> reason < length (getF state)

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
using clauseFalseAppendValuation[of "nth (getF state) reason" "elements (getM state)" "[hd (getQ state)]"]
[PROOF STATE]
proof (prove)
using this:
clauseFalse (getF state ! reason) (elements (getM state))
getReason state literal = Some reason
0 \<le> reason \<and> reason < length (getF state)
clauseFalse (getF state ! reason) (elements (getM state)) \<Longrightarrow> clauseFalse (getF state ! reason) (elements (getM state) @ [hd (getQ state)])

goal (1 subgoal):
 1. \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); ?literal2 el removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?literal2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?literal2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?l2 el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> ?l2 el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel ?l2 (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?l2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?l2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
\<lbrakk>0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); ?literal2 el removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?literal2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?literal2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?l2 el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> ?l2 el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel ?l2 (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?l2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?l2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
\<lbrakk>0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); ?literal2 el removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?literal2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?literal2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
[PROOF STEP]
unfolding InvariantGetReasonIsReason_def
[PROOF STATE]
proof (prove)
using this:
?l2 el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> ?l2 el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel ?l2 (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?l2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?l2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))
\<lbrakk>0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); ?literal2 el removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ?literal2 = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) ?literal2 (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. \<forall>literal. (literal el elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> \<not> literal el decisions (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> 0 < elementLevel literal (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<longrightarrow> (\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> isReason (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))) \<and> (0 < currentLevel (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> literal \<in> set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<longrightarrow> (\<exists>reason. getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) literal = Some reason \<and> 0 \<le> reason \<and> reason < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) \<and> (isUnitClause (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) literal (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<or> clauseFalse (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) ! reason) (elements (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
hence "InvariantGetReasonIsReason (getReason ?state') (getF ?state') (getM ?state') (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ ?state') - set (getQ state)))"
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)))
[PROOF STEP]
unfolding assertLiteral_def
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (Let (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (notifyWatches (opposite (hd (getQ state)))))) (getF (Let (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (notifyWatches (opposite (hd (getQ state)))))) (getM (Let (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (notifyWatches (opposite (hd (getQ state)))))) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (Let (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (notifyWatches (opposite (hd (getQ state)))))) - set (getQ state)))
[PROOF STEP]
unfolding notifyWatches_def
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getF (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getM (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) - set (getQ state)))
[PROOF STEP]
using InvariantGetReasonIsReasonAfterNotifyWatches[of
      "?state0" "getWatchList ?state0 (opposite (hd (getQ state)))"  "opposite (hd (getQ state))" "getM state" "False"
      "set (removeAll (hd (getQ ?state0)) (getQ ?state0))" "[]"]
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> 0 \<le> c \<and> c < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> Some (opposite (hd (getQ state))) = getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c \<or> Some (opposite (hd (getQ state))) = getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c; uniq (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))); getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) = getM state @ [(opposite (opposite (hd (getQ state))), False)]; InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))\<rbrakk> \<Longrightarrow> let state' = notifyWatches_loop (opposite (hd (getQ state))) (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) [] (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) in Let (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<union> (set (getQ state') - set (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))) (InvariantGetReasonIsReason (getReason state') (getF state') (getM state'))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getF (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getM (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) - set (getQ state)))
[PROOF STEP]
unfolding InvariantWatchListsContainOnlyClausesFromF_def
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> 0 \<le> c \<and> c < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> Some (opposite (hd (getQ state))) = getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c \<or> Some (opposite (hd (getQ state))) = getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c; uniq (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))); getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) = getM state @ [(opposite (opposite (hd (getQ state))), False)]; InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))\<rbrakk> \<Longrightarrow> let state' = notifyWatches_loop (opposite (hd (getQ state))) (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) [] (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) in Let (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<union> (set (getQ state') - set (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))) (InvariantGetReasonIsReason (getReason state') (getF state') (getM state'))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getF (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getM (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) - set (getQ state)))
[PROOF STEP]
unfolding InvariantWatchListsCharacterization_def
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
InvariantWatchListsUniq (getWatchList state)
\<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> 0 \<le> c \<and> c < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> Some (opposite (hd (getQ state))) = getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c \<or> Some (opposite (hd (getQ state))) = getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c; uniq (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))); getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) = getM state @ [(opposite (opposite (hd (getQ state))), False)]; InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))\<rbrakk> \<Longrightarrow> let state' = notifyWatches_loop (opposite (hd (getQ state))) (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) [] (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) in Let (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<union> (set (getQ state') - set (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))) (InvariantGetReasonIsReason (getReason state') (getF state') (getM state'))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getF (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getM (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) - set (getQ state)))
[PROOF STEP]
unfolding InvariantWatchListsUniq_def
[PROOF STATE]
proof (prove)
using this:
InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))
\<forall>l c. c \<in> set (getWatchList state l) \<longrightarrow> 0 \<le> c \<and> c < length (getF state)
\<forall>l. uniq (getWatchList state l)
\<forall>c l. (c \<in> set (getWatchList state l)) = (Some l = getWatch1 state c \<or> Some l = getWatch2 state c)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> 0 \<le> c \<and> c < length (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)); \<forall>c. c \<in> set (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) \<longrightarrow> Some (opposite (hd (getQ state))) = getWatch1 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c \<or> Some (opposite (hd (getQ state))) = getWatch2 (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) c; uniq (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))); getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) = getM state @ [(opposite (opposite (hd (getQ state))), False)]; InvariantGetReasonIsReason (getReason (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getF (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (getM (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)) (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))))\<rbrakk> \<Longrightarrow> let state' = notifyWatches_loop (opposite (hd (getQ state))) (getWatchList (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) (opposite (hd (getQ state)))) [] (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>) in Let (set (removeAll (hd (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>))) \<union> (set (getQ state') - set (getQ (state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr>)))) (InvariantGetReasonIsReason (getReason state') (getF state') (getM state'))

goal (1 subgoal):
 1. InvariantGetReasonIsReason (getReason (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getF (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (getM (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (let state' = state\<lparr>getM := getM state @ [(hd (getQ state), False)]\<rparr> in notifyWatches_loop (opposite (hd (getQ state))) (getWatchList state' (opposite (hd (getQ state)))) [] state')) - set (getQ state)))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (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:
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (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" "hd (getQ state)" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (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:
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (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. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (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 simp
[PROOF STATE]
proof (state)
this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s

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

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

goal (1 subgoal):
 1. hd (getQ (assertLiteral (hd (getQ state)) False state)) = hd (getQ 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> [] \<Longrightarrow> hd (getQ state @ s) = hd (getQ state)
getQ state \<noteq> []

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

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
have " set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ ?state') - set (getQ state)) =
         set (removeAll (hd (getQ state)) (getQ ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
using \<open>getQ ?state' = getQ state @ s\<close>
[PROOF STATE]
proof (prove)
using this:
getQ (assertLiteral (hd (getQ state)) False state) = getQ state @ s

goal (1 subgoal):
 1. set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)) = set (removeAll (hd (getQ state)) (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. set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))

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

goal (1 subgoal):
 1. uniq (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using InvariantUniqQAfterAssertLiteral[of "state" "hd (getQ state)" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
InvariantUniqQ (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (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. uniq (getQ (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
unfolding InvariantUniqQ_def
[PROOF STATE]
proof (prove)
using this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantConflictFlagCharacterization (getConflictFlag state) (getF state) (getM state)
uniq (getQ state)
InvariantGetReasonIsReason (getReason state) (getF state) (getM state) (set (getQ state))
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); uniq (getQ state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in uniq (getQ state')

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

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
have "set (getQ ?state'') = set (removeAll (hd (getQ state)) (getQ ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
[PROOF STEP]
using \<open>uniq (getQ ?state')\<close>
[PROOF STATE]
proof (prove)
using this:
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 \<open>hd (getQ ?state') = hd (getQ state)\<close>
[PROOF STATE]
proof (prove)
using this:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
hd (getQ (assertLiteral (hd (getQ state)) False state)) = hd (getQ 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:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
hd (getQ (assertLiteral (hd (getQ state)) False state)) = hd (getQ 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:
uniq (getQ (assertLiteral (hd (getQ state)) False state))
hd (getQ (assertLiteral (hd (getQ state)) False state)) = hd (getQ 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 InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using 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 InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
using \<open>InvariantGetReasonIsReason (getReason ?state') (getF ?state') (getM ?state') (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ ?state') - set (getQ state)))\<close>
[PROOF STATE]
proof (prove)
using this:
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
using \<open>set (getQ ?state'') = set (removeAll (hd (getQ state)) (getQ ?state'))\<close>
[PROOF STATE]
proof (prove)
using this:
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ 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 InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
using \<open>set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ ?state') - set (getQ state)) =
         set (removeAll (hd (getQ state)) (getQ ?state'))\<close>
[PROOF STATE]
proof (prove)
using this:
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)))
set (getQ (applyUnitPropagate state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))
set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)) = set (removeAll (hd (getQ state)) (getQ (assertLiteral (hd (getQ state)) False state)))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
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)))
InvariantGetReasonIsReason (getReason (assertLiteral (hd (getQ state)) False state)) (getF (assertLiteral (hd (getQ state)) False state)) (getM (assertLiteral (hd (getQ state)) False state)) (set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ 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)))
set (removeAll (hd (getQ state)) (getQ state)) \<union> (set (getQ (assertLiteral (hd (getQ state)) False state)) - set (getQ state)) = 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 InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantGetReasonIsReason (getReason state') (getF state') (getM state') (set (getQ state'))

goal:
No subgoals!
[PROOF STEP]
qed