[STATEMENT]
lemma InvariantWatchCharacterizationInBackjumpPrefix:
assumes
  "InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)"

shows
  "let l = getCl state in
   let level = getBackjumpLevel state in
   let prefix = prefixToLevel level (getM state) in
   let state' = state\<lparr> getConflictFlag := False, getQ := [], getM := prefix \<rparr> in
     InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?l = "getCl state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?level = "getBackjumpLevel state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?prefix = "prefixToLevel ?level (getM state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?state' = "state\<lparr> getConflictFlag := False, getQ := [], getM := ?prefix \<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
fix c w1 w2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
assume "c < length (getF state)" "Some w1 = getWatch1 state c" "Some w2 = getWatch2 state c"
[PROOF STATE]
proof (state)
this:
c < length (getF state)
Some w1 = getWatch1 state c
Some w2 = getWatch2 state c

goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
with \<open>InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
c < length (getF state)
Some w1 = getWatch1 state c
Some w2 = getWatch2 state c
[PROOF STEP]
have "watchCharacterizationCondition w1 w2 (getM state) (nth (getF state) c)"
        "watchCharacterizationCondition w2 w1 (getM state) (nth (getF state) c)"
[PROOF STATE]
proof (prove)
using this:
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
c < length (getF state)
Some w1 = getWatch1 state c
Some w2 = getWatch2 state c

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM state) (getF state ! c) &&& watchCharacterizationCondition w2 w1 (getM state) (getF state ! c)
[PROOF STEP]
unfolding InvariantWatchCharacterization_def
[PROOF STATE]
proof (prove)
using this:
\<forall>c w1 w2. 0 \<le> c \<and> c < length (getF state) \<and> Some w1 = getWatch1 state c \<and> Some w2 = getWatch2 state c \<longrightarrow> watchCharacterizationCondition w1 w2 (getM state) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM state) (getF state ! c)
c < length (getF state)
Some w1 = getWatch1 state c
Some w2 = getWatch2 state c

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM state) (getF state ! c) &&& watchCharacterizationCondition w2 w1 (getM state) (getF state ! c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
watchCharacterizationCondition w1 w2 (getM state) (getF state ! c)
watchCharacterizationCondition w2 w1 (getM state) (getF state ! c)

goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?clause = "nth (getF state) c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let "?a state w1 w2" = "\<exists> l. l el ?clause \<and> literalTrue l (elements (getM state)) \<and>
                                   elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let "?b state w1 w2" = "\<forall> l. l el ?clause \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow>
                             literalFalse l (elements (getM state)) \<and>
                             elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
have "watchCharacterizationCondition w1 w2 (getM ?state') ?clause \<and>
            watchCharacterizationCondition w2 w1 (getM ?state') ?clause"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
assume "literalFalse w1 (elements (getM ?state'))"
[PROOF STATE]
proof (state)
this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
hence "literalFalse w1 (elements (getM state))"
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. literalFalse w1 (elements (getM state))
[PROOF STEP]
using isPrefixPrefixToLevel[of "?level" "getM state"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state)

goal (1 subgoal):
 1. literalFalse w1 (elements (getM state))
[PROOF STEP]
using isPrefixElements[of "prefixToLevel ?level (getM state)" "getM state"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state)
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state) \<Longrightarrow> isPrefix (elements (prefixToLevel (getBackjumpLevel state) (getM state))) (elements (getM state))

goal (1 subgoal):
 1. literalFalse w1 (elements (getM state))
[PROOF STEP]
using prefixIsSubset[of "elements (prefixToLevel ?level (getM state))" "elements (getM state)"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state)
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state) \<Longrightarrow> isPrefix (elements (prefixToLevel (getBackjumpLevel state) (getM state))) (elements (getM state))
isPrefix (elements (prefixToLevel (getBackjumpLevel state) (getM state))) (elements (getM state)) \<Longrightarrow> set (elements (prefixToLevel (getBackjumpLevel state) (getM state))) \<subseteq> set (elements (getM state))

goal (1 subgoal):
 1. literalFalse w1 (elements (getM state))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalFalse w1 (elements (getM state))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
from \<open>literalFalse w1 (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel (opposite w1) (getM state) \<le> ?level"
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
[PROOF STEP]
using prefixToLevelElementsElementLevel[of  "opposite w1" "?level" "getM state"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
opposite w1 \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state))) \<Longrightarrow> elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
from \<open>literalFalse w1 (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel (opposite w1) (getM ?state') = elementLevel (opposite w1) (getM state)"
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)
[PROOF STEP]
using elementLevelPrefixElement
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
?e \<in> set (elements (prefixToLevel ?level ?M)) \<Longrightarrow> elementLevel ?e (prefixToLevel ?level ?M) = elementLevel ?e ?M

goal (1 subgoal):
 1. elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
have "?a ?state' w1 w2 \<or> ?b ?state' w1 w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
proof (cases "?a state w1 w2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)
[PROOF STEP]
obtain l
              where "l el ?clause" "literalTrue l (elements (getM state))"
              "elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l el getF state ! c; literalTrue l (elements (getM state)); elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l el getF state ! c
literalTrue l (elements (getM state))
elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "literalTrue l (elements (getM ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite w1) (getM state) \<le> ?level\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using elementLevelLtLevelImpliesMemberPrefixToLevel[of "l" "getM state" "?level"]
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
\<lbrakk>l \<in> set (elements (getM state)); elementLevel l (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
\<lbrakk>l \<in> set (elements (getM state)); elementLevel l (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>literalTrue l (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
\<lbrakk>l \<in> set (elements (getM state)); elementLevel l (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)
literalTrue l (elements (getM state))

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
from \<open>literalTrue l (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel l (getM ?state') = elementLevel l (getM state)"
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
[PROOF STEP]
using elementLevelPrefixElement
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
?e \<in> set (elements (prefixToLevel ?level ?M)) \<Longrightarrow> elementLevel ?e (prefixToLevel ?level ?M) = elementLevel ?e ?M

goal (1 subgoal):
 1. elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite w1) (getM ?state') = elementLevel (opposite w1) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)
elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>l el ?clause\<close>
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)
elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)
l el getF state ! c

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
assume "l el ?clause" "l \<noteq> w1" "l \<noteq> w2"
[PROOF STATE]
proof (state)
this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
hence "literalFalse l (elements (getM state))"
                "elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)"
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
[PROOF STEP]
using \<open>literalFalse w1 (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w1 (elements (getM state))

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w1 (elements (getM state))
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
[PROOF STEP]
using \<open>watchCharacterizationCondition w1 w2 (getM state) ?clause\<close>
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w1 (elements (getM state))
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)
watchCharacterizationCondition w1 w2 (getM state) (getF state ! c)

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
[PROOF STEP]
unfolding watchCharacterizationCondition_def
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w1 (elements (getM state))
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)
literalFalse w1 (elements (getM state)) \<longrightarrow> (\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state)) \<or> (\<forall>l. l el getF state ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM state)) \<and> elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state))

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM state))
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "literalFalse l (elements (getM ?state')) \<and>
                elementLevel (opposite l) (getM ?state') \<le> elementLevel (opposite w1) (getM ?state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
have "literalFalse l (elements (getM ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite w1) (getM state) \<le> ?level\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using elementLevelLtLevelImpliesMemberPrefixToLevel[of "opposite l" "getM state" "?level"]
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
\<lbrakk>opposite l \<in> set (elements (getM state)); elementLevel (opposite l) (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> opposite l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
\<lbrakk>opposite l \<in> set (elements (getM state)); elementLevel (opposite l) (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> opposite l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>literalFalse l (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w1) (getM state) \<le> getBackjumpLevel state
\<lbrakk>opposite l \<in> set (elements (getM state)); elementLevel (opposite l) (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> opposite l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
literalFalse l (elements (getM state))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
from \<open>literalFalse l (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel (opposite l) (getM ?state') = elementLevel (opposite l) (getM state)"
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
[PROOF STEP]
using elementLevelPrefixElement
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
?e \<in> set (elements (prefixToLevel ?level ?M)) \<Longrightarrow> elementLevel ?e (prefixToLevel ?level ?M) = elementLevel ?e ?M

goal (1 subgoal):
 1. elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
using \<open>elementLevel (opposite w1) (getM ?state') = elementLevel (opposite w1) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
using \<open>elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
using \<open>l el ?clause\<close>
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w1) (getM state)
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w1) (getM state)
l el getF state ! c

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?l2 el getF state ! c; ?l2 \<noteq> w1; ?l2 \<noteq> w2\<rbrakk> \<Longrightarrow> literalFalse ?l2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite ?l2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w1) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l2 el getF state ! c; ?l2 \<noteq> w1; ?l2 \<noteq> w2\<rbrakk> \<Longrightarrow> literalFalse ?l2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite ?l2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
assume "literalFalse w2 (elements (getM ?state'))"
[PROOF STATE]
proof (state)
this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
hence "literalFalse w2 (elements (getM state))"
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. literalFalse w2 (elements (getM state))
[PROOF STEP]
using isPrefixPrefixToLevel[of "?level" "getM state"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state)

goal (1 subgoal):
 1. literalFalse w2 (elements (getM state))
[PROOF STEP]
using isPrefixElements[of "prefixToLevel ?level (getM state)" "getM state"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state)
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state) \<Longrightarrow> isPrefix (elements (prefixToLevel (getBackjumpLevel state) (getM state))) (elements (getM state))

goal (1 subgoal):
 1. literalFalse w2 (elements (getM state))
[PROOF STEP]
using prefixIsSubset[of "elements (prefixToLevel ?level (getM state))" "elements (getM state)"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state)
isPrefix (prefixToLevel (getBackjumpLevel state) (getM state)) (getM state) \<Longrightarrow> isPrefix (elements (prefixToLevel (getBackjumpLevel state) (getM state))) (elements (getM state))
isPrefix (elements (prefixToLevel (getBackjumpLevel state) (getM state))) (elements (getM state)) \<Longrightarrow> set (elements (prefixToLevel (getBackjumpLevel state) (getM state))) \<subseteq> set (elements (getM state))

goal (1 subgoal):
 1. literalFalse w2 (elements (getM state))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalFalse w2 (elements (getM state))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
from \<open>literalFalse w2 (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel (opposite w2) (getM state) \<le> ?level"
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
[PROOF STEP]
using prefixToLevelElementsElementLevel[of "opposite w2" "?level" "getM state"]
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
opposite w2 \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state))) \<Longrightarrow> elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
from \<open>literalFalse w2 (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel (opposite w2) (getM ?state') = elementLevel (opposite w2) (getM state)"
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)
[PROOF STEP]
using elementLevelPrefixElement
[PROOF STATE]
proof (prove)
using this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
?e \<in> set (elements (prefixToLevel ?level ?M)) \<Longrightarrow> elementLevel ?e (prefixToLevel ?level ?M) = elementLevel ?e ?M

goal (1 subgoal):
 1. elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
have "?a ?state' w2 w1 \<or> ?b ?state' w2 w1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
proof (cases "?a state w2 w1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)
[PROOF STEP]
obtain l
              where "l el ?clause" "literalTrue l (elements (getM state))"
              "elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l el getF state ! c; literalTrue l (elements (getM state)); elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l el getF state ! c
literalTrue l (elements (getM state))
elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "literalTrue l (elements (getM ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite w2) (getM state) \<le> ?level\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using elementLevelLtLevelImpliesMemberPrefixToLevel[of "l" "getM state" "?level"]
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
\<lbrakk>l \<in> set (elements (getM state)); elementLevel l (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
\<lbrakk>l \<in> set (elements (getM state)); elementLevel l (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>literalTrue l (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
\<lbrakk>l \<in> set (elements (getM state)); elementLevel l (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)
literalTrue l (elements (getM state))

goal (1 subgoal):
 1. literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
from \<open>literalTrue l (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel l (getM ?state') = elementLevel l (getM state)"
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
[PROOF STEP]
using elementLevelPrefixElement
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
?e \<in> set (elements (prefixToLevel ?level ?M)) \<Longrightarrow> elementLevel ?e (prefixToLevel ?level ?M) = elementLevel ?e ?M

goal (1 subgoal):
 1. elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)

goal (2 subgoals):
 1. \<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
 2. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite w2) (getM ?state') = elementLevel (opposite w2) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)
elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>l el ?clause\<close>
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel l (getM state)
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)
elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)
l el getF state ! c

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
assume "l el ?clause" "l \<noteq> w1" "l \<noteq> w2"
[PROOF STATE]
proof (state)
this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
hence "literalFalse l (elements (getM state))"
                "elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)"
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
[PROOF STEP]
using \<open>literalFalse w2 (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w2 (elements (getM state))

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w2 (elements (getM state))
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
[PROOF STEP]
using \<open>watchCharacterizationCondition w2 w1 (getM state) ?clause\<close>
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w2 (elements (getM state))
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)
watchCharacterizationCondition w2 w1 (getM state) (getF state ! c)

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
[PROOF STEP]
unfolding watchCharacterizationCondition_def
[PROOF STATE]
proof (prove)
using this:
l el getF state ! c
l \<noteq> w1
l \<noteq> w2
literalFalse w2 (elements (getM state))
\<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)
literalFalse w2 (elements (getM state)) \<longrightarrow> (\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state)) \<or> (\<forall>l. l el getF state ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM state)) \<and> elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state))

goal (1 subgoal):
 1. literalFalse l (elements (getM state)) &&& elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM state))
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "literalFalse l (elements (getM ?state')) \<and>
                elementLevel (opposite l) (getM ?state') \<le> elementLevel (opposite w2) (getM ?state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
have "literalFalse l (elements (getM ?state'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite w2) (getM state) \<le> ?level\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using elementLevelLtLevelImpliesMemberPrefixToLevel[of "opposite l" "getM state" "?level"]
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
\<lbrakk>opposite l \<in> set (elements (getM state)); elementLevel (opposite l) (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> opposite l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
\<lbrakk>opposite l \<in> set (elements (getM state)); elementLevel (opposite l) (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> opposite l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
using \<open>literalFalse l (elements (getM state))\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite w2) (getM state) \<le> getBackjumpLevel state
\<lbrakk>opposite l \<in> set (elements (getM state)); elementLevel (opposite l) (getM state) \<le> getBackjumpLevel state\<rbrakk> \<Longrightarrow> opposite l \<in> set (elements (prefixToLevel (getBackjumpLevel state) (getM state)))
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
literalFalse l (elements (getM state))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
from \<open>literalFalse l (elements (getM ?state'))\<close>
[PROOF STATE]
proof (chain)
picking this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
have "elementLevel (opposite l) (getM ?state') = elementLevel (opposite l) (getM state)"
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
[PROOF STEP]
using elementLevelPrefixElement
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
?e \<in> set (elements (prefixToLevel ?level ?M)) \<Longrightarrow> elementLevel ?e (prefixToLevel ?level ?M) = elementLevel ?e ?M

goal (1 subgoal):
 1. elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
using \<open>elementLevel (opposite w2) (getM ?state') = elementLevel (opposite w2) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
using \<open>elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)\<close>
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
using \<open>l el ?clause\<close>
[PROOF STATE]
proof (prove)
using this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite l) (getM state)
elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) = elementLevel (opposite w2) (getM state)
elementLevel (opposite l) (getM state) \<le> elementLevel (opposite w2) (getM state)
l el getF state ! c

goal (1 subgoal):
 1. literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?l2 el getF state ! c; ?l2 \<noteq> w1; ?l2 \<noteq> w2\<rbrakk> \<Longrightarrow> literalFalse ?l2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite ?l2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal (1 subgoal):
 1. \<nexists>l. l el getF state ! c \<and> literalTrue l (elements (getM state)) \<and> elementLevel l (getM state) \<le> elementLevel (opposite w2) (getM state) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l2 el getF state ! c; ?l2 \<noteq> w1; ?l2 \<noteq> w2\<rbrakk> \<Longrightarrow> literalFalse ?l2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite ?l2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))

goal (1 subgoal):
 1. (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)
[PROOF STEP]
unfolding watchCharacterizationCondition_def
[PROOF STATE]
proof (prove)
using this:
literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))
literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<Longrightarrow> (\<exists>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>) ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))

goal (1 subgoal):
 1. (literalFalse w1 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<longrightarrow> (\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF state ! c \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w1) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)))) \<and> (literalFalse w2 (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<longrightarrow> (\<exists>l. l el getF state ! c \<and> literalTrue l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel l (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<or> (\<forall>l. l el getF state ! c \<and> l \<noteq> w2 \<and> l \<noteq> w1 \<longrightarrow> literalFalse l (elements (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))) \<and> elementLevel (opposite l) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) \<le> elementLevel (opposite w2) (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
watchCharacterizationCondition w1 w2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c) \<and> watchCharacterizationCondition w2 w1 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! c)

goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c2 < length (getF state); Some ?w1.2 = getWatch1 state ?c2; Some ?w2.2 = getWatch2 state ?c2\<rbrakk> \<Longrightarrow> watchCharacterizationCondition ?w1.2 ?w2.2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! ?c2) \<and> watchCharacterizationCondition ?w2.2 ?w1.2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! ?c2)

goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 < length (getF state); Some ?w1.2 = getWatch1 state ?c2; Some ?w2.2 = getWatch2 state ?c2\<rbrakk> \<Longrightarrow> watchCharacterizationCondition ?w1.2 ?w2.2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! ?c2) \<and> watchCharacterizationCondition ?w2.2 ?w1.2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! ?c2)

goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
unfolding InvariantWatchCharacterization_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 < length (getF state); Some ?w1.2 = getWatch1 state ?c2; Some ?w2.2 = getWatch2 state ?c2\<rbrakk> \<Longrightarrow> watchCharacterizationCondition ?w1.2 ?w2.2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! ?c2) \<and> watchCharacterizationCondition ?w2.2 ?w1.2 (getM (state\<lparr>getConflictFlag := False, getQ := [], getM := prefixToLevel (getBackjumpLevel state) (getM state)\<rparr>)) (getF state ! ?c2)

goal (1 subgoal):
 1. let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in \<forall>c w1 w2. 0 \<le> c \<and> c < length (getF state') \<and> Some w1 = getWatch1 state' c \<and> Some w2 = getWatch2 state' c \<longrightarrow> watchCharacterizationCondition w1 w2 (getM state') (getF state' ! c) \<and> watchCharacterizationCondition w2 w1 (getM state') (getF state' ! c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
let l = getCl state; level = getBackjumpLevel state; prefix = prefixToLevel level (getM state); state' = state\<lparr>getConflictFlag := False, getQ := [], getM := prefix\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')

goal:
No subgoals!
[PROOF STEP]
qed