[STATEMENT]
lemma InvariantReasonClausesAfterLearn:
  fixes F :: Formula and F' :: Formula and M :: LiteralTrail and C :: Clause
  assumes "InvariantReasonClauses F M" and
  "formulaEntailsClause F C" and
  "F' = F @ [C]"
  shows "InvariantReasonClauses F' M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
fix literal :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
assume "literal el elements M \<and> \<not> literal el decisions M"
[PROOF STATE]
proof (state)
this:
literal el elements M \<and> \<not> literal el decisions M

goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
with \<open>InvariantReasonClauses F M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantReasonClauses F M
literal el elements M \<and> \<not> literal el decisions M
[PROOF STEP]
obtain clause::Clause
      where "formulaEntailsClause F clause" "isReason clause literal (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M
literal el elements M \<and> \<not> literal el decisions M

goal (1 subgoal):
 1. (\<And>clause. \<lbrakk>formulaEntailsClause F clause; isReason clause literal (elements M)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding InvariantReasonClauses_def
[PROOF STATE]
proof (prove)
using this:
\<forall>literal. literal el elements M \<and> \<not> literal el decisions M \<longrightarrow> (\<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M))
literal el elements M \<and> \<not> literal el decisions M

goal (1 subgoal):
 1. (\<And>clause. \<lbrakk>formulaEntailsClause F clause; isReason clause literal (elements M)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
formulaEntailsClause F clause
isReason clause literal (elements M)

goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
from \<open>formulaEntailsClause F clause\<close> \<open>F' = F @ [C]\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsClause F clause
F' = F @ [C]
[PROOF STEP]
have "formulaEntailsClause F' clause"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F clause
F' = F @ [C]

goal (1 subgoal):
 1. formulaEntailsClause F' clause
[PROOF STEP]
by (simp add:formulaEntailsClauseAppend)
[PROOF STATE]
proof (state)
this:
formulaEntailsClause F' clause

goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
with \<open>isReason clause literal (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isReason clause literal (elements M)
formulaEntailsClause F' clause
[PROOF STEP]
have "\<exists> clause. formulaEntailsClause F' clause \<and> isReason clause literal (elements M)"
[PROOF STATE]
proof (prove)
using this:
isReason clause literal (elements M)
formulaEntailsClause F' clause

goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F' clause \<and> isReason clause literal (elements M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>clause. formulaEntailsClause F' clause \<and> isReason clause literal (elements M)

goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?literal2 el elements M \<and> \<not> ?literal2 el decisions M \<Longrightarrow> \<exists>clause. formulaEntailsClause F' clause \<and> isReason clause ?literal2 (elements M)

goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?literal2 el elements M \<and> \<not> ?literal2 el decisions M \<Longrightarrow> \<exists>clause. formulaEntailsClause F' clause \<and> isReason clause ?literal2 (elements M)

goal (1 subgoal):
 1. InvariantReasonClauses F' M
[PROOF STEP]
unfolding InvariantReasonClauses_def
[PROOF STATE]
proof (prove)
using this:
?literal2 el elements M \<and> \<not> ?literal2 el decisions M \<Longrightarrow> \<exists>clause. formulaEntailsClause F' clause \<and> isReason clause ?literal2 (elements M)

goal (1 subgoal):
 1. \<forall>literal. literal el elements M \<and> \<not> literal el decisions M \<longrightarrow> (\<exists>clause. formulaEntailsClause F' clause \<and> isReason clause literal (elements M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InvariantReasonClauses F' M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantVarsFAfterLearn:
  fixes F0 :: Formula and F :: Formula and F' :: Formula and C :: Clause
  assumes "InvariantVarsF F F0 Vbl" and
  "vars C \<subseteq> (vars F0) \<union> Vbl" and
  "F' = F @ [C]"
  shows "InvariantVarsF F' F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsF F' F0 Vbl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantVarsF F F0 Vbl
vars C \<subseteq> vars F0 \<union> Vbl
F' = F @ [C]

goal (1 subgoal):
 1. InvariantVarsF F' F0 Vbl
[PROOF STEP]
using varsAppendFormulae[of "F" "[C]"]
[PROOF STATE]
proof (prove)
using this:
InvariantVarsF F F0 Vbl
vars C \<subseteq> vars F0 \<union> Vbl
F' = F @ [C]
vars (F @ [C]) = vars F \<union> vars [C]

goal (1 subgoal):
 1. InvariantVarsF F' F0 Vbl
[PROOF STEP]
unfolding InvariantVarsF_def
[PROOF STATE]
proof (prove)
using this:
vars F \<subseteq> vars F0 \<union> Vbl
vars C \<subseteq> vars F0 \<union> Vbl
F' = F @ [C]
vars (F @ [C]) = vars F \<union> vars [C]

goal (1 subgoal):
 1. vars F' \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
by auto


[STATEMENT]
lemma InvariantEquivalentAfterLearn:
  fixes F0 :: Formula and F :: Formula and F' :: Formula and C :: Clause
  assumes "InvariantEquivalent F0 F" and
  "formulaEntailsClause F C" and
  "F' = F @ [C]"
  shows "InvariantEquivalent F0 F'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantEquivalent F0 F'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantEquivalent F0 F'
[PROOF STEP]
from \<open>InvariantEquivalent F0 F\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantEquivalent F0 F
[PROOF STEP]
have "equivalentFormulae F0 F"
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalent F0 F

goal (1 subgoal):
 1. equivalentFormulae F0 F
[PROOF STEP]
unfolding InvariantEquivalent_def
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 F

goal (1 subgoal):
 1. equivalentFormulae F0 F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
equivalentFormulae F0 F

goal (1 subgoal):
 1. InvariantEquivalent F0 F'
[PROOF STEP]
with \<open>formulaEntailsClause F C\<close> \<open>F' = F @ [C]\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsClause F C
F' = F @ [C]
equivalentFormulae F0 F
[PROOF STEP]
have "equivalentFormulae F0 (F @ [C])"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F C
F' = F @ [C]
equivalentFormulae F0 F

goal (1 subgoal):
 1. equivalentFormulae F0 (F @ [C])
[PROOF STEP]
using extendEquivalentFormulaWithEntailedClause [of "F0" "F" "C"]
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F C
F' = F @ [C]
equivalentFormulae F0 F
\<lbrakk>equivalentFormulae F0 F; formulaEntailsClause F C\<rbrakk> \<Longrightarrow> equivalentFormulae F0 (F @ [C])

goal (1 subgoal):
 1. equivalentFormulae F0 (F @ [C])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
equivalentFormulae F0 (F @ [C])

goal (1 subgoal):
 1. InvariantEquivalent F0 F'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 (F @ [C])

goal (1 subgoal):
 1. InvariantEquivalent F0 F'
[PROOF STEP]
unfolding InvariantEquivalent_def
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 (F @ [C])

goal (1 subgoal):
 1. equivalentFormulae F0 F'
[PROOF STEP]
using \<open>F' = F @ [C]\<close>
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 (F @ [C])
F' = F @ [C]

goal (1 subgoal):
 1. equivalentFormulae F0 F'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InvariantEquivalent F0 F'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantCEntailedAfterLearn:
  fixes F0 :: Formula and F :: Formula and F' :: Formula and C :: Clause
  assumes "InvariantCEntailed conflictFlag F C" and
  "F' = F @ [C]"
  shows "InvariantCEntailed conflictFlag F' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCEntailed conflictFlag F' C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantCEntailed conflictFlag F C
F' = F @ [C]

goal (1 subgoal):
 1. InvariantCEntailed conflictFlag F' C
[PROOF STEP]
unfolding InvariantCEntailed_def
[PROOF STATE]
proof (prove)
using this:
conflictFlag \<longrightarrow> formulaEntailsClause F C
F' = F @ [C]

goal (1 subgoal):
 1. conflictFlag \<longrightarrow> formulaEntailsClause F' C
[PROOF STEP]
by (auto simp add:formulaEntailsClauseAppend)


[STATEMENT]
lemma InvariantCFalseAfterExplain:
  fixes conflictFlag::bool and M::LiteralTrail and C::Clause and literal :: Literal
  assumes "InvariantCFalse conflictFlag M C" and
  "opposite literal el C" and "isReason reason literal (elements M)" and
  "C' = resolve C reason (opposite literal)"
  shows "InvariantCFalse conflictFlag M C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCFalse conflictFlag M C'
[PROOF STEP]
unfolding InvariantCFalse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflictFlag \<longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
assume "conflictFlag"
[PROOF STATE]
proof (state)
this:
conflictFlag

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
with \<open>InvariantCFalse conflictFlag M C\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantCFalse conflictFlag M C
conflictFlag
[PROOF STEP]
have "clauseFalse C (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantCFalse conflictFlag M C
conflictFlag

goal (1 subgoal):
 1. clauseFalse C (elements M)
[PROOF STEP]
unfolding InvariantCFalse_def
[PROOF STATE]
proof (prove)
using this:
conflictFlag \<longrightarrow> clauseFalse C (elements M)
conflictFlag

goal (1 subgoal):
 1. clauseFalse C (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
clauseFalse C (elements M)

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
hence "clauseFalse (removeAll (opposite literal) C) (elements M)"
[PROOF STATE]
proof (prove)
using this:
clauseFalse C (elements M)

goal (1 subgoal):
 1. clauseFalse (removeAll (opposite literal) C) (elements M)
[PROOF STEP]
by (simp add: clauseFalseIffAllLiteralsAreFalse)
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll (opposite literal) C) (elements M)

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll (opposite literal) C) (elements M)

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
from \<open>isReason reason literal (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isReason reason literal (elements M)
[PROOF STEP]
have "clauseFalse (removeAll literal reason) (elements M)"
[PROOF STATE]
proof (prove)
using this:
isReason reason literal (elements M)

goal (1 subgoal):
 1. clauseFalse (removeAll literal reason) (elements M)
[PROOF STEP]
unfolding isReason_def
[PROOF STATE]
proof (prove)
using this:
literal el reason \<and> clauseFalse (removeAll literal reason) (elements M) \<and> (\<forall>literal'. literal' el removeAll literal reason \<longrightarrow> precedes (opposite literal') literal (elements M) \<and> opposite literal' \<noteq> literal)

goal (1 subgoal):
 1. clauseFalse (removeAll literal reason) (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll literal reason) (elements M)

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
clauseFalse (removeAll (opposite literal) C) (elements M)
clauseFalse (removeAll literal reason) (elements M)
[PROOF STEP]
show "clauseFalse C' (elements M)"
[PROOF STATE]
proof (prove)
using this:
clauseFalse (removeAll (opposite literal) C) (elements M)
clauseFalse (removeAll literal reason) (elements M)

goal (1 subgoal):
 1. clauseFalse C' (elements M)
[PROOF STEP]
using \<open>C' = resolve C reason (opposite literal)\<close>
    resolveFalseClauses [of "opposite literal" "C" "elements M" "reason"]
[PROOF STATE]
proof (prove)
using this:
clauseFalse (removeAll (opposite literal) C) (elements M)
clauseFalse (removeAll literal reason) (elements M)
C' = resolve C reason (opposite literal)
\<lbrakk>clauseFalse (removeAll (opposite literal) C) (elements M); clauseFalse (removeAll (opposite (opposite literal)) reason) (elements M)\<rbrakk> \<Longrightarrow> clauseFalse (resolve C reason (opposite literal)) (elements M)

goal (1 subgoal):
 1. clauseFalse C' (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
clauseFalse C' (elements M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantCEntailedAfterExplain:
  fixes conflictFlag::bool and M::LiteralTrail and C::Clause and literal :: Literal and reason :: Clause
  assumes "InvariantCEntailed conflictFlag F C" and
  "formulaEntailsClause F reason" and "C' = (resolve C reason (opposite l))"
  shows "InvariantCEntailed conflictFlag F C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCEntailed conflictFlag F C'
[PROOF STEP]
unfolding InvariantCEntailed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflictFlag \<longrightarrow> formulaEntailsClause F C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> formulaEntailsClause F C'
[PROOF STEP]
assume "conflictFlag"
[PROOF STATE]
proof (state)
this:
conflictFlag

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> formulaEntailsClause F C'
[PROOF STEP]
with \<open>InvariantCEntailed conflictFlag F C\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantCEntailed conflictFlag F C
conflictFlag
[PROOF STEP]
have "formulaEntailsClause F C"
[PROOF STATE]
proof (prove)
using this:
InvariantCEntailed conflictFlag F C
conflictFlag

goal (1 subgoal):
 1. formulaEntailsClause F C
[PROOF STEP]
unfolding InvariantCEntailed_def
[PROOF STATE]
proof (prove)
using this:
conflictFlag \<longrightarrow> formulaEntailsClause F C
conflictFlag

goal (1 subgoal):
 1. formulaEntailsClause F C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaEntailsClause F C

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> formulaEntailsClause F C'
[PROOF STEP]
with \<open>formulaEntailsClause F reason\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsClause F reason
formulaEntailsClause F C
[PROOF STEP]
show "formulaEntailsClause F C'"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F reason
formulaEntailsClause F C

goal (1 subgoal):
 1. formulaEntailsClause F C'
[PROOF STEP]
using \<open>C' = (resolve C reason (opposite l))\<close>
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F reason
formulaEntailsClause F C
C' = resolve C reason (opposite l)

goal (1 subgoal):
 1. formulaEntailsClause F C'
[PROOF STEP]
by (simp add:formulaEntailsResolvent)
[PROOF STATE]
proof (state)
this:
formulaEntailsClause F C'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invariantCFalseAfterConflict:
  fixes conflictFlag::bool and conflictFlag'::bool and M::LiteralTrail and F :: Formula and clause :: Clause and C' :: Clause
  assumes "conflictFlag = False" and
  "formulaFalse F (elements M)" and "clause el F" "clauseFalse clause (elements M)" and
  "C' = clause" and "conflictFlag' = True"
  shows "InvariantCFalse conflictFlag' M C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCFalse conflictFlag' M C'
[PROOF STEP]
unfolding InvariantCFalse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflictFlag' \<longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conflictFlag' \<Longrightarrow> clauseFalse C' (elements M)
[PROOF STEP]
from \<open>conflictFlag' = True\<close>
[PROOF STATE]
proof (chain)
picking this:
conflictFlag' = True
[PROOF STEP]
show "clauseFalse C' (elements M)"
[PROOF STATE]
proof (prove)
using this:
conflictFlag' = True

goal (1 subgoal):
 1. clauseFalse C' (elements M)
[PROOF STEP]
using \<open>clauseFalse clause (elements M)\<close> \<open>C' = clause\<close>
[PROOF STATE]
proof (prove)
using this:
conflictFlag' = True
clauseFalse clause (elements M)
C' = clause

goal (1 subgoal):
 1. clauseFalse C' (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
clauseFalse C' (elements M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invariantCEntailedAfterConflict:
  fixes conflictFlag::bool and conflictFlag'::bool and M::LiteralTrail and F :: Formula and clause :: Clause and C' :: Clause
  assumes "conflictFlag = False" and
  "formulaFalse F (elements M)" and "clause el F" and "clauseFalse clause (elements M)" and
  "C' = clause" and "conflictFlag' = True"
  shows "InvariantCEntailed conflictFlag' F C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCEntailed conflictFlag' F C'
[PROOF STEP]
unfolding InvariantCEntailed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflictFlag' \<longrightarrow> formulaEntailsClause F C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conflictFlag' \<Longrightarrow> formulaEntailsClause F C'
[PROOF STEP]
from \<open>conflictFlag' = True\<close>
[PROOF STATE]
proof (chain)
picking this:
conflictFlag' = True
[PROOF STEP]
show "formulaEntailsClause F C'"
[PROOF STATE]
proof (prove)
using this:
conflictFlag' = True

goal (1 subgoal):
 1. formulaEntailsClause F C'
[PROOF STEP]
using \<open>clause el F\<close> \<open>C' = clause\<close>
[PROOF STATE]
proof (prove)
using this:
conflictFlag' = True
clause el F
C' = clause

goal (1 subgoal):
 1. formulaEntailsClause F C'
[PROOF STEP]
by (simp add:formulaEntailsItsClauses)
[PROOF STATE]
proof (state)
this:
formulaEntailsClause F C'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unsatReport:
  fixes F :: Formula and M :: LiteralTrail and F0 :: Formula
  assumes "InvariantImpliedLiterals F M" and "InvariantEquivalent F0 F" and
  "decisions M = []" and "formulaFalse F (elements M)"
  shows "\<not> satisfiable F0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
have "formulaEntailsValuation F (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
fix literal::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
assume "literal el (elements M)"
[PROOF STATE]
proof (state)
this:
literal el elements M

goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
from \<open>decisions M = []\<close>
[PROOF STATE]
proof (chain)
picking this:
decisions M = []
[PROOF STEP]
have "decisionsTo literal M = []"
[PROOF STATE]
proof (prove)
using this:
decisions M = []

goal (1 subgoal):
 1. decisionsTo literal M = []
[PROOF STEP]
by (simp add:markedElementsEmptyImpliesMarkedElementsToEmpty)
[PROOF STATE]
proof (state)
this:
decisionsTo literal M = []

goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
with \<open>literal el (elements M)\<close> \<open>InvariantImpliedLiterals F M\<close>
[PROOF STATE]
proof (chain)
picking this:
literal el elements M
InvariantImpliedLiterals F M
decisionsTo literal M = []
[PROOF STEP]
have "formulaEntailsLiteral F literal"
[PROOF STATE]
proof (prove)
using this:
literal el elements M
InvariantImpliedLiterals F M
decisionsTo literal M = []

goal (1 subgoal):
 1. formulaEntailsLiteral F literal
[PROOF STEP]
unfolding InvariantImpliedLiterals_def
[PROOF STATE]
proof (prove)
using this:
literal el elements M
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
decisionsTo literal M = []

goal (1 subgoal):
 1. formulaEntailsLiteral F literal
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral F literal

goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?literal2 el elements M \<Longrightarrow> formulaEntailsLiteral F ?literal2

goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?literal2 el elements M \<Longrightarrow> formulaEntailsLiteral F ?literal2

goal (1 subgoal):
 1. formulaEntailsValuation F (elements M)
[PROOF STEP]
unfolding formulaEntailsValuation_def
[PROOF STATE]
proof (prove)
using this:
?literal2 el elements M \<Longrightarrow> formulaEntailsLiteral F ?literal2

goal (1 subgoal):
 1. \<forall>literal. literal el elements M \<longrightarrow> formulaEntailsLiteral F literal
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaEntailsValuation F (elements M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
formulaEntailsValuation F (elements M)

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
with \<open>formulaFalse F (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaFalse F (elements M)
formulaEntailsValuation F (elements M)
[PROOF STEP]
have "\<not> satisfiable F"
[PROOF STATE]
proof (prove)
using this:
formulaFalse F (elements M)
formulaEntailsValuation F (elements M)

goal (1 subgoal):
 1. \<not> satisfiable F
[PROOF STEP]
by (simp add:formulaFalseInEntailedValuationIsUnsatisfiable)
[PROOF STATE]
proof (state)
this:
\<not> satisfiable F

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
with \<open>InvariantEquivalent F0 F\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantEquivalent F0 F
\<not> satisfiable F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalent F0 F
\<not> satisfiable F

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
unfolding InvariantEquivalent_def
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 F
\<not> satisfiable F

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
by (simp add:satisfiableEquivalent)
[PROOF STATE]
proof (state)
this:
\<not> satisfiable F0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unsatReportExtensiveExplain:
  fixes F :: Formula and M :: LiteralTrail and F0 :: Formula and C :: Clause and conflictFlag :: bool
  assumes "InvariantEquivalent F0 F" and "InvariantCEntailed conflictFlag F C" and
  "conflictFlag" and "C = []"
  shows "\<not> satisfiable F0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
from \<open>conflictFlag\<close> \<open>InvariantCEntailed conflictFlag F C\<close>
[PROOF STATE]
proof (chain)
picking this:
conflictFlag
InvariantCEntailed conflictFlag F C
[PROOF STEP]
have "formulaEntailsClause F C"
[PROOF STATE]
proof (prove)
using this:
conflictFlag
InvariantCEntailed conflictFlag F C

goal (1 subgoal):
 1. formulaEntailsClause F C
[PROOF STEP]
unfolding InvariantCEntailed_def
[PROOF STATE]
proof (prove)
using this:
conflictFlag
conflictFlag \<longrightarrow> formulaEntailsClause F C

goal (1 subgoal):
 1. formulaEntailsClause F C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaEntailsClause F C

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
with \<open>C=[]\<close>
[PROOF STATE]
proof (chain)
picking this:
C = []
formulaEntailsClause F C
[PROOF STEP]
have "\<not> satisfiable F"
[PROOF STATE]
proof (prove)
using this:
C = []
formulaEntailsClause F C

goal (1 subgoal):
 1. \<not> satisfiable F
[PROOF STEP]
by (simp add:formulaUnsatIffImpliesEmptyClause)
[PROOF STATE]
proof (state)
this:
\<not> satisfiable F

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
with \<open>InvariantEquivalent F0 F\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantEquivalent F0 F
\<not> satisfiable F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalent F0 F
\<not> satisfiable F

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
unfolding InvariantEquivalent_def
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 F
\<not> satisfiable F

goal (1 subgoal):
 1. \<not> satisfiable F0
[PROOF STEP]
by (simp add:satisfiableEquivalent)
[PROOF STATE]
proof (state)
this:
\<not> satisfiable F0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma satReport:
  fixes F0 :: Formula and F :: Formula and M::LiteralTrail
  assumes "vars F0 \<subseteq> Vbl" and "InvariantVarsF F F0 Vbl" and "InvariantConsistent M" and "InvariantEquivalent F0 F" and
  "\<not> formulaFalse F (elements M)" and "vars (elements M) \<supseteq> Vbl"
  shows "model (elements M) F0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
from \<open>InvariantConsistent M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
[PROOF STEP]
have "consistent (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M

goal (1 subgoal):
 1. consistent (elements M)
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)

goal (1 subgoal):
 1. consistent (elements M)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
consistent (elements M)

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
consistent (elements M)

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
from \<open>InvariantVarsF F F0 Vbl\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantVarsF F F0 Vbl
[PROOF STEP]
have "vars F \<subseteq> vars F0 \<union> Vbl"
[PROOF STATE]
proof (prove)
using this:
InvariantVarsF F F0 Vbl

goal (1 subgoal):
 1. vars F \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
unfolding InvariantVarsF_def
[PROOF STATE]
proof (prove)
using this:
vars F \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. vars F \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vars F \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
with \<open>vars F0 \<subseteq> Vbl\<close>
[PROOF STATE]
proof (chain)
picking this:
vars F0 \<subseteq> Vbl
vars F \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
have "vars F \<subseteq> Vbl"
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> Vbl
vars F \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. vars F \<subseteq> Vbl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars F \<subseteq> Vbl

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
with \<open>vars (elements M) \<supseteq> Vbl\<close>
[PROOF STATE]
proof (chain)
picking this:
Vbl \<subseteq> vars (elements M)
vars F \<subseteq> Vbl
[PROOF STEP]
have "vars F \<subseteq> vars (elements M)"
[PROOF STATE]
proof (prove)
using this:
Vbl \<subseteq> vars (elements M)
vars F \<subseteq> Vbl

goal (1 subgoal):
 1. vars F \<subseteq> vars (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars F \<subseteq> vars (elements M)

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
hence "formulaTrue F (elements M) \<or> formulaFalse F (elements M)"
[PROOF STATE]
proof (prove)
using this:
vars F \<subseteq> vars (elements M)

goal (1 subgoal):
 1. formulaTrue F (elements M) \<or> formulaFalse F (elements M)
[PROOF STEP]
by (simp add:totalValuationForFormulaDefinesItsValue)
[PROOF STATE]
proof (state)
this:
formulaTrue F (elements M) \<or> formulaFalse F (elements M)

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
with \<open>\<not> formulaFalse F (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> formulaFalse F (elements M)
formulaTrue F (elements M) \<or> formulaFalse F (elements M)
[PROOF STEP]
have "formulaTrue F (elements M)"
[PROOF STATE]
proof (prove)
using this:
\<not> formulaFalse F (elements M)
formulaTrue F (elements M) \<or> formulaFalse F (elements M)

goal (1 subgoal):
 1. formulaTrue F (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaTrue F (elements M)

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
consistent (elements M)
formulaTrue F (elements M)
[PROOF STEP]
have "model (elements M) F"
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
formulaTrue F (elements M)

goal (1 subgoal):
 1. model (elements M) F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model (elements M) F

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
with \<open>InvariantEquivalent F0 F\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantEquivalent F0 F
model (elements M) F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantEquivalent F0 F
model (elements M) F

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
unfolding InvariantEquivalent_def
[PROOF STATE]
proof (prove)
using this:
equivalentFormulae F0 F
model (elements M) F

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
unfolding equivalentFormulae_def
[PROOF STATE]
proof (prove)
using this:
\<forall>valuation. model valuation F0 = model valuation F
model (elements M) F

goal (1 subgoal):
 1. model (elements M) F0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
model (elements M) F0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lastAssertedLiteralHasHighestElementLevel:
  fixes literal :: Literal and clause :: Clause and M :: LiteralTrail
  assumes "isLastAssertedLiteral literal clause (elements M)" and "uniq (elements M)"
  shows "\<forall> l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M <= elementLevel literal M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
fix l' :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
assume "l' el clause" "l' el elements M"
[PROOF STATE]
proof (state)
this:
l' el clause
l' el elements M

goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
hence "elementLevel l' M <= elementLevel literal M"
[PROOF STATE]
proof (prove)
using this:
l' el clause
l' el elements M

goal (1 subgoal):
 1. elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
proof (cases "l' = literal")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l' el clause; l' el elements M; l' = literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
 2. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l' = literal

goal (2 subgoals):
 1. \<lbrakk>l' el clause; l' el elements M; l' = literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
 2. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l' = literal

goal (1 subgoal):
 1. elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elementLevel l' M \<le> elementLevel literal M

goal (1 subgoal):
 1. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
l' \<noteq> literal

goal (1 subgoal):
 1. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
from \<open>isLastAssertedLiteral literal clause (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isLastAssertedLiteral literal clause (elements M)
[PROOF STEP]
have "literalTrue literal (elements M)"
        "\<forall> l. l el clause \<and> l \<noteq> literal \<longrightarrow> \<not>  precedes literal l (elements M)"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral literal clause (elements M)

goal (1 subgoal):
 1. literalTrue literal (elements M) &&& \<forall>l. l el clause \<and> l \<noteq> literal \<longrightarrow> \<not> precedes literal l (elements M)
[PROOF STEP]
by (auto simp add:isLastAssertedLiteral_def)
[PROOF STATE]
proof (state)
this:
literalTrue literal (elements M)
\<forall>l. l el clause \<and> l \<noteq> literal \<longrightarrow> \<not> precedes literal l (elements M)

goal (1 subgoal):
 1. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
with \<open>l' el clause\<close> False
[PROOF STATE]
proof (chain)
picking this:
l' el clause
l' \<noteq> literal
literalTrue literal (elements M)
\<forall>l. l el clause \<and> l \<noteq> literal \<longrightarrow> \<not> precedes literal l (elements M)
[PROOF STEP]
have "\<not> precedes literal l' (elements M)"
[PROOF STATE]
proof (prove)
using this:
l' el clause
l' \<noteq> literal
literalTrue literal (elements M)
\<forall>l. l el clause \<and> l \<noteq> literal \<longrightarrow> \<not> precedes literal l (elements M)

goal (1 subgoal):
 1. \<not> precedes literal l' (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> precedes literal l' (elements M)

goal (1 subgoal):
 1. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
with False \<open>l' el (elements M)\<close> \<open>literalTrue literal (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
l' \<noteq> literal
l' el elements M
literalTrue literal (elements M)
\<not> precedes literal l' (elements M)
[PROOF STEP]
have "precedes l' literal (elements M)"
[PROOF STATE]
proof (prove)
using this:
l' \<noteq> literal
l' el elements M
literalTrue literal (elements M)
\<not> precedes literal l' (elements M)

goal (1 subgoal):
 1. precedes l' literal (elements M)
[PROOF STEP]
using precedesTotalOrder [of "l'"  "elements M" "literal"]
[PROOF STATE]
proof (prove)
using this:
l' \<noteq> literal
l' el elements M
literalTrue literal (elements M)
\<not> precedes literal l' (elements M)
\<lbrakk>l' \<in> set (elements M); literal \<in> set (elements M)\<rbrakk> \<Longrightarrow> l' = literal \<or> precedes l' literal (elements M) \<or> precedes literal l' (elements M)

goal (1 subgoal):
 1. precedes l' literal (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
precedes l' literal (elements M)

goal (1 subgoal):
 1. \<lbrakk>l' el clause; l' el elements M; l' \<noteq> literal\<rbrakk> \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
with \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
uniq (elements M)
precedes l' literal (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
precedes l' literal (elements M)

goal (1 subgoal):
 1. elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
using elementLevelPrecedesLeq [of "l'" "literal" "M"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
precedes l' literal (elements M)
precedes l' literal (elements M) \<Longrightarrow> elementLevel l' M \<le> elementLevel literal M

goal (1 subgoal):
 1. elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elementLevel l' M \<le> elementLevel literal M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
elementLevel l' M \<le> elementLevel literal M

goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?l'2 el clause; ?l'2 el elements M\<rbrakk> \<Longrightarrow> elementLevel ?l'2 M \<le> elementLevel literal M

goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el clause; ?l'2 el elements M\<rbrakk> \<Longrightarrow> elementLevel ?l'2 M \<le> elementLevel literal M

goal (1 subgoal):
 1. \<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el clause \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel literal M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma backjumpLevelZero:
  fixes M :: LiteralTrail and C :: Clause and l :: Literal
  assumes
  "isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)" and
  "elementLevel (opposite l) M > 0" and
  "set C = {l}"
  shows
  "isBackjumpLevel 0 l C M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isBackjumpLevel 0 l C M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isBackjumpLevel 0 l C M
[PROOF STEP]
have "\<forall> l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
fix l'::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
assume "l' el C \<and> l' \<noteq> l"
[PROOF STATE]
proof (state)
this:
l' el C \<and> l' \<noteq> l

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
hence "False"
[PROOF STATE]
proof (prove)
using this:
l' el C \<and> l' \<noteq> l

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>set C = {l}\<close>
[PROOF STATE]
proof (prove)
using this:
l' el C \<and> l' \<noteq> l
set C = {l}

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

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l'2 el C \<and> ?l'2 \<noteq> l \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?l'2 el C \<and> ?l'2 \<noteq> l \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0

goal (1 subgoal):
 1. isBackjumpLevel 0 l C M
[PROOF STEP]
with \<open>elementLevel (opposite l) M > 0\<close>
    \<open>isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0

goal (1 subgoal):
 1. isBackjumpLevel 0 l C M
[PROOF STEP]
unfolding isBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
0 < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0

goal (1 subgoal):
 1. isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M) \<and> 0 \<le> 0 \<and> 0 < elementLevel (opposite l) M \<and> (\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isBackjumpLevel 0 l C M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma backjumpLevelLastLast:
  fixes M :: LiteralTrail and C :: Clause and l :: Literal
  assumes
  "isUIP l C M" and
  "uniq (elements M)" and
  "clauseFalse C (elements M)" and
  "isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)"
  shows
  "isBackjumpLevel (elementLevel (opposite ll) M) l C M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
from \<open>isUIP l C M\<close>
[PROOF STATE]
proof (chain)
picking this:
isUIP l C M
[PROOF STEP]
have "isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)"
[PROOF STATE]
proof (prove)
using this:
isUIP l C M

goal (1 subgoal):
 1. isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)
[PROOF STEP]
unfolding isUIP_def
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M) \<and> (\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M)

goal (1 subgoal):
 1. isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
from \<open>isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)
[PROOF STEP]
have "literalTrue (opposite ll) (elements M)" "(opposite ll) el (removeAll (opposite l) (oppositeLiteralList C))"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)

goal (1 subgoal):
 1. literalTrue (opposite ll) (elements M) &&& opposite ll el removeAll (opposite l) (oppositeLiteralList C)
[PROOF STEP]
unfolding isLastAssertedLiteral_def
[PROOF STATE]
proof (prove)
using this:
opposite ll el removeAll (opposite l) (oppositeLiteralList C) \<and> literalTrue (opposite ll) (elements M) \<and> (\<forall>literal'. literal' el removeAll (opposite l) (oppositeLiteralList C) \<and> literal' \<noteq> opposite ll \<longrightarrow> \<not> precedes (opposite ll) literal' (elements M))

goal (1 subgoal):
 1. literalTrue (opposite ll) (elements M) &&& opposite ll el removeAll (opposite l) (oppositeLiteralList C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literalTrue (opposite ll) (elements M)
opposite ll el removeAll (opposite l) (oppositeLiteralList C)

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
have "\<forall> l'. l' el (oppositeLiteralList C) \<longrightarrow> literalTrue l' (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
fix l'::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
assume "l' el oppositeLiteralList C"
[PROOF STATE]
proof (state)
this:
l' el oppositeLiteralList C

goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
hence "opposite l' el C"
[PROOF STATE]
proof (prove)
using this:
l' el oppositeLiteralList C

goal (1 subgoal):
 1. opposite l' el C
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "opposite l'" "C"]
[PROOF STATE]
proof (prove)
using this:
l' el oppositeLiteralList C
opposite l' el C = opposite (opposite l') el oppositeLiteralList C

goal (1 subgoal):
 1. opposite l' el C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
opposite l' el C

goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
with \<open>clauseFalse C (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
clauseFalse C (elements M)
opposite l' el C
[PROOF STEP]
have "literalTrue l' (elements M)"
[PROOF STATE]
proof (prove)
using this:
clauseFalse C (elements M)
opposite l' el C

goal (1 subgoal):
 1. literalTrue l' (elements M)
[PROOF STEP]
by (auto simp add: clauseFalseIffAllLiteralsAreFalse)
[PROOF STATE]
proof (state)
this:
literalTrue l' (elements M)

goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l'2 el oppositeLiteralList C \<Longrightarrow> literalTrue ?l'2 (elements M)

goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?l'2 el oppositeLiteralList C \<Longrightarrow> literalTrue ?l'2 (elements M)

goal (1 subgoal):
 1. \<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
have "\<forall> l'. l' el C \<and> l' \<noteq> l  \<longrightarrow>
    elementLevel (opposite l') M <= elementLevel (opposite ll) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
fix l' :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
assume "l' el C \<and> l' \<noteq> l"
[PROOF STATE]
proof (state)
this:
l' el C \<and> l' \<noteq> l

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
hence "(opposite l') el (oppositeLiteralList C)" "opposite l' \<noteq> opposite l"
[PROOF STATE]
proof (prove)
using this:
l' el C \<and> l' \<noteq> l

goal (1 subgoal):
 1. opposite l' el oppositeLiteralList C &&& opposite l' \<noteq> opposite l
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList
[PROOF STATE]
proof (prove)
using this:
l' el C \<and> l' \<noteq> l
?literal el ?literalList = opposite ?literal el oppositeLiteralList ?literalList

goal (1 subgoal):
 1. opposite l' el oppositeLiteralList C &&& opposite l' \<noteq> opposite l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
opposite l' el oppositeLiteralList C
opposite l' \<noteq> opposite l

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
hence "opposite l' el (removeAll (opposite l) (oppositeLiteralList C))"
[PROOF STATE]
proof (prove)
using this:
opposite l' el oppositeLiteralList C
opposite l' \<noteq> opposite l

goal (1 subgoal):
 1. opposite l' el removeAll (opposite l) (oppositeLiteralList C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
opposite l' el removeAll (opposite l) (oppositeLiteralList C)

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
from \<open>opposite l' el (oppositeLiteralList C)\<close>
        \<open>\<forall> l'. l' el (oppositeLiteralList C) \<longrightarrow> literalTrue l' (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
opposite l' el oppositeLiteralList C
\<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)
[PROOF STEP]
have "literalTrue (opposite l') (elements M)"
[PROOF STATE]
proof (prove)
using this:
opposite l' el oppositeLiteralList C
\<forall>l'. l' el oppositeLiteralList C \<longrightarrow> literalTrue l' (elements M)

goal (1 subgoal):
 1. literalTrue (opposite l') (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literalTrue (opposite l') (elements M)

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
with \<open>opposite l' el (removeAll (opposite l) (oppositeLiteralList C))\<close>
        \<open>isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)\<close>
        \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
opposite l' el removeAll (opposite l) (oppositeLiteralList C)
isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)
uniq (elements M)
literalTrue (opposite l') (elements M)
[PROOF STEP]
have "elementLevel (opposite l') M <= elementLevel (opposite ll) M"
[PROOF STATE]
proof (prove)
using this:
opposite l' el removeAll (opposite l) (oppositeLiteralList C)
isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)
uniq (elements M)
literalTrue (opposite l') (elements M)

goal (1 subgoal):
 1. elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
using lastAssertedLiteralHasHighestElementLevel[of "opposite ll" "removeAll (opposite l) (oppositeLiteralList C)" "M"]
[PROOF STATE]
proof (prove)
using this:
opposite l' el removeAll (opposite l) (oppositeLiteralList C)
isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M)
uniq (elements M)
literalTrue (opposite l') (elements M)
\<lbrakk>isLastAssertedLiteral (opposite ll) (removeAll (opposite l) (oppositeLiteralList C)) (elements M); uniq (elements M)\<rbrakk> \<Longrightarrow> \<forall>l'. l' el removeAll (opposite l) (oppositeLiteralList C) \<and> l' el elements M \<longrightarrow> elementLevel l' M \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elementLevel (opposite l') M \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l'2 el C \<and> ?l'2 \<noteq> l \<Longrightarrow> elementLevel (opposite ?l'2) M \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?l'2 el C \<and> ?l'2 \<noteq> l \<Longrightarrow> elementLevel (opposite ?l'2) M \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
from \<open>literalTrue (opposite ll) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
literalTrue (opposite ll) (elements M)
[PROOF STEP]
have "elementLevel (opposite ll) M \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
literalTrue (opposite ll) (elements M)

goal (1 subgoal):
 1. 0 \<le> elementLevel (opposite ll) M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> elementLevel (opposite ll) M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
from \<open>(opposite ll) el (removeAll (opposite l) (oppositeLiteralList C))\<close>
[PROOF STATE]
proof (chain)
picking this:
opposite ll el removeAll (opposite l) (oppositeLiteralList C)
[PROOF STEP]
have "ll el C" and "ll \<noteq> l"
[PROOF STATE]
proof (prove)
using this:
opposite ll el removeAll (opposite l) (oppositeLiteralList C)

goal (1 subgoal):
 1. ll el C &&& ll \<noteq> l
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "ll" "C"]
[PROOF STATE]
proof (prove)
using this:
opposite ll el removeAll (opposite l) (oppositeLiteralList C)
ll el C = opposite ll el oppositeLiteralList C

goal (1 subgoal):
 1. ll el C &&& ll \<noteq> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ll el C
ll \<noteq> l

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
from \<open>isUIP l C M\<close>
[PROOF STATE]
proof (chain)
picking this:
isUIP l C M
[PROOF STEP]
have "\<forall> l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M"
[PROOF STATE]
proof (prove)
using this:
isUIP l C M

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
unfolding isUIP_def
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M) \<and> (\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M)

goal (1 subgoal):
 1. \<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
with \<open>ll el C\<close> \<open>ll \<noteq> l\<close>
[PROOF STATE]
proof (chain)
picking this:
ll el C
ll \<noteq> l
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
have "elementLevel (opposite ll) M < elementLevel (opposite l) M"
[PROOF STATE]
proof (prove)
using this:
ll el C
ll \<noteq> l
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M

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

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
0 \<le> elementLevel (opposite ll) M
elementLevel (opposite ll) M < elementLevel (opposite l) M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
0 \<le> elementLevel (opposite ll) M
elementLevel (opposite ll) M < elementLevel (opposite l) M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
using \<open>isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
0 \<le> elementLevel (opposite ll) M
elementLevel (opposite ll) M < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (opposite ll) M) l C M
[PROOF STEP]
unfolding isBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M
0 \<le> elementLevel (opposite ll) M
elementLevel (opposite ll) M < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M)

goal (1 subgoal):
 1. isLastAssertedLiteral (opposite l) (oppositeLiteralList C) (elements M) \<and> 0 \<le> elementLevel (opposite ll) M \<and> elementLevel (opposite ll) M < elementLevel (opposite l) M \<and> (\<forall>l'. l' el C \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> elementLevel (opposite ll) M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isBackjumpLevel (elementLevel (opposite ll) M) l C M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isUIPExistsBackjumpLevel:
  fixes M :: LiteralTrail and c :: Clause and l :: Literal
  assumes
  "clauseFalse c (elements M)" and
  "isUIP l c M" and
  "uniq (elements M)" and
  "elementLevel (opposite l) M > 0"
  shows
  "\<exists> level. (isBackjumpLevel level l c M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
from \<open>isUIP l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
isUIP l c M
[PROOF STEP]
have "isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)"
[PROOF STATE]
proof (prove)
using this:
isUIP l c M

goal (1 subgoal):
 1. isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
[PROOF STEP]
unfolding isUIP_def
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M) \<and> (\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M)

goal (1 subgoal):
 1. isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
proof (cases "set c = {l}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set c = {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
 2. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
set c = {l}

goal (2 subgoals):
 1. set c = {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
 2. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
with \<open>elementLevel (opposite l) M > 0\<close> \<open>isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
set c = {l}
[PROOF STEP]
have "isBackjumpLevel 0 l c M"
[PROOF STATE]
proof (prove)
using this:
0 < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
set c = {l}

goal (1 subgoal):
 1. isBackjumpLevel 0 l c M
[PROOF STEP]
using backjumpLevelZero[of "l" "c" "M"]
[PROOF STATE]
proof (prove)
using this:
0 < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
set c = {l}
\<lbrakk>isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M); 0 < elementLevel (opposite l) M; set c = {l}\<rbrakk> \<Longrightarrow> isBackjumpLevel 0 l c M

goal (1 subgoal):
 1. isBackjumpLevel 0 l c M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isBackjumpLevel 0 l c M

goal (2 subgoals):
 1. set c = {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
 2. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel 0 l c M

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>level. isBackjumpLevel level l c M

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
set c \<noteq> {l}

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
have "\<exists> literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
let ?ll = "getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
from \<open>clauseFalse c (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
clauseFalse c (elements M)
[PROOF STEP]
have "clauseFalse (removeAll l c) (elements M)"
[PROOF STATE]
proof (prove)
using this:
clauseFalse c (elements M)

goal (1 subgoal):
 1. clauseFalse (removeAll l c) (elements M)
[PROOF STEP]
by (simp add:clauseFalseRemove)
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll l c) (elements M)

goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll l c) (elements M)

goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
have "removeAll l c \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
have "(set c) \<subseteq> {l} \<union> set (removeAll l c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set c \<subseteq> {l} \<union> set (removeAll l c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set c \<subseteq> {l} \<union> set (removeAll l c)

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
from \<open>isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
[PROOF STEP]
have "(opposite l) el oppositeLiteralList c"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. opposite l el oppositeLiteralList c
[PROOF STEP]
unfolding isLastAssertedLiteral_def
[PROOF STATE]
proof (prove)
using this:
opposite l el oppositeLiteralList c \<and> literalTrue (opposite l) (elements M) \<and> (\<forall>literal'. literal' el oppositeLiteralList c \<and> literal' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) literal' (elements M))

goal (1 subgoal):
 1. opposite l el oppositeLiteralList c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
opposite l el oppositeLiteralList c

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
hence "l el c"
[PROOF STATE]
proof (prove)
using this:
opposite l el oppositeLiteralList c

goal (1 subgoal):
 1. l el c
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "l" "c"]
[PROOF STATE]
proof (prove)
using this:
opposite l el oppositeLiteralList c
l el c = opposite l el oppositeLiteralList c

goal (1 subgoal):
 1. l el c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l el c

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
hence "l \<in> set c"
[PROOF STATE]
proof (prove)
using this:
l el c

goal (1 subgoal):
 1. l \<in> set c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<in> set c

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
l \<in> set c

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> removeAll l c \<noteq> []

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
hence "set (removeAll l c) = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> removeAll l c \<noteq> []

goal (1 subgoal):
 1. set (removeAll l c) = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (removeAll l c) = {}

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
with \<open>(set c) \<subseteq> {l} \<union> set (removeAll l c)\<close>
[PROOF STATE]
proof (chain)
picking this:
set c \<subseteq> {l} \<union> set (removeAll l c)
set (removeAll l c) = {}
[PROOF STEP]
have "set c \<subseteq> {l}"
[PROOF STATE]
proof (prove)
using this:
set c \<subseteq> {l} \<union> set (removeAll l c)
set (removeAll l c) = {}

goal (1 subgoal):
 1. set c \<subseteq> {l}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set c \<subseteq> {l}

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
with \<open>l \<in> set c\<close>
[PROOF STATE]
proof (chain)
picking this:
l \<in> set c
set c \<subseteq> {l}
[PROOF STEP]
have "set c = {l}"
[PROOF STATE]
proof (prove)
using this:
l \<in> set c
set c \<subseteq> {l}

goal (1 subgoal):
 1. set c = {l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set c = {l}

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
set c \<noteq> {l}
set c = {l}
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
set c \<noteq> {l}
set c = {l}

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

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> removeAll l c \<noteq> [] \<Longrightarrow> False

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> removeAll l c \<noteq> [] \<Longrightarrow> False

goal (1 subgoal):
 1. removeAll l c \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
removeAll l c \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
removeAll l c \<noteq> []

goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
clauseFalse (removeAll l c) (elements M)
removeAll l c \<noteq> []
[PROOF STEP]
have "isLastAssertedLiteral ?ll (oppositeLiteralList (removeAll l c)) (elements M)"
[PROOF STATE]
proof (prove)
using this:
clauseFalse (removeAll l c) (elements M)
removeAll l c \<noteq> []

goal (1 subgoal):
 1. isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)
[PROOF STEP]
using \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
clauseFalse (removeAll l c) (elements M)
removeAll l c \<noteq> []
uniq (elements M)

goal (1 subgoal):
 1. isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)
[PROOF STEP]
using getLastAssertedLiteralCharacterization [of "removeAll l c" "elements M"]
[PROOF STATE]
proof (prove)
using this:
clauseFalse (removeAll l c) (elements M)
removeAll l c \<noteq> []
uniq (elements M)
\<lbrakk>clauseFalse (removeAll l c) (elements M); removeAll l c \<noteq> []; uniq (elements M)\<rbrakk> \<Longrightarrow> isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)

goal (1 subgoal):
 1. isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)

goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
hence "isLastAssertedLiteral ?ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)

goal (1 subgoal):
 1. isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
using oppositeLiteralListRemove[of "l" "c"]
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (oppositeLiteralList (removeAll l c)) (elements M)
oppositeLiteralList (removeAll l c) = removeAll (opposite l) (oppositeLiteralList c)

goal (1 subgoal):
 1. isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (getLastAssertedLiteral (oppositeLiteralList (removeAll l c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. \<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
obtain ll::Literal where "isLastAssertedLiteral ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)"
[PROOF STATE]
proof (prove)
using this:
\<exists>literal. isLastAssertedLiteral literal (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. (\<And>ll. isLastAssertedLiteral ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isLastAssertedLiteral ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
with \<open>uniq (elements M)\<close> \<open>clauseFalse c (elements M)\<close> \<open>isUIP l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
uniq (elements M)
clauseFalse c (elements M)
isUIP l c M
isLastAssertedLiteral ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
have "isBackjumpLevel (elementLevel ll M) l c M"
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
clauseFalse c (elements M)
isUIP l c M
isLastAssertedLiteral ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel ll M) l c M
[PROOF STEP]
using backjumpLevelLastLast[of "l" "c" "M" "opposite ll"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
clauseFalse c (elements M)
isUIP l c M
isLastAssertedLiteral ll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
\<lbrakk>isUIP l c M; uniq (elements M); clauseFalse c (elements M); isLastAssertedLiteral (opposite (opposite ll)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)\<rbrakk> \<Longrightarrow> isBackjumpLevel (elementLevel (opposite (opposite ll)) M) l c M

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel ll M) l c M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isBackjumpLevel (elementLevel ll M) l c M

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel (elementLevel ll M) l c M

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>level. isBackjumpLevel level l c M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>level. isBackjumpLevel level l c M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isBackjumpLevelEnsuresIsUnitInPrefix:
  fixes M :: LiteralTrail and conflictFlag :: bool and c :: Clause and l :: Literal
  assumes "consistent (elements M)" and "uniq (elements M)" and
  "clauseFalse c (elements M)" and "isBackjumpLevel level l c M"
  shows "isUnitClause c l (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
from \<open>isBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
isBackjumpLevel level l c M
[PROOF STEP]
have "isLastAssertedLiteral (opposite l) (oppositeLiteralList c)(elements M)"
    "0 \<le> level"   "level < elementLevel (opposite l) M" and
    *: "\<forall> l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> level"
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M

goal (1 subgoal):
 1. (isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M) &&& 0 \<le> level &&& level < elementLevel (opposite l) M) &&& \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> level
[PROOF STEP]
unfolding isBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M) \<and> 0 \<le> level \<and> level < elementLevel (opposite l) M \<and> (\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> level)

goal (1 subgoal):
 1. (isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M) &&& 0 \<le> level &&& level < elementLevel (opposite l) M) &&& \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> level
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
0 \<le> level
level < elementLevel (opposite l) M
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> level

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
from \<open>isLastAssertedLiteral (opposite l)(oppositeLiteralList c) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
[PROOF STEP]
have "l el c" "literalTrue (opposite l) (elements M)"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. l el c &&& literalTrue (opposite l) (elements M)
[PROOF STEP]
using isLastAssertedCharacterization [of "opposite l" "c" "elements M"]
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M) \<Longrightarrow> opposite (opposite l) el c
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M) \<Longrightarrow> literalTrue (opposite l) (elements M)

goal (1 subgoal):
 1. l el c &&& literalTrue (opposite l) (elements M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l el c
literalTrue (opposite l) (elements M)

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
have "\<not> literalFalse l (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> literalFalse l (elements (prefixToLevel level M))
[PROOF STEP]
using \<open>level < elementLevel (opposite l) M\<close> \<open>0 <= level\<close> \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
level < elementLevel (opposite l) M
0 \<le> level
uniq (elements M)

goal (1 subgoal):
 1. \<not> literalFalse l (elements (prefixToLevel level M))
[PROOF STEP]
by (simp add: literalNotInEarlierLevelsThanItsLevel)
[PROOF STATE]
proof (state)
this:
\<not> literalFalse l (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> literalFalse l (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
have "\<not> literalTrue l (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> literalTrue l (elements (prefixToLevel level M))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> literalTrue l (elements (prefixToLevel level M))
[PROOF STEP]
from \<open>consistent (elements M)\<close> \<open>literalTrue (opposite l) (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
consistent (elements M)
literalTrue (opposite l) (elements M)
[PROOF STEP]
have "\<not> literalFalse (opposite l) (elements M)"
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
literalTrue (opposite l) (elements M)

goal (1 subgoal):
 1. \<not> literalFalse (opposite l) (elements M)
[PROOF STEP]
by (auto simp add:inconsistentCharacterization)
[PROOF STATE]
proof (state)
this:
\<not> literalFalse (opposite l) (elements M)

goal (1 subgoal):
 1. \<not> literalTrue l (elements (prefixToLevel level M))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse (opposite l) (elements M)

goal (1 subgoal):
 1. \<not> literalTrue l (elements (prefixToLevel level M))
[PROOF STEP]
using isPrefixPrefixToLevel[of "level" "M"]
        prefixElementsAreTrailElements[of "prefixToLevel level M" "M"]
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse (opposite l) (elements M)
isPrefix (prefixToLevel level M) M
isPrefix (prefixToLevel level M) M \<Longrightarrow> set (elements (prefixToLevel level M)) \<subseteq> set (elements M)

goal (1 subgoal):
 1. \<not> literalTrue l (elements (prefixToLevel level M))
[PROOF STEP]
unfolding prefixToLevel_def
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse (opposite l) (elements M)
isPrefix (prefixToLevel_aux M level 0) M
isPrefix (prefixToLevel_aux M level 0) M \<Longrightarrow> set (elements (prefixToLevel_aux M level 0)) \<subseteq> set (elements M)

goal (1 subgoal):
 1. \<not> literalTrue l (elements (prefixToLevel_aux M level 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> literalTrue l (elements (prefixToLevel level M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> literalTrue l (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> literalTrue l (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
have "\<forall> l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
fix l' :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
assume "l' el c" "l' \<noteq> l"
[PROOF STATE]
proof (state)
this:
l' el c
l' \<noteq> l

goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
from \<open>l' el c\<close> \<open>clauseFalse c (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
l' el c
clauseFalse c (elements M)
[PROOF STEP]
have "literalFalse l' (elements M)"
[PROOF STATE]
proof (prove)
using this:
l' el c
clauseFalse c (elements M)

goal (1 subgoal):
 1. literalFalse l' (elements M)
[PROOF STEP]
by (simp add:clauseFalseIffAllLiteralsAreFalse)
[PROOF STATE]
proof (state)
this:
literalFalse l' (elements M)

goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
have "literalFalse l' (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
from \<open>l' el c\<close> \<open>l' \<noteq> l\<close>
[PROOF STATE]
proof (chain)
picking this:
l' el c
l' \<noteq> l
[PROOF STEP]
have "elementLevel (opposite l') M <= level"
[PROOF STATE]
proof (prove)
using this:
l' el c
l' \<noteq> l

goal (1 subgoal):
 1. elementLevel (opposite l') M \<le> level
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
l' el c
l' \<noteq> l
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> elementLevel (opposite l') M \<le> level

goal (1 subgoal):
 1. elementLevel (opposite l') M \<le> level
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elementLevel (opposite l') M \<le> level

goal (1 subgoal):
 1. literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite l') M \<le> level

goal (1 subgoal):
 1. literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
using \<open>literalFalse l' (elements M)\<close>
          \<open>0 <= level\<close>
          elementLevelLtLevelImpliesMemberPrefixToLevel[of "opposite l'" "M" "level"]
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite l') M \<le> level
literalFalse l' (elements M)
0 \<le> level
\<lbrakk>opposite l' \<in> set (elements M); elementLevel (opposite l') M \<le> level\<rbrakk> \<Longrightarrow> opposite l' \<in> set (elements (prefixToLevel level M))

goal (1 subgoal):
 1. literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literalFalse l' (elements (prefixToLevel level M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
literalFalse l' (elements (prefixToLevel level M))

goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> literalFalse ?l'2 (elements (prefixToLevel level M))

goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> literalFalse ?l'2 (elements (prefixToLevel level M))

goal (1 subgoal):
 1. \<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> literalFalse l (elements (prefixToLevel level M))
\<not> literalTrue l (elements (prefixToLevel level M))
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse l (elements (prefixToLevel level M))
\<not> literalTrue l (elements (prefixToLevel level M))
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
using \<open>l el c\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse l (elements (prefixToLevel level M))
\<not> literalTrue l (elements (prefixToLevel level M))
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
l el c

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse l (elements (prefixToLevel level M))
\<not> literalTrue l (elements (prefixToLevel level M))
\<forall>l'. l' el c \<and> l' \<noteq> l \<longrightarrow> literalFalse l' (elements (prefixToLevel level M))
l el c

goal (1 subgoal):
 1. l el c \<and> \<not> literalTrue l (elements (prefixToLevel level M)) \<and> \<not> literalFalse l (elements (prefixToLevel level M)) \<and> (\<forall>literal. literal el c \<and> literal \<noteq> l \<longrightarrow> literalFalse literal (elements (prefixToLevel level M)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isUnitClause c l (elements (prefixToLevel level M))

goal:
No subgoals!
[PROOF STEP]
qed