[STATEMENT]
lemma isMinimalBackjumpLevelCharacterization:
assumes
"isUIP l c M"
"clauseFalse c (elements M)"
"uniq (elements M)"
shows
"isMinimalBackjumpLevel level l c M =
  (isBackjumpLevel level l c M \<and>
   (\<forall> level'. level' < level \<longrightarrow> \<not> isBackjumpLevel level' l c M))" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M = (isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isMinimalBackjumpLevel level l c M \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
 2. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M) \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
assume "?lhs"
[PROOF STATE]
proof (state)
this:
isMinimalBackjumpLevel level l c M

goal (2 subgoals):
 1. isMinimalBackjumpLevel level l c M \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
 2. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M) \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
show "?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
proof (cases "set c = {l}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set c = {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
 2. set c \<noteq> {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> 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> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
 2. set c \<noteq> {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set c = {l}

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
using \<open>?lhs\<close>
[PROOF STATE]
proof (prove)
using this:
set c = {l}
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
set c = {l}
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> 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> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
with \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
isMinimalBackjumpLevel level l c M
set c \<noteq> {l}
[PROOF STEP]
obtain ll
      where "ll el c" "elementLevel (opposite ll) M = level" "isBackjumpLevel level l c M"
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
set c \<noteq> {l}

goal (1 subgoal):
 1. (\<And>ll. \<lbrakk>ll el c; elementLevel (opposite ll) M = level; isBackjumpLevel level l c M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
set c \<noteq> {l}

goal (1 subgoal):
 1. (\<And>ll. \<lbrakk>ll el c; elementLevel (opposite ll) M = level; isBackjumpLevel level l c M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ll el c
elementLevel (opposite ll) M = level
isBackjumpLevel level l c M

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
have "l \<noteq> ll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> ll
[PROOF STEP]
using \<open>isMinimalBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. l \<noteq> ll
[PROOF STEP]
using \<open>elementLevel (opposite ll) M = level\<close>
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
elementLevel (opposite ll) M = level

goal (1 subgoal):
 1. l \<noteq> ll
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
elementLevel (opposite ll) M = level

goal (1 subgoal):
 1. l \<noteq> ll
[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)) \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
elementLevel (opposite ll) M = level

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
using \<open>isBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
using \<open>elementLevel (opposite ll) M = level\<close>
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M
elementLevel (opposite ll) M = level

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
using \<open>ll el c\<close> \<open>l \<noteq> ll\<close>
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M
elementLevel (opposite ll) M = level
ll el c
l \<noteq> ll

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[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)
elementLevel (opposite ll) M = level
ll el c
l \<noteq> ll

goal (1 subgoal):
 1. (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)) \<and> (\<forall>level'<level. \<not> (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')))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

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

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M) \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M) \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
assume "?rhs"
[PROOF STATE]
proof (state)
this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

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

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

goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
using \<open>?rhs\<close>
[PROOF STATE]
proof (prove)
using this:
set c = {l}
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
using backjumpLevelZero[of "l" "c" "M"]
[PROOF STATE]
proof (prove)
using this:
set c = {l}
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
\<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. isMinimalBackjumpLevel level l c M
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
set c = {l}
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
\<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 level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
[PROOF STEP]
unfolding isBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
set c = {l}
(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)) \<and> (\<forall>level'<level. \<not> (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')))
\<lbrakk>isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M); 0 < elementLevel (opposite l) M; set c = {l}\<rbrakk> \<Longrightarrow> 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)

goal (1 subgoal):
 1. (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)) \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel 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> isMinimalBackjumpLevel level l c M
[PROOF STEP]
from \<open>?rhs\<close>
[PROOF STATE]
proof (chain)
picking this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
have "l el c"
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

goal (1 subgoal):
 1. l el c
[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)) \<and> (\<forall>level'<level. \<not> (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. l el c
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "l" "c"]
[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)) \<and> (\<forall>level'<level. \<not> (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')))
l el c = opposite l el oppositeLiteralList c

goal (1 subgoal):
 1. l el 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))) \<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)) \<and> (\<forall>level'<level. \<not> ((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))) \<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')))
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. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
let ?oll = "getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
have "clauseFalse (removeAll l c) (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clauseFalse (removeAll l c) (elements M)
[PROOF STEP]
using \<open>clauseFalse c (elements M)\<close>
[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: clauseFalseIffAllLiteralsAreFalse)
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll l c) (elements M)

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
clauseFalse (removeAll l c) (elements M)

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c 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]
{
[PROOF STATE]
proof (state)
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]
hence "set c \<subseteq> {l}"
[PROOF STATE]
proof (prove)
using this:
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]
hence False
[PROOF STATE]
proof (prove)
using this:
set c \<subseteq> {l}

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>set c \<noteq> {l}\<close>
[PROOF STATE]
proof (prove)
using this:
set c \<subseteq> {l}
set c \<noteq> {l}

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[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. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
clauseFalse (removeAll l c) (elements M)
removeAll l c \<noteq> []
[PROOF STEP]
have "isLastAssertedLiteral ?oll (removeAll (opposite l) (oppositeLiteralList 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 (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList 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 (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList 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 (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
[PROOF STEP]
using oppositeLiteralListRemove[of "l" "c"]
[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)
oppositeLiteralList (removeAll l c) = removeAll (opposite l) (oppositeLiteralList c)

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
hence  "isBackjumpLevel  (elementLevel ?oll M) l c M"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

goal (1 subgoal):
 1. isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)
isUIP l c M
clauseFalse c (elements M)
uniq (elements M)

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

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
have "?oll el (removeAll (opposite l) (oppositeLiteralList c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el removeAll (opposite l) (oppositeLiteralList c)
[PROOF STEP]
using \<open>isLastAssertedLiteral ?oll (removeAll (opposite l) (oppositeLiteralList c)) (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) (removeAll (opposite l) (oppositeLiteralList c)) (elements M)

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

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
hence "?oll el (oppositeLiteralList c)" "?oll \<noteq> opposite l"
[PROOF STATE]
proof (prove)
using this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el removeAll (opposite l) (oppositeLiteralList c)

goal (1 subgoal):
 1. getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el oppositeLiteralList c &&& getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el oppositeLiteralList c
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
hence "opposite ?oll el c"
[PROOF STATE]
proof (prove)
using this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el oppositeLiteralList c
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l

goal (1 subgoal):
 1. opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "?oll" "oppositeLiteralList c"]
[PROOF STATE]
proof (prove)
using this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el oppositeLiteralList c
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) el oppositeLiteralList c = opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el oppositeLiteralList (oppositeLiteralList c)

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
from \<open>?oll \<noteq> opposite l\<close>
[PROOF STATE]
proof (chain)
picking this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l
[PROOF STEP]
have "opposite ?oll \<noteq> l"
[PROOF STATE]
proof (prove)
using this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l

goal (1 subgoal):
 1. opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) \<noteq> l
[PROOF STEP]
using oppositeSymmetry[of "?oll" "l"]
[PROOF STATE]
proof (prove)
using this:
getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M) \<noteq> opposite l
(opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) = l) = (opposite l = getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M))

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
have "elementLevel ?oll M \<ge> level"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
assume "elementLevel ?oll M < level"
[PROOF STATE]
proof (state)
this:
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M < level

goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
hence "\<not> isBackjumpLevel  (elementLevel ?oll M) l c M"
[PROOF STATE]
proof (prove)
using this:
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M < level

goal (1 subgoal):
 1. \<not> isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M
[PROOF STEP]
using \<open>?rhs\<close>
[PROOF STATE]
proof (prove)
using this:
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M < level
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

goal (1 subgoal):
 1. \<not> isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M

goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
with \<open>isBackjumpLevel  (elementLevel ?oll M) l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M
\<not> isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M
\<not> isBackjumpLevel (elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M) l c M

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

goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M < level \<Longrightarrow> False

goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M < level \<Longrightarrow> False

goal (1 subgoal):
 1. level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
from \<open>?rhs\<close>
[PROOF STATE]
proof (chain)
picking this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
[PROOF STEP]
have "elementLevel ?oll M \<le> level"
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

goal (1 subgoal):
 1. elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M \<le> level
[PROOF STEP]
using \<open>opposite ?oll el c\<close>
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c

goal (1 subgoal):
 1. elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M \<le> level
[PROOF STEP]
using \<open>opposite ?oll \<noteq> l\<close>
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) \<noteq> l

goal (1 subgoal):
 1. elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) 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)) \<and> (\<forall>level'<level. \<not> (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')))
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) \<noteq> l

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M \<le> level
[PROOF STEP]
have "elementLevel ?oll M = level"
[PROOF STATE]
proof (prove)
using this:
level \<le> elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M \<le> level

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

goal (1 subgoal):
 1. set c \<noteq> {l} \<Longrightarrow> isMinimalBackjumpLevel level l c M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
using \<open>opposite ?oll el c\<close>
[PROOF STATE]
proof (prove)
using this:
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c

goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
using \<open>elementLevel ?oll M = level\<close>
[PROOF STATE]
proof (prove)
using this:
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M = level

goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
using \<open>?rhs\<close>
[PROOF STATE]
proof (prove)
using this:
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M = level
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)

goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
using \<open>set c \<noteq> {l}\<close>
[PROOF STATE]
proof (prove)
using this:
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M = level
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
set c \<noteq> {l}

goal (1 subgoal):
 1. isMinimalBackjumpLevel level l c M
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
opposite (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) el c
elementLevel (getLastAssertedLiteral (removeAll (opposite l) (oppositeLiteralList c)) (elements M)) M = level
isBackjumpLevel level l c M \<and> (\<forall>level'<level. \<not> isBackjumpLevel level' l c M)
set c \<noteq> {l}

goal (1 subgoal):
 1. isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
[PROOF STEP]
by (auto simp del: set_removeAll)
[PROOF STATE]
proof (state)
this:
isMinimalBackjumpLevel level l c M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
isMinimalBackjumpLevel level l c M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isMinimalBackjumpLevelEnsuresIsNotUnitBeforePrefix:
  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)" "isMinimalBackjumpLevel level l c M" and
  "level' < level"
  shows "\<not> (\<exists> l'. isUnitClause c l' (elements (prefixToLevel level' M)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
from \<open>isMinimalBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
isMinimalBackjumpLevel level l c M
[PROOF STEP]
have "isUnitClause c l (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
consistent (elements M)
uniq (elements M)
clauseFalse c (elements M)
isMinimalBackjumpLevel level l c M
level' < level

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
using isBackjumpLevelEnsuresIsUnitInPrefix[of "M" "c" "level" "l"]
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
consistent (elements M)
uniq (elements M)
clauseFalse c (elements M)
isMinimalBackjumpLevel level l c M
level' < level
\<lbrakk>consistent (elements M); uniq (elements M); clauseFalse c (elements M); isBackjumpLevel level l c M\<rbrakk> \<Longrightarrow> isUnitClause c l (elements (prefixToLevel level M))

goal (1 subgoal):
 1. isUnitClause c l (elements (prefixToLevel level M))
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
consistent (elements M)
uniq (elements M)
clauseFalse c (elements M)
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
level' < level
\<lbrakk>consistent (elements M); uniq (elements M); clauseFalse c (elements M); isBackjumpLevel level l c M\<rbrakk> \<Longrightarrow> isUnitClause c l (elements (prefixToLevel level M))

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

goal (1 subgoal):
 1. \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
hence "\<not> literalFalse l (elements (prefixToLevel level M))"
[PROOF STATE]
proof (prove)
using this:
isUnitClause c l (elements (prefixToLevel level M))

goal (1 subgoal):
 1. \<not> literalFalse l (elements (prefixToLevel level M))
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
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)))

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

goal (1 subgoal):
 1. \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
hence "\<not> literalFalse  l (elements M) \<or> elementLevel (opposite l) M > level"
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse l (elements (prefixToLevel level M))

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

goal (1 subgoal):
 1. \<not> literalFalse l (elements M) \<or> level < elementLevel (opposite l) M
[PROOF STEP]
using elementLevelLtLevelImpliesMemberPrefixToLevel[of "opposite l" "M" "level"]
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse l (elements (prefixToLevel level M))
\<lbrakk>l \<in> set (elements M); elementLevel l M \<le> level\<rbrakk> \<Longrightarrow> l \<in> set (elements (prefixToLevel level M))
\<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. \<not> literalFalse l (elements M) \<or> level < elementLevel (opposite l) M
[PROOF STEP]
by (force)+
[PROOF STATE]
proof (state)
this:
\<not> literalFalse l (elements M) \<or> level < elementLevel (opposite l) M

goal (1 subgoal):
 1. \<nexists>l'. 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]
proof (cases "\<not> literalFalse l (elements M)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> literalFalse l (elements M) \<Longrightarrow> \<not> literalFalse l (elements (prefixToLevel level' M))
 2. \<not> \<not> literalFalse l (elements M) \<Longrightarrow> \<not> literalFalse l (elements (prefixToLevel level' M))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<not> literalFalse l (elements M)

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

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

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

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

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

goal (1 subgoal):
 1. \<not> \<not> literalFalse l (elements M) \<Longrightarrow> \<not> literalFalse l (elements (prefixToLevel level' M))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> literalFalse l (elements M) \<Longrightarrow> \<not> literalFalse l (elements (prefixToLevel level' M))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<not> literalFalse l (elements M)

goal (1 subgoal):
 1. \<not> \<not> literalFalse l (elements M) \<Longrightarrow> \<not> literalFalse l (elements (prefixToLevel level' M))
[PROOF STEP]
with \<open>\<not> literalFalse l (elements M) \<or> elementLevel (opposite l) M > level\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> literalFalse l (elements M) \<or> level < elementLevel (opposite l) M
\<not> \<not> literalFalse l (elements M)
[PROOF STEP]
have "level < elementLevel (opposite l) M"
[PROOF STATE]
proof (prove)
using this:
\<not> literalFalse l (elements M) \<or> level < elementLevel (opposite l) M
\<not> \<not> literalFalse l (elements M)

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

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

goal (1 subgoal):
 1. \<not> literalFalse l (elements (prefixToLevel level' M))
[PROOF STEP]
using prefixToLevelElementsElementLevel[of "opposite l" "level'" "M"]
[PROOF STATE]
proof (prove)
using this:
level < elementLevel (opposite l) M
opposite l \<in> set (elements (prefixToLevel level' M)) \<Longrightarrow> elementLevel (opposite l) M \<le> level'

goal (1 subgoal):
 1. \<not> literalFalse l (elements (prefixToLevel level' M))
[PROOF STEP]
using \<open>level' < level\<close>
[PROOF STATE]
proof (prove)
using this:
level < elementLevel (opposite l) M
opposite l \<in> set (elements (prefixToLevel level' M)) \<Longrightarrow> elementLevel (opposite l) M \<le> level'
level' < level

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

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

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

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
from \<open>isMinimalBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
isMinimalBackjumpLevel level l c M
[PROOF STEP]
obtain ll
      where "ll el c" "elementLevel (opposite ll) M = level"
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. (\<And>ll. \<lbrakk>ll el c; elementLevel (opposite ll) M = level\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>set c \<noteq> {l}\<close>
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
set c \<noteq> {l}

goal (1 subgoal):
 1. (\<And>ll. \<lbrakk>ll el c; elementLevel (opposite ll) M = level\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
set c \<noteq> {l}

goal (1 subgoal):
 1. (\<And>ll. \<lbrakk>ll el c; elementLevel (opposite ll) M = level\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ll el c
elementLevel (opposite ll) M = level

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
hence "\<not> literalFalse ll (elements (prefixToLevel level' M))"
[PROOF STATE]
proof (prove)
using this:
ll el c
elementLevel (opposite ll) M = level

goal (1 subgoal):
 1. \<not> literalFalse ll (elements (prefixToLevel level' M))
[PROOF STEP]
using literalNotInEarlierLevelsThanItsLevel[of "level'" "opposite ll" "M"]
[PROOF STATE]
proof (prove)
using this:
ll el c
elementLevel (opposite ll) M = level
level' < elementLevel (opposite ll) M \<Longrightarrow> opposite ll \<notin> set (elements (prefixToLevel level' M))

goal (1 subgoal):
 1. \<not> literalFalse ll (elements (prefixToLevel level' M))
[PROOF STEP]
using \<open>level' < level\<close>
[PROOF STATE]
proof (prove)
using this:
ll el c
elementLevel (opposite ll) M = level
level' < elementLevel (opposite ll) M \<Longrightarrow> opposite ll \<notin> set (elements (prefixToLevel level' M))
level' < level

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

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
have "l \<noteq> ll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> ll
[PROOF STEP]
using \<open>isMinimalBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. l \<noteq> ll
[PROOF STEP]
using \<open>elementLevel (opposite ll) M = level\<close>
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
elementLevel (opposite ll) M = level

goal (1 subgoal):
 1. l \<noteq> ll
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
elementLevel (opposite ll) M = level

goal (1 subgoal):
 1. l \<noteq> ll
[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)) \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
elementLevel (opposite ll) M = level

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

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
l \<noteq> ll

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M)))

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M)))
[PROOF STEP]
obtain l'
        where "isUnitClause c l' (elements (prefixToLevel level' M))"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M)))

goal (1 subgoal):
 1. (\<And>l'. isUnitClause c l' (elements (prefixToLevel level' M)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isUnitClause c l' (elements (prefixToLevel level' M))

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "l = l'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = l' \<Longrightarrow> False
 2. l \<noteq> l' \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l = l'

goal (2 subgoals):
 1. l = l' \<Longrightarrow> False
 2. l \<noteq> l' \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = l'

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>l \<noteq> ll\<close> \<open>ll el c\<close>
[PROOF STATE]
proof (prove)
using this:
l = l'
l \<noteq> ll
ll el c

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
l = l'
l \<noteq> ll
ll el c
\<not> literalFalse ll (elements (prefixToLevel level' M))
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)))

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

goal (1 subgoal):
 1. l \<noteq> l' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> l' \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
l \<noteq> l'

goal (1 subgoal):
 1. l \<noteq> l' \<Longrightarrow> False
[PROOF STEP]
have "l el c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l el c
[PROOF STEP]
using \<open>isMinimalBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M

goal (1 subgoal):
 1. l el c
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)

goal (1 subgoal):
 1. l el c
[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)) \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)

goal (1 subgoal):
 1. l el 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))) \<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)) \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)

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 \<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))) \<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)) \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
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. l \<noteq> l' \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l el c

goal (1 subgoal):
 1. False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
l el c
l \<noteq> l'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
l el c
l \<noteq> l'
\<not> literalFalse l (elements (prefixToLevel level' M))
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)))

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

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

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))) \<Longrightarrow> False

goal (2 subgoals):
 1. set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
 2. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))) \<Longrightarrow> False

goal (1 subgoal):
 1. \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))

goal (1 subgoal):
 1. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> set c \<noteq> {l}

goal (1 subgoal):
 1. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
with \<open>isMinimalBackjumpLevel level l c M\<close>
[PROOF STATE]
proof (chain)
picking this:
isMinimalBackjumpLevel level l c M
\<not> set c \<noteq> {l}
[PROOF STEP]
have "level = 0"
[PROOF STATE]
proof (prove)
using this:
isMinimalBackjumpLevel level l c M
\<not> set c \<noteq> {l}

goal (1 subgoal):
 1. level = 0
[PROOF STEP]
unfolding isMinimalBackjumpLevel_def
[PROOF STATE]
proof (prove)
using this:
isBackjumpLevel level l c M \<and> (if set c \<noteq> {l} then \<exists>ll. ll el c \<and> elementLevel (opposite ll) M = level else level = 0)
\<not> set c \<noteq> {l}

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

goal (1 subgoal):
 1. \<not> set c \<noteq> {l} \<Longrightarrow> \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
with \<open>level' < level\<close>
[PROOF STATE]
proof (chain)
picking this:
level' < level
level = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
level' < level
level = 0

goal (1 subgoal):
 1. \<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>l'. isUnitClause c l' (elements (prefixToLevel level' M))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allDecisionsThenUIP:
  fixes M :: LiteralTrail and c:: Clause
  assumes "(uniq (elements M))" and
  "\<forall> l'. l' el c \<longrightarrow> (opposite l') el (decisions M)"
  "isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)"
  shows "isUIP l c M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isUIP l c 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" "(opposite l) el (elements M)"
    and *: "\<forall>l'. l' el (oppositeLiteralList c) \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. (l el c &&& opposite l el elements M) &&& \<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
[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. (l el c &&& opposite l el elements M) &&& \<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
[PROOF STEP]
using "literalElListIffOppositeLiteralElOppositeLiteralList"
[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))
?literal el ?literalList = opposite ?literal el oppositeLiteralList ?literalList

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
with \<open>\<forall> l'. l' el c \<longrightarrow> (opposite l') el (decisions M)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
l el c
opposite l el elements M
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
[PROOF STEP]
have "(opposite l) el (decisions M)"
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
l el c
opposite l el elements M
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
opposite l el decisions M

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
fix l' :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isUIP l c 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. isUIP l c M
[PROOF STEP]
hence "opposite l' el (oppositeLiteralList c)" and "opposite l' \<noteq> opposite l"
[PROOF STATE]
proof (prove)
using this:
l' el c
l' \<noteq> l

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

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. isUIP l c M
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
opposite l' el oppositeLiteralList c
opposite l' \<noteq> opposite l
[PROOF STEP]
have "\<not> precedes (opposite l) (opposite l') (elements M)"
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
opposite l' el oppositeLiteralList c
opposite l' \<noteq> opposite l

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

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

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
hence "(opposite l') el (elements M)"
[PROOF STATE]
proof (prove)
using this:
opposite l' el decisions M

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

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

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

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
with \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
uniq (elements M)
precedes (opposite l') (opposite l) (elements M)
[PROOF STEP]
have "elementLevel (opposite l') M <= elementLevel (opposite l) M"
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
precedes (opposite l') (opposite l) (elements M)

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

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

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

goal (1 subgoal):
 1. elementLevel (opposite l) M \<noteq> elementLevel (opposite l') M
[PROOF STEP]
using differentMarkedElementsHaveDifferentLevels[of "M" "opposite l" "opposite l'"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
opposite l el decisions M
opposite l' el decisions M
l' \<noteq> l
\<lbrakk>uniq (elements M); opposite l \<in> set (decisions M); opposite l' \<in> set (decisions M); opposite l \<noteq> opposite l'\<rbrakk> \<Longrightarrow> elementLevel (opposite l) M \<noteq> elementLevel (opposite l') M

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
elementLevel (opposite l') M \<le> elementLevel (opposite l) M
elementLevel (opposite l) M \<noteq> elementLevel (opposite l') M
[PROOF STEP]
have "elementLevel (opposite l') M < elementLevel (opposite l) M"
[PROOF STATE]
proof (prove)
using this:
elementLevel (opposite l') M \<le> elementLevel (opposite l) M
elementLevel (opposite l) M \<noteq> elementLevel (opposite l') M

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
using \<open>isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
unfolding isUIP_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. 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)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isUIP l c M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lastDecisionThenUIP:
  fixes M :: LiteralTrail and c:: Clause
  assumes "(uniq (elements M))" and
  "(opposite l) el (decisions M)"
  "clauseFalse c (elements M)"
  "isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)"
  shows "isUIP l c M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isUIP l c 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" "(opposite l) el (elements M)"
    and *: "\<forall>l'. l' el (oppositeLiteralList c) \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. (l el c &&& opposite l el elements M) &&& \<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
[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. (l el c &&& opposite l el elements M) &&& \<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
[PROOF STEP]
using "literalElListIffOppositeLiteralElOppositeLiteralList"
[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))
?literal el ?literalList = opposite ?literal el oppositeLiteralList ?literalList

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
l el c
opposite l el elements M
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
fix l' :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isUIP l c 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. isUIP l c M
[PROOF STEP]
hence "opposite l' el (oppositeLiteralList c)" and "opposite l' \<noteq> opposite l"
[PROOF STATE]
proof (prove)
using this:
l' el c
l' \<noteq> l

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

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. isUIP l c M
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
opposite l' el oppositeLiteralList c
opposite l' \<noteq> opposite l
[PROOF STEP]
have "\<not> precedes (opposite l) (opposite l') (elements M)"
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el oppositeLiteralList c \<and> l' \<noteq> opposite l \<longrightarrow> \<not> precedes (opposite l) l' (elements M)
opposite l' el oppositeLiteralList c
opposite l' \<noteq> opposite l

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
have "(opposite l') el (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opposite l' el elements M
[PROOF STEP]
using \<open>l' el c\<close> \<open>clauseFalse c (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
l' el c
clauseFalse c (elements M)

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

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

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

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
hence "elementLevel (opposite l') M < elementLevel (opposite l) M"
[PROOF STATE]
proof (prove)
using this:
precedes (opposite l') (opposite l) (elements M)

goal (1 subgoal):
 1. elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
using elementLevelPrecedesMarkedElementLt[of "M" "opposite l'" "opposite l"]
[PROOF STATE]
proof (prove)
using this:
precedes (opposite l') (opposite l) (elements M)
\<lbrakk>uniq (elements M); opposite l' \<noteq> opposite l; opposite l \<in> set (decisions M); precedes (opposite l') (opposite l) (elements M)\<rbrakk> \<Longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M

goal (1 subgoal):
 1. elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
using \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
precedes (opposite l') (opposite l) (elements M)
\<lbrakk>uniq (elements M); opposite l' \<noteq> opposite l; opposite l \<in> set (decisions M); precedes (opposite l') (opposite l) (elements M)\<rbrakk> \<Longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M
uniq (elements M)

goal (1 subgoal):
 1. elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
using \<open>opposite l el (decisions M)\<close>
[PROOF STATE]
proof (prove)
using this:
precedes (opposite l') (opposite l) (elements M)
\<lbrakk>uniq (elements M); opposite l' \<noteq> opposite l; opposite l \<in> set (decisions M); precedes (opposite l') (opposite l) (elements M)\<rbrakk> \<Longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M
uniq (elements M)
opposite l el decisions M

goal (1 subgoal):
 1. elementLevel (opposite l') M < elementLevel (opposite l) M
[PROOF STEP]
using \<open>l' \<noteq> l\<close>
[PROOF STATE]
proof (prove)
using this:
precedes (opposite l') (opposite l) (elements M)
\<lbrakk>uniq (elements M); opposite l' \<noteq> opposite l; opposite l \<in> set (decisions M); precedes (opposite l') (opposite l) (elements M)\<rbrakk> \<Longrightarrow> elementLevel (opposite l') M < elementLevel (opposite l) M
uniq (elements M)
opposite l el decisions M
l' \<noteq> l

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

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
using \<open>isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
unfolding SatSolverVerification.isUIP_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?l'2 el c; ?l'2 \<noteq> l\<rbrakk> \<Longrightarrow> elementLevel (opposite ?l'2) M < elementLevel (opposite l) M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. 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)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isUIP l c M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allDecisionsThenExistsBackjumpLevel:
  fixes M :: LiteralTrail and c:: Clause
  assumes "(uniq (elements M))" and
  "\<forall> l'. l' el c \<longrightarrow> (opposite l') el (decisions M)"
  "isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)"
  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 assms
[PROOF STATE]
proof (chain)
picking this:
uniq (elements M)
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
[PROOF STEP]
have "isUIP l c M"
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. isUIP l c M
[PROOF STEP]
using allDecisionsThenUIP
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)
\<lbrakk>uniq (elements ?M); \<forall>l'. l' el ?c \<longrightarrow> opposite l' el decisions ?M; isLastAssertedLiteral (opposite ?l) (oppositeLiteralList ?c) (elements ?M)\<rbrakk> \<Longrightarrow> isUIP ?l ?c ?M

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

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

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c 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"
[PROOF STATE]
proof (prove)
using this:
isLastAssertedLiteral (opposite l) (oppositeLiteralList c) (elements M)

goal (1 subgoal):
 1. l el 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. l el c
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList
[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))
?literal el ?literalList = opposite ?literal el oppositeLiteralList ?literalList

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

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
with \<open>\<forall> l'. l' el c \<longrightarrow> (opposite l') el (decisions M)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
l el c
[PROOF STEP]
have "(opposite l) el (decisions M)"
[PROOF STATE]
proof (prove)
using this:
\<forall>l'. l' el c \<longrightarrow> opposite l' el decisions M
l el c

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

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
hence "elementLevel (opposite l) M > 0"
[PROOF STATE]
proof (prove)
using this:
opposite l el decisions M

goal (1 subgoal):
 1. 0 < elementLevel (opposite l) M
[PROOF STEP]
using \<open>uniq (elements M)\<close>
      elementLevelMarkedGeq1[of "M" "opposite l"]
[PROOF STATE]
proof (prove)
using this:
opposite l el decisions M
uniq (elements M)
\<lbrakk>uniq (elements M); opposite l \<in> set (decisions M)\<rbrakk> \<Longrightarrow> 1 \<le> elementLevel (opposite l) M

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

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

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
have "clauseFalse c (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
fix l'::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
assume "l' el c"
[PROOF STATE]
proof (state)
this:
l' el c

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

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

goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
hence "literalFalse l' (elements M)"
[PROOF STATE]
proof (prove)
using this:
opposite l' el decisions M

goal (1 subgoal):
 1. literalFalse l' (elements M)
[PROOF STEP]
using markedElementsAreElements
[PROOF STATE]
proof (prove)
using this:
opposite l' el decisions M
?m \<in> set (markedElements ?M) \<Longrightarrow> ?m \<in> set (elements ?M)

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

goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l'2 el c \<Longrightarrow> literalFalse ?l'2 (elements M)

goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?l'2 el c \<Longrightarrow> literalFalse ?l'2 (elements M)

goal (1 subgoal):
 1. clauseFalse c (elements M)
[PROOF STEP]
using clauseFalseIffAllLiteralsAreFalse
[PROOF STATE]
proof (prove)
using this:
?l'2 el c \<Longrightarrow> literalFalse ?l'2 (elements M)
clauseFalse ?clause ?valuation = (\<forall>literal. literal el ?clause \<longrightarrow> literalFalse literal ?valuation)

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
[PROOF STATE]
proof (state)
this:
clauseFalse c (elements M)

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isUIP l c M
0 < elementLevel (opposite l) M
clauseFalse c (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isUIP l c M
0 < elementLevel (opposite l) M
clauseFalse c (elements M)

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
using \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (prove)
using this:
isUIP l c M
0 < elementLevel (opposite l) M
clauseFalse c (elements M)
uniq (elements M)

goal (1 subgoal):
 1. \<exists>level. isBackjumpLevel level l c M
[PROOF STEP]
using isUIPExistsBackjumpLevel
[PROOF STATE]
proof (prove)
using this:
isUIP l c M
0 < elementLevel (opposite l) M
clauseFalse c (elements M)
uniq (elements M)
\<lbrakk>clauseFalse ?c (elements ?M); isUIP ?l ?c ?M; uniq (elements ?M); 0 < elementLevel (opposite ?l) ?M\<rbrakk> \<Longrightarrow> \<exists>level. isBackjumpLevel level ?l ?c ?M

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma explainApplicableToEachNonDecision:
  fixes F :: Formula and M :: LiteralTrail and conflictFlag :: bool and C :: Clause and literal :: Literal
  assumes "InvariantReasonClauses F M" and "InvariantCFalse conflictFlag M C" and
  "conflictFlag = True" and "opposite literal el C" and "\<not> literal el (decisions M)"
  shows "\<exists> clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
from \<open>conflictFlag = True\<close> \<open>InvariantCFalse conflictFlag M C\<close>
[PROOF STATE]
proof (chain)
picking this:
conflictFlag = True
InvariantCFalse conflictFlag M C
[PROOF STEP]
have "clauseFalse C (elements M)"
[PROOF STATE]
proof (prove)
using this:
conflictFlag = True
InvariantCFalse conflictFlag M C

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

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. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
with \<open>opposite literal el C\<close>
[PROOF STATE]
proof (chain)
picking this:
opposite literal el C
clauseFalse C (elements M)
[PROOF STEP]
have "literalTrue literal (elements M)"
[PROOF STATE]
proof (prove)
using this:
opposite literal el C
clauseFalse C (elements M)

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

goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
with \<open>\<not> literal el (decisions M)\<close> \<open>InvariantReasonClauses F M\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> literal el decisions M
InvariantReasonClauses F M
literalTrue literal (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> literal el decisions M
InvariantReasonClauses F M
literalTrue literal (elements M)

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

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:
No subgoals!
[PROOF STEP]
qed