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

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
proof (induct state rule: exhaustiveUnitPropagate_dom.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state)) (getF (applyUnitPropagate state)); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state)); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantWatchesEl (getF (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantWatchesDiffer (getF (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state)) (getConflictClause (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
case (step state')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state')); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state)) (getF (applyUnitPropagate state)); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state)); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantWatchesEl (getF (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantWatchesDiffer (getF (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state)) (getConflictClause (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
note ih = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state')); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')
InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state)) (getF (applyUnitPropagate state)); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state)); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantWatchesEl (getF (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantWatchesDiffer (getF (applyUnitPropagate state)) (getWatch1 (applyUnitPropagate state)) (getWatch2 (applyUnitPropagate state)); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state)) (getConflictClause (applyUnitPropagate state)) (getF (applyUnitPropagate state)) (getM (applyUnitPropagate state))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state'); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantConflictClauseCharacterization (getConflictFlag state) (getConflictClause state) (getF state) (getM state)\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
proof (cases "(getConflictFlag state') \<or> (getQ state') = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
getConflictFlag state' \<or> getQ state' = []

goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
with exhaustiveUnitPropagate.simps[of "state'"]
[PROOF STATE]
proof (chain)
picking this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
have "exhaustiveUnitPropagate state' = state'"
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = state'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate state' = state'

goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = state'

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

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
by (auto simp only: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
let ?state'' = "applyUnitPropagate state'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
have "exhaustiveUnitPropagate state' = exhaustiveUnitPropagate ?state''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
using exhaustiveUnitPropagate.simps[of "state'"]
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
have "InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state'') (getF ?state'')" and
      "InvariantWatchListsUniq (getWatchList ?state'')" and
      "InvariantWatchListsCharacterization (getWatchList ?state'') (getWatch1 ?state'') (getWatch2 ?state'')"
      "InvariantWatchesEl (getF ?state'') (getWatch1 ?state'') (getWatch2 ?state'')" and
      "InvariantWatchesDiffer (getF ?state'') (getWatch1 ?state'') (getWatch2 ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')) &&& InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))) &&& (InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')) &&& InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))) &&& InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
[PROOF STEP]
using ih(2) ih(3) ih(4) ih(5) ih(6) ih(7)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state')); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
InvariantWatchesDiffer (getF state') (getWatch1 state') (getWatch2 state')

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

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

goal (1 subgoal):
 1. (InvariantWatchListsContainOnlyClausesFromF (getWatchList (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) &&& InvariantWatchListsUniq (getWatchList (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>))) &&& (InvariantWatchListsCharacterization (getWatchList (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch1 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch2 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) &&& InvariantWatchesEl (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch1 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch2 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>))) &&& InvariantWatchesDiffer (getF (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch1 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>)) (getWatch2 (let state' = assertLiteral (hd (getQ state')) False state' in state'\<lparr>getQ := tl (getQ state')\<rparr>))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
have "InvariantConflictClauseCharacterization (getConflictFlag ?state'') (getConflictClause ?state'') (getF ?state'') (getM ?state'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using ih(2) ih(3) ih(4) ih(5) ih(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state')); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')

goal (1 subgoal):
 1. InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
using \<open>\<not> (getConflictFlag state' \<or> getQ state' = [])\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state')); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList state') (getF state')
InvariantWatchListsUniq (getWatchList state')
InvariantWatchListsCharacterization (getWatchList state') (getWatch1 state') (getWatch2 state')
InvariantWatchesEl (getF state') (getWatch1 state') (getWatch2 state')
\<not> (getConflictFlag state' \<or> getQ state' = [])

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

goal (1 subgoal):
 1. InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
using ih(1) ih(2)
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state'))
InvariantWatchListsUniq (getWatchList (applyUnitPropagate state'))
InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state'))
InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []; InvariantWatchListsContainOnlyClausesFromF (getWatchList (applyUnitPropagate state')) (getF (applyUnitPropagate state')); InvariantWatchListsUniq (getWatchList (applyUnitPropagate state')); InvariantWatchListsCharacterization (getWatchList (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesEl (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantWatchesDiffer (getF (applyUnitPropagate state')) (getWatch1 (applyUnitPropagate state')) (getWatch2 (applyUnitPropagate state')); InvariantConflictClauseCharacterization (getConflictFlag (applyUnitPropagate state')) (getConflictClause (applyUnitPropagate state')) (getF (applyUnitPropagate state')) (getM (applyUnitPropagate state'))\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

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

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')
[PROOF STEP]
by (simp only: Let_def) (blast)
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in InvariantConflictClauseCharacterization (getConflictFlag state') (getConflictClause state') (getF state') (getM state')

goal:
No subgoals!
[PROOF STEP]
qed