[STATEMENT]
lemma InvariantConsistentAfterUnitPropagate:
  fixes M :: LiteralTrail and F :: Formula and M' :: LiteralTrail and uClause :: Clause and uLiteral :: Literal
  assumes "InvariantConsistent M" and
  "isUnitClause uClause uLiteral (elements M)" and
  "M' = M @ [(uLiteral, False)]"
  shows "InvariantConsistent M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
from \<open>InvariantConsistent M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
[PROOF STEP]
have "consistent (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M

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

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
from \<open>isUnitClause uClause uLiteral (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isUnitClause uClause uLiteral (elements M)
[PROOF STEP]
have "\<not> literalFalse uLiteral (elements M)"
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause uLiteral (elements M)

goal (1 subgoal):
 1. \<not> literalFalse uLiteral (elements M)
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
uLiteral el uClause \<and> \<not> literalTrue uLiteral (elements M) \<and> \<not> literalFalse uLiteral (elements M) \<and> (\<forall>literal. literal el uClause \<and> literal \<noteq> uLiteral \<longrightarrow> literalFalse literal (elements M))

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> literalFalse uLiteral (elements M)

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
assume "inconsistent (elements M')"
[PROOF STATE]
proof (state)
this:
inconsistent (elements M')

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with \<open>M' = M @ [(uLiteral, False)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(uLiteral, False)]
inconsistent (elements M')
[PROOF STEP]
have "inconsistent (elements M) \<or> inconsistent [unitLiteral] \<or> (\<exists> l. literalTrue l (elements M) \<and> literalFalse l [uLiteral])"
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(uLiteral, False)]
inconsistent (elements M')

goal (1 subgoal):
 1. inconsistent (elements M) \<or> inconsistent [unitLiteral] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [uLiteral])
[PROOF STEP]
using inconsistentAppend [of "elements M" "[uLiteral]"]
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(uLiteral, False)]
inconsistent (elements M')
inconsistent (elements M @ [uLiteral]) \<Longrightarrow> inconsistent (elements M) \<or> inconsistent [uLiteral] \<or> (\<exists>literal. literalTrue literal (elements M) \<and> literalFalse literal [uLiteral])

goal (1 subgoal):
 1. inconsistent (elements M) \<or> inconsistent [unitLiteral] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [uLiteral])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inconsistent (elements M) \<or> inconsistent [unitLiteral] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [uLiteral])

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with \<open>consistent (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
consistent (elements M)
inconsistent (elements M) \<or> inconsistent [unitLiteral] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [uLiteral])
[PROOF STEP]
obtain literal::Literal
      where "literalTrue literal (elements M)" and "literalFalse literal [uLiteral]"
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
inconsistent (elements M) \<or> inconsistent [unitLiteral] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [uLiteral])

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
hence "literal = opposite uLiteral"
[PROOF STATE]
proof (prove)
using this:
literalTrue literal (elements M)
literalFalse literal [uLiteral]

goal (1 subgoal):
 1. literal = opposite uLiteral
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literal = opposite uLiteral

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with \<open>literalTrue literal (elements M)\<close> \<open>\<not> literalFalse uLiteral (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
literalTrue literal (elements M)
\<not> literalFalse uLiteral (elements M)
literal = opposite uLiteral
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
literalTrue literal (elements M)
\<not> literalFalse uLiteral (elements M)
literal = opposite uLiteral

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inconsistent (elements M') \<Longrightarrow> False

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inconsistent (elements M') \<Longrightarrow> False

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
inconsistent (elements M') \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantUniqAfterUnitPropagate:
  fixes M :: LiteralTrail and F :: Formula and M' :: LiteralTrail and uClause :: Clause and uLiteral :: Literal
  assumes "InvariantUniq M" and
  "isUnitClause uClause uLiteral (elements M)" and
  "M' = M @ [(uLiteral, False)]"
  shows "InvariantUniq M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
from \<open>InvariantUniq M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantUniq M
[PROOF STEP]
have "uniq (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M

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

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uniq (elements M)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
from \<open>isUnitClause uClause uLiteral (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isUnitClause uClause uLiteral (elements M)
[PROOF STEP]
have "\<not> literalTrue uLiteral (elements M)"
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause uLiteral (elements M)

goal (1 subgoal):
 1. \<not> literalTrue uLiteral (elements M)
[PROOF STEP]
unfolding isUnitClause_def
[PROOF STATE]
proof (prove)
using this:
uLiteral el uClause \<and> \<not> literalTrue uLiteral (elements M) \<and> \<not> literalFalse uLiteral (elements M) \<and> (\<forall>literal. literal el uClause \<and> literal \<noteq> uLiteral \<longrightarrow> literalFalse literal (elements M))

goal (1 subgoal):
 1. \<not> literalTrue uLiteral (elements M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> literalTrue uLiteral (elements M)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uniq (elements M)
\<not> literalTrue uLiteral (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
\<not> literalTrue uLiteral (elements M)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
using \<open>M' = M @ [(uLiteral, False)]\<close> uniqAppendElement[of "elements M" "uLiteral"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
\<not> literalTrue uLiteral (elements M)
M' = M @ [(uLiteral, False)]
uniq (elements M) \<Longrightarrow> (uLiteral \<notin> set (elements M)) = uniq (elements M @ [uLiteral])

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
\<not> literalTrue uLiteral (elements M)
M' = M @ [(uLiteral, False)]
uniq (elements M) \<Longrightarrow> (uLiteral \<notin> set (elements M)) = uniq (elements M @ [uLiteral])

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantReasonClausesAfterUnitPropagate:
  fixes M :: LiteralTrail and F :: Formula and M' :: LiteralTrail and uClause :: Clause and uLiteral :: Literal
  assumes "InvariantReasonClauses F M" and
  "formulaEntailsClause F uClause" and "isUnitClause uClause uLiteral (elements M)" and
  "M' = M @ [(uLiteral, False)]"
  shows "InvariantReasonClauses F M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
from \<open>InvariantReasonClauses F M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantReasonClauses F M
[PROOF STEP]
have *: "(\<forall> literal. (literal el (elements M)) \<and> \<not> (literal el (decisions M)) \<longrightarrow>
    (\<exists> clause. formulaEntailsClause F clause \<and> (isReason clause literal (elements M))))"
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M

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

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

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

goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
fix literal::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
assume "literal el elements M'" "\<not> literal el decisions M'"
[PROOF STATE]
proof (state)
this:
literal el elements M'
\<not> literal el decisions M'

goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
have "\<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 (cases "literal el elements M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
 2. \<not> literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
literal el elements M

goal (2 subgoals):
 1. literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
 2. \<not> literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
with assms \<open>\<not> literal el decisions M'\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantReasonClauses F M
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
M' = M @ [(uLiteral, False)]
\<not> literal el decisions M'
literal el elements M
[PROOF STEP]
obtain clause::Clause
        where "formulaEntailsClause F clause \<and> isReason clause literal (elements M')"
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
M' = M @ [(uLiteral, False)]
\<not> literal el decisions M'
literal el elements M

goal (1 subgoal):
 1. (\<And>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using InvariantReasonClausesHoldsForPrefixElements [of "F" "M" "M'" "literal"]
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
M' = M @ [(uLiteral, False)]
\<not> literal el decisions M'
literal el elements M
\<lbrakk>InvariantReasonClauses F M; isPrefix M M'; literal el elements M; \<not> literal el decisions M'\<rbrakk> \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')

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

goal (2 subgoals):
 1. literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
 2. \<not> literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F clause \<and> isReason clause 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 (1 subgoal):
 1. \<not> literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> literal el elements M

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

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

goal (1 subgoal):
 1. \<not> literal el elements M \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
with \<open>M' = M @ [(uLiteral, False)]\<close> \<open>isUnitClause uClause uLiteral (elements M)\<close> \<open>formulaEntailsClause F uClause\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(uLiteral, False)]
isUnitClause uClause uLiteral (elements M)
formulaEntailsClause F uClause
literal = uLiteral
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(uLiteral, False)]
isUnitClause uClause uLiteral (elements M)
formulaEntailsClause F uClause
literal = uLiteral

goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')
[PROOF STEP]
using isUnitClauseIsReason [of "uClause" "uLiteral" "elements M"]
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(uLiteral, False)]
isUnitClause uClause uLiteral (elements M)
formulaEntailsClause F uClause
literal = uLiteral
\<lbrakk>isUnitClause uClause uLiteral (elements M); uLiteral el ?valuation'\<rbrakk> \<Longrightarrow> isReason uClause uLiteral (elements M @ ?valuation')

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
[PROOF STATE]
proof (state)
this:
\<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M')

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantCFalseAfterUnitPropagate:
  fixes M :: LiteralTrail and F :: Formula and M' :: LiteralTrail and uClause :: Clause and uLiteral :: Literal
  assumes "InvariantCFalse conflictFlag M C" and
  "M' = M @ [(uLiteral, False)]"
  shows "InvariantCFalse conflictFlag M' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCFalse conflictFlag M' C
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantCFalse conflictFlag M' C
[PROOF STEP]
from \<open>InvariantCFalse conflictFlag M C\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantCFalse conflictFlag M C
[PROOF STEP]
have *: "conflictFlag \<longrightarrow> clauseFalse C (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantCFalse conflictFlag M C

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

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

goal (1 subgoal):
 1. InvariantCFalse conflictFlag M' C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
conflictFlag \<longrightarrow> clauseFalse C (elements M)

goal (1 subgoal):
 1. InvariantCFalse conflictFlag M' C
[PROOF STEP]
assume "conflictFlag"
[PROOF STATE]
proof (state)
this:
conflictFlag

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

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

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

goal (1 subgoal):
 1. InvariantCFalse conflictFlag M' C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
conflictFlag \<Longrightarrow> clauseFalse C (elements M')

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

goal (1 subgoal):
 1. conflictFlag \<longrightarrow> clauseFalse C (elements M')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InvariantCFalse conflictFlag M' C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAfterBacktrack:
  fixes F::Formula and M::LiteralTrail
  assumes "InvariantImpliedLiterals F M" and "InvariantUniq M" and "InvariantConsistent M" and
  "decisions M \<noteq> []" and "formulaFalse F (elements M)"
  "M' = (prefixBeforeLastDecision M) @ [(opposite (lastDecision M), False)]"
  shows "InvariantImpliedLiterals F M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
have "isPrefix (prefixBeforeLastDecision M) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPrefix (prefixBeforeLastDecision M) M
[PROOF STEP]
by (simp add: isPrefixPrefixBeforeLastMarked)
[PROOF STATE]
proof (state)
this:
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
fix l'::Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
assume "l' el (elements M')"
[PROOF STATE]
proof (state)
this:
l' el elements M'

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
let ?p = "(prefixBeforeLastDecision M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
let ?l = "lastDecision M"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
proof (cases "l' el (elements ?p)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
 2. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l' el elements (prefixBeforeLastDecision M)

goal (2 subgoals):
 1. l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
 2. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>isPrefix ?p M\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix (prefixBeforeLastDecision M) M
l' el elements (prefixBeforeLastDecision M)
[PROOF STEP]
have "l' el (elements M)"
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M
l' el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. l' el elements M
[PROOF STEP]
using prefixElementsAreTrailElements[of "?p" "M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M
l' el elements (prefixBeforeLastDecision M)
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> set (elements (prefixBeforeLastDecision M)) \<subseteq> set (elements M)

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

goal (2 subgoals):
 1. l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
 2. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>InvariantImpliedLiterals F M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
l' el elements M
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisionsTo l' M)) l'"
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
l' el elements M

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

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l' M)) l'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M)) l'

goal (2 subgoals):
 1. l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
 2. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M)) l'

goal (2 subgoals):
 1. l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
 2. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>M' = ?p @ [(opposite ?l, False)]\<close> True \<open>isPrefix ?p M\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
l' el elements (prefixBeforeLastDecision M)
isPrefix (prefixBeforeLastDecision M) M
[PROOF STEP]
have "(decisionsTo l' M') = (decisionsTo l' M)"
[PROOF STATE]
proof (prove)
using this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
l' el elements (prefixBeforeLastDecision M)
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. decisionsTo l' M' = decisionsTo l' M
[PROOF STEP]
using prefixToElementToPrefixElement[of "?p" "M" "l'"]
[PROOF STATE]
proof (prove)
using this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
l' el elements (prefixBeforeLastDecision M)
isPrefix (prefixBeforeLastDecision M) M
\<lbrakk>isPrefix (prefixBeforeLastDecision M) M; l' \<in> set (elements (prefixBeforeLastDecision M))\<rbrakk> \<Longrightarrow> prefixToElement l' M = prefixToElement l' (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. decisionsTo l' M' = decisionsTo l' M
[PROOF STEP]
unfolding markedElementsTo_def
[PROOF STATE]
proof (prove)
using this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
l' el elements (prefixBeforeLastDecision M)
isPrefix (prefixBeforeLastDecision M) M
\<lbrakk>isPrefix (prefixBeforeLastDecision M) M; l' \<in> set (elements (prefixBeforeLastDecision M))\<rbrakk> \<Longrightarrow> prefixToElement l' M = prefixToElement l' (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. decisions (prefixToElement l' M') = decisions (prefixToElement l' M)
[PROOF STEP]
by (auto simp add: prefixToElementAppend)
[PROOF STATE]
proof (state)
this:
decisionsTo l' M' = decisionsTo l' M

goal (2 subgoals):
 1. l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
 2. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M)) l'
decisionsTo l' M' = decisionsTo l' M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M)) l'
decisionsTo l' M' = decisionsTo l' M

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> l' el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>l' el (elements M')\<close> and \<open>M' = ?p @ [(opposite ?l, False)]\<close>
[PROOF STATE]
proof (chain)
picking this:
l' el elements M'
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
\<not> l' el elements (prefixBeforeLastDecision M)
[PROOF STEP]
have "?l = (opposite l')"
[PROOF STATE]
proof (prove)
using this:
l' el elements M'
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
\<not> l' el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. lastDecision M = opposite l'
[PROOF STEP]
by (auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
lastDecision M = opposite l'

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
hence "l' = (opposite ?l)"
[PROOF STATE]
proof (prove)
using this:
lastDecision M = opposite l'

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

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>InvariantUniq M\<close> and \<open>markedElements M \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantUniq M
decisions M \<noteq> []
[PROOF STEP]
have "(decisionsTo ?l M) = (decisions M)"
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M
decisions M \<noteq> []

goal (1 subgoal):
 1. decisionsTo (lastDecision M) M = decisions M
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
decisions M \<noteq> []

goal (1 subgoal):
 1. decisionsTo (lastDecision M) M = decisions M
[PROOF STEP]
using markedElementsToLastMarkedAreAllMarkedElements
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
decisions M \<noteq> []
\<lbrakk>uniq (elements ?M); markedElements ?M \<noteq> []\<rbrakk> \<Longrightarrow> markedElementsTo (lastMarked ?M) ?M = markedElements ?M

goal (1 subgoal):
 1. decisionsTo (lastDecision M) M = decisions M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
decisionsTo (lastDecision M) M = decisions M

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
decisionsTo (lastDecision M) M = decisions M

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>decisions M \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
decisions M \<noteq> []
[PROOF STEP]
have "?l el (elements M)"
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []

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

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>InvariantConsistent M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
lastDecision M el elements M
[PROOF STEP]
have "\<not> (opposite ?l) el (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M
lastDecision M el elements M

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements M
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
lastDecision M el elements M

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

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>isPrefix ?p M\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix (prefixBeforeLastDecision M) M
\<not> opposite (lastDecision M) el elements M
[PROOF STEP]
have "\<not> (opposite ?l) el (elements ?p)"
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M
\<not> opposite (lastDecision M) el elements M

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
using prefixElementsAreTrailElements[of "?p" "M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M
\<not> opposite (lastDecision M) el elements M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> set (elements (prefixBeforeLastDecision M)) \<subseteq> set (elements M)

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>M' = ?p @ [(opposite ?l, False)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
have "decisionsTo (opposite ?l) M' = decisions ?p"
[PROOF STATE]
proof (prove)
using this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)
[PROOF STEP]
using markedElementsToAppend [of "opposite ?l" "?p" "[(opposite ?l, False)]"]
[PROOF STATE]
proof (prove)
using this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
decisionsTo (opposite (lastDecision M)) (prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]) = (if opposite (lastDecision M) \<in> set (elements (prefixBeforeLastDecision M)) then decisionsTo (opposite (lastDecision M)) (prefixBeforeLastDecision M) else decisions (prefixBeforeLastDecision M) @ decisionsTo (opposite (lastDecision M)) [(opposite (lastDecision M), False)])

goal (1 subgoal):
 1. decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)
[PROOF STEP]
unfolding markedElementsTo_def
[PROOF STATE]
proof (prove)
using this:
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
decisions (prefixToElement (opposite (lastDecision M)) (prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)])) = (if opposite (lastDecision M) \<in> set (elements (prefixBeforeLastDecision M)) then decisions (prefixToElement (opposite (lastDecision M)) (prefixBeforeLastDecision M)) else decisions (prefixBeforeLastDecision M) @ decisions (prefixToElement (opposite (lastDecision M)) [(opposite (lastDecision M), False)]))

goal (1 subgoal):
 1. decisions (prefixToElement (opposite (lastDecision M)) M') = decisions (prefixBeforeLastDecision M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>InvariantUniq M\<close> \<open>decisions M \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantUniq M
decisions M \<noteq> []
[PROOF STEP]
have "\<not> ?l el (elements ?p)"
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M
decisions M \<noteq> []

goal (1 subgoal):
 1. \<not> lastDecision M el elements (prefixBeforeLastDecision M)
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
decisions M \<noteq> []

goal (1 subgoal):
 1. \<not> lastDecision M el elements (prefixBeforeLastDecision M)
[PROOF STEP]
using lastMarkedNotInPrefixBeforeLastMarked[of "M"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
decisions M \<noteq> []
\<lbrakk>uniq (elements M); decisions M \<noteq> []\<rbrakk> \<Longrightarrow> lastDecision M \<notin> set (elements (prefixBeforeLastDecision M))

goal (1 subgoal):
 1. \<not> lastDecision M el elements (prefixBeforeLastDecision M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
hence "\<not> ?l el (decisions ?p)"
[PROOF STATE]
proof (prove)
using this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> lastDecision M el decisions (prefixBeforeLastDecision M)
[PROOF STEP]
by (auto simp add: markedElementsAreElements)
[PROOF STATE]
proof (state)
this:
\<not> lastDecision M el decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
hence "(removeAll ?l (decisions ?p)) = (decisions ?p)"
[PROOF STATE]
proof (prove)
using this:
\<not> lastDecision M el decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M)) = decisions (prefixBeforeLastDecision M)
[PROOF STEP]
by (simp add: removeAll_id)
[PROOF STATE]
proof (state)
this:
removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M)) = decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
hence "(removeAll ?l ((decisions ?p) @ [?l])) = (decisions ?p)"
[PROOF STATE]
proof (prove)
using this:
removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M)) = decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M) @ [lastDecision M]) = decisions (prefixBeforeLastDecision M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M) @ [lastDecision M]) = decisions (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>decisions M \<noteq> []\<close> False \<open>l' = (opposite ?l)\<close>
[PROOF STATE]
proof (chain)
picking this:
decisions M \<noteq> []
\<not> l' el elements (prefixBeforeLastDecision M)
l' = opposite (lastDecision M)
[PROOF STEP]
have "(decisions ?p) @ [?l] = (decisions M)"
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
\<not> l' el elements (prefixBeforeLastDecision M)
l' = opposite (lastDecision M)

goal (1 subgoal):
 1. decisions (prefixBeforeLastDecision M) @ [lastDecision M] = decisions M
[PROOF STEP]
using markedElementsAreElementsBeforeLastDecisionAndLastDecision[of "M"]
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
\<not> l' el elements (prefixBeforeLastDecision M)
l' = opposite (lastDecision M)
decisions M \<noteq> [] \<Longrightarrow> decisions M = decisions (prefixBeforeLastDecision M) @ [lastDecision M]

goal (1 subgoal):
 1. decisions (prefixBeforeLastDecision M) @ [lastDecision M] = decisions M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
decisions (prefixBeforeLastDecision M) @ [lastDecision M] = decisions M

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>(removeAll ?l ((decisions ?p) @ [?l])) = (decisions ?p)\<close>
[PROOF STATE]
proof (chain)
picking this:
removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M) @ [lastDecision M]) = decisions (prefixBeforeLastDecision M)
decisions (prefixBeforeLastDecision M) @ [lastDecision M] = decisions M
[PROOF STEP]
have "(decisions ?p) = (removeAll ?l (decisions M))"
[PROOF STATE]
proof (prove)
using this:
removeAll (lastDecision M) (decisions (prefixBeforeLastDecision M) @ [lastDecision M]) = decisions (prefixBeforeLastDecision M)
decisions (prefixBeforeLastDecision M) @ [lastDecision M] = decisions M

goal (1 subgoal):
 1. decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>formulaFalse F (elements M)\<close> \<open>InvariantImpliedLiterals F M\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaFalse F (elements M)
InvariantImpliedLiterals F M
[PROOF STEP]
have "\<not> satisfiable (F @ (val2form (decisions M)))"
[PROOF STATE]
proof (prove)
using this:
formulaFalse F (elements M)
InvariantImpliedLiterals F M

goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
using InvariantImpliedLiteralsAndFormulaFalseThenFormulaAndDecisionsAreNotSatisfiable[of "F" "M"]
[PROOF STATE]
proof (prove)
using this:
formulaFalse F (elements M)
InvariantImpliedLiterals F M
\<lbrakk>InvariantImpliedLiterals F M; formulaFalse F (elements M)\<rbrakk> \<Longrightarrow> \<not> satisfiable (F @ val2form (decisions M))

goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> satisfiable (F @ val2form (decisions M))

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
from \<open>decisions M \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
decisions M \<noteq> []
[PROOF STEP]
have "?l el (decisions M)"
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []

goal (1 subgoal):
 1. lastDecision M el decisions M
[PROOF STEP]
unfolding lastMarked_def
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []

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

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
hence "[?l] el val2form (decisions M)"
[PROOF STATE]
proof (prove)
using this:
lastDecision M el decisions M

goal (1 subgoal):
 1. [lastDecision M] el val2form (decisions M)
[PROOF STEP]
using val2FormEl[of "?l" "(decisions M)"]
[PROOF STATE]
proof (prove)
using this:
lastDecision M el decisions M
lastDecision M el decisions M = [lastDecision M] el val2form (decisions M)

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

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
with \<open>\<not> satisfiable (F @ (val2form (decisions M)))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> satisfiable (F @ val2form (decisions M))
[lastDecision M] el val2form (decisions M)
[PROOF STEP]
have "formulaEntailsLiteral (removeAll [?l] (F @ val2form (decisions M))) (opposite ?l)"
[PROOF STATE]
proof (prove)
using this:
\<not> satisfiable (F @ val2form (decisions M))
[lastDecision M] el val2form (decisions M)

goal (1 subgoal):
 1. formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))
[PROOF STEP]
using unsatisfiableFormulaWithSingleLiteralClause[of "F @ val2form (decisions M)" "lastDecision M"]
[PROOF STATE]
proof (prove)
using this:
\<not> satisfiable (F @ val2form (decisions M))
[lastDecision M] el val2form (decisions M)
\<lbrakk>\<not> satisfiable (F @ val2form (decisions M)); [lastDecision M] el F @ val2form (decisions M)\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))

goal (1 subgoal):
 1. formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))

goal (1 subgoal):
 1. \<not> l' el elements (prefixBeforeLastDecision M) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
decisionsTo (lastDecision M) M = decisions M
decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)
decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)
formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
decisionsTo (lastDecision M) M = decisions M
decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)
decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)
formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
using \<open>l' = (opposite ?l)\<close>
[PROOF STATE]
proof (prove)
using this:
decisionsTo (lastDecision M) M = decisions M
decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)
decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)
formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))
l' = opposite (lastDecision M)

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
using formulaEntailsLiteralRemoveAllAppend[of "[?l]" "F" "val2form (removeAll ?l (decisions M))" "opposite ?l"]
[PROOF STATE]
proof (prove)
using this:
decisionsTo (lastDecision M) M = decisions M
decisionsTo (opposite (lastDecision M)) M' = decisions (prefixBeforeLastDecision M)
decisions (prefixBeforeLastDecision M) = removeAll (lastDecision M) (decisions M)
formulaEntailsLiteral (removeAll [lastDecision M] (F @ val2form (decisions M))) (opposite (lastDecision M))
l' = opposite (lastDecision M)
formulaEntailsLiteral (removeAll [lastDecision M] F @ val2form (removeAll (lastDecision M) (decisions M))) (opposite (lastDecision M)) \<Longrightarrow> formulaEntailsLiteral (F @ val2form (removeAll (lastDecision M) (decisions M))) (opposite (lastDecision M))

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'
[PROOF STEP]
by (auto simp add: val2FormRemoveAll)
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l' M')) l'

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l'2 el elements M' \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo ?l'2 M')) ?l'2

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?l'2 el elements M' \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo ?l'2 M')) ?l'2

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
unfolding InvariantImpliedLiterals_def
[PROOF STATE]
proof (prove)
using this:
?l'2 el elements M' \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo ?l'2 M')) ?l'2

goal (1 subgoal):
 1. \<forall>l. l el elements M' \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
InvariantImpliedLiterals F M'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantConsistentAfterBacktrack:
  fixes F::Formula and M::LiteralTrail
  assumes "InvariantUniq M" and "InvariantConsistent M" and
  "decisions M \<noteq> []" and
  "M' = (prefixBeforeLastDecision M) @ [(opposite (lastDecision M), False)]"
  shows "InvariantConsistent M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
from \<open>decisions M \<noteq> []\<close> \<open>InvariantUniq M\<close>
[PROOF STATE]
proof (chain)
picking this:
decisions M \<noteq> []
InvariantUniq M
[PROOF STEP]
have "\<not> lastDecision M el elements (prefixBeforeLastDecision M)"
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
InvariantUniq M

goal (1 subgoal):
 1. \<not> lastDecision M el elements (prefixBeforeLastDecision M)
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
uniq (elements M)

goal (1 subgoal):
 1. \<not> lastDecision M el elements (prefixBeforeLastDecision M)
[PROOF STEP]
using lastMarkedNotInPrefixBeforeLastMarked
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
uniq (elements M)
\<lbrakk>uniq (elements ?M); markedElements ?M \<noteq> []\<rbrakk> \<Longrightarrow> lastMarked ?M \<notin> set (elements (prefixBeforeLastMarked ?M))

goal (1 subgoal):
 1. \<not> lastDecision M el elements (prefixBeforeLastDecision M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
from \<open>InvariantConsistent M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
[PROOF STEP]
have "consistent (elements (prefixBeforeLastDecision M))"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M

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

goal (1 subgoal):
 1. consistent (elements (prefixBeforeLastDecision M))
[PROOF STEP]
using isPrefixPrefixBeforeLastMarked[of "M"]
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. consistent (elements (prefixBeforeLastDecision M))
[PROOF STEP]
using isPrefixElements[of "prefixBeforeLastDecision M" "M"]
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)

goal (1 subgoal):
 1. consistent (elements (prefixBeforeLastDecision M))
[PROOF STEP]
using consistentPrefix[of "elements (prefixBeforeLastDecision M)" "elements M"]
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)
\<lbrakk>isPrefix (elements (prefixBeforeLastDecision M)) (elements M); consistent (elements M)\<rbrakk> \<Longrightarrow> consistent (elements (prefixBeforeLastDecision M))

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)
consistent (elements (prefixBeforeLastDecision M))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)
consistent (elements (prefixBeforeLastDecision M))

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)
consistent (elements (prefixBeforeLastDecision M))

goal (1 subgoal):
 1. consistent (elements M')
[PROOF STEP]
using \<open>M' = (prefixBeforeLastDecision M) @ [(opposite (lastDecision M), False)]\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)
consistent (elements (prefixBeforeLastDecision M))
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]

goal (1 subgoal):
 1. consistent (elements M')
[PROOF STEP]
using inconsistentAppend[of "elements (prefixBeforeLastDecision M)" "[opposite (lastDecision M)]"]
[PROOF STATE]
proof (prove)
using this:
\<not> lastDecision M el elements (prefixBeforeLastDecision M)
consistent (elements (prefixBeforeLastDecision M))
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
inconsistent (elements (prefixBeforeLastDecision M) @ [opposite (lastDecision M)]) \<Longrightarrow> inconsistent (elements (prefixBeforeLastDecision M)) \<or> inconsistent [opposite (lastDecision M)] \<or> (\<exists>literal. literalTrue literal (elements (prefixBeforeLastDecision M)) \<and> literalFalse literal [opposite (lastDecision M)])

goal (1 subgoal):
 1. consistent (elements M')
[PROOF STEP]
by (auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
InvariantConsistent M'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantUniqAfterBacktrack:
  fixes F::Formula and M::LiteralTrail
  assumes "InvariantUniq M" and "InvariantConsistent M" and
  "decisions M \<noteq> []" and
  "M' = (prefixBeforeLastDecision M) @ [(opposite (lastDecision M), False)]"
  shows "InvariantUniq M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
from \<open>InvariantUniq M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantUniq M
[PROOF STEP]
have "uniq (elements (prefixBeforeLastDecision M))"
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M

goal (1 subgoal):
 1. uniq (elements (prefixBeforeLastDecision M))
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)

goal (1 subgoal):
 1. uniq (elements (prefixBeforeLastDecision M))
[PROOF STEP]
using isPrefixPrefixBeforeLastMarked[of "M"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. uniq (elements (prefixBeforeLastDecision M))
[PROOF STEP]
using isPrefixElements[of "prefixBeforeLastDecision M" "M"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)

goal (1 subgoal):
 1. uniq (elements (prefixBeforeLastDecision M))
[PROOF STEP]
using uniqListImpliesUniqPrefix
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)
\<lbrakk>isPrefix ?p ?l; uniq ?l\<rbrakk> \<Longrightarrow> uniq ?p

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uniq (elements (prefixBeforeLastDecision M))

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

goal (1 subgoal):
 1. lastDecision M el elements M
[PROOF STEP]
using lastMarkedIsMarkedElement[of "M"]
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
decisions M \<noteq> [] \<Longrightarrow> lastDecision M \<in> set (decisions M)

goal (1 subgoal):
 1. lastDecision M el elements M
[PROOF STEP]
using markedElementsAreElements[of "lastDecision M" "M"]
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
decisions M \<noteq> [] \<Longrightarrow> lastDecision M \<in> set (decisions M)
lastDecision M \<in> set (decisions M) \<Longrightarrow> lastDecision M \<in> set (elements M)

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
with \<open>InvariantConsistent M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
lastDecision M el elements M
[PROOF STEP]
have "\<not> opposite (lastDecision M) el (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M
lastDecision M el elements M

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements M
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
lastDecision M el elements M

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements M
[PROOF STEP]
using inconsistentCharacterization
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
lastDecision M el elements M
inconsistent ?valuation = (\<exists>literal. literalTrue literal ?valuation \<and> literalFalse literal ?valuation)

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
hence "\<not> opposite (lastDecision M) el (elements (prefixBeforeLastDecision M))"
[PROOF STATE]
proof (prove)
using this:
\<not> opposite (lastDecision M) el elements M

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
using isPrefixPrefixBeforeLastMarked[of "M"]
[PROOF STATE]
proof (prove)
using this:
\<not> opposite (lastDecision M) el elements M
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
using isPrefixElements[of "prefixBeforeLastDecision M" "M"]
[PROOF STATE]
proof (prove)
using this:
\<not> opposite (lastDecision M) el elements M
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
using prefixIsSubset[of "elements (prefixBeforeLastDecision M)" "elements M"]
[PROOF STATE]
proof (prove)
using this:
\<not> opposite (lastDecision M) el elements M
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)
isPrefix (elements (prefixBeforeLastDecision M)) (elements M) \<Longrightarrow> set (elements (prefixBeforeLastDecision M)) \<subseteq> set (elements M)

goal (1 subgoal):
 1. \<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uniq (elements (prefixBeforeLastDecision M))
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uniq (elements (prefixBeforeLastDecision M))
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
using
      \<open>M' = (prefixBeforeLastDecision M) @ [(opposite (lastDecision M), False)]\<close>
      uniqAppendElement[of "elements (prefixBeforeLastDecision M)" "opposite (lastDecision M)"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements (prefixBeforeLastDecision M))
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
uniq (elements (prefixBeforeLastDecision M)) \<Longrightarrow> (opposite (lastDecision M) \<notin> set (elements (prefixBeforeLastDecision M))) = uniq (elements (prefixBeforeLastDecision M) @ [opposite (lastDecision M)])

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
uniq (elements (prefixBeforeLastDecision M))
\<not> opposite (lastDecision M) el elements (prefixBeforeLastDecision M)
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
uniq (elements (prefixBeforeLastDecision M)) \<Longrightarrow> (opposite (lastDecision M) \<notin> set (elements (prefixBeforeLastDecision M))) = uniq (elements (prefixBeforeLastDecision M) @ [opposite (lastDecision M)])

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantVarsMAfterBacktrack:
  fixes F::Formula and M::LiteralTrail
  assumes "InvariantVarsM M F0 Vbl"
  "decisions M \<noteq> []" and
  "M' = (prefixBeforeLastDecision M) @ [(opposite (lastDecision M), False)]"
  shows "InvariantVarsM M' F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
from \<open>decisions M \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
decisions M \<noteq> []
[PROOF STEP]
have "lastDecision M el (elements M)"
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []

goal (1 subgoal):
 1. lastDecision M el elements M
[PROOF STEP]
using lastMarkedIsMarkedElement[of "M"]
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
decisions M \<noteq> [] \<Longrightarrow> lastDecision M \<in> set (decisions M)

goal (1 subgoal):
 1. lastDecision M el elements M
[PROOF STEP]
using markedElementsAreElements[of "lastDecision M" "M"]
[PROOF STATE]
proof (prove)
using this:
decisions M \<noteq> []
decisions M \<noteq> [] \<Longrightarrow> lastDecision M \<in> set (decisions M)
lastDecision M \<in> set (decisions M) \<Longrightarrow> lastDecision M \<in> set (elements M)

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

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
hence "var (lastDecision M) \<in> vars (elements M)"
[PROOF STATE]
proof (prove)
using this:
lastDecision M el elements M

goal (1 subgoal):
 1. var (lastDecision M) \<in> vars (elements M)
[PROOF STEP]
using valuationContainsItsLiteralsVariable[of "lastDecision M" "elements M"]
[PROOF STATE]
proof (prove)
using this:
lastDecision M el elements M
lastDecision M el elements M \<Longrightarrow> var (lastDecision M) \<in> vars (elements M)

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

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
var (lastDecision M) \<in> vars (elements M)

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
have "vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
[PROOF STEP]
using isPrefixPrefixBeforeLastMarked[of "M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M

goal (1 subgoal):
 1. vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
[PROOF STEP]
using isPrefixElements[of "prefixBeforeLastDecision M" "M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)

goal (1 subgoal):
 1. vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
[PROOF STEP]
using varsPrefixValuation[of "elements (prefixBeforeLastDecision M)" "elements M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix (prefixBeforeLastDecision M) M
isPrefix (prefixBeforeLastDecision M) M \<Longrightarrow> isPrefix (elements (prefixBeforeLastDecision M)) (elements M)
isPrefix (elements (prefixBeforeLastDecision M)) (elements M) \<Longrightarrow> vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)

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

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
var (lastDecision M) \<in> vars (elements M)
vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
var (lastDecision M) \<in> vars (elements M)
vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
var (lastDecision M) \<in> vars (elements M)
vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
InvariantVarsM M F0 Vbl
decisions M \<noteq> []
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
using varsAppendValuation[of "elements (prefixBeforeLastDecision M)" "[opposite (lastDecision M)]"]
[PROOF STATE]
proof (prove)
using this:
var (lastDecision M) \<in> vars (elements M)
vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
InvariantVarsM M F0 Vbl
decisions M \<noteq> []
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
vars (elements (prefixBeforeLastDecision M) @ [opposite (lastDecision M)]) = vars (elements (prefixBeforeLastDecision M)) \<union> vars [opposite (lastDecision M)]

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
unfolding InvariantVarsM_def
[PROOF STATE]
proof (prove)
using this:
var (lastDecision M) \<in> vars (elements M)
vars (elements (prefixBeforeLastDecision M)) \<subseteq> vars (elements M)
vars (elements M) \<subseteq> vars F0 \<union> Vbl
decisions M \<noteq> []
M' = prefixBeforeLastDecision M @ [(opposite (lastDecision M), False)]
vars (elements (prefixBeforeLastDecision M) @ [opposite (lastDecision M)]) = vars (elements (prefixBeforeLastDecision M)) \<union> vars [opposite (lastDecision M)]

goal (1 subgoal):
 1. vars (elements M') \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
InvariantVarsM M' F0 Vbl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAfterBackjump:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail and bClause::Clause and bLiteral::Literal
  assumes "InvariantImpliedLiterals F M" and
  "isPrefix p M" and "formulaEntailsClause F bClause" and "isUnitClause bClause bLiteral (elements p)" and
  "M' = p @ [(bLiteral, False)]"
  shows "InvariantImpliedLiterals F M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
from \<open>InvariantImpliedLiterals F M\<close> \<open>isPrefix p M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
isPrefix p M
[PROOF STEP]
have "InvariantImpliedLiterals F p"
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
isPrefix p M

goal (1 subgoal):
 1. InvariantImpliedLiterals F p
[PROOF STEP]
using InvariantImpliedLiteralsHoldsForPrefix [of "F" "M" "p"]
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
isPrefix p M
\<lbrakk>InvariantImpliedLiterals F M; isPrefix p M\<rbrakk> \<Longrightarrow> InvariantImpliedLiterals F p

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

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
isPrefix p M
formulaEntailsClause F bClause
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
InvariantImpliedLiterals F p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
isPrefix p M
formulaEntailsClause F bClause
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
InvariantImpliedLiterals F p

goal (1 subgoal):
 1. InvariantImpliedLiterals F M'
[PROOF STEP]
using InvariantImpliedLiteralsAfterUnitPropagate [of "F" "p" "bClause" "bLiteral" "M'"]
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
isPrefix p M
formulaEntailsClause F bClause
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
InvariantImpliedLiterals F p
\<lbrakk>InvariantImpliedLiterals F p; formulaEntailsClause F bClause; isUnitClause bClause bLiteral (elements p); M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> InvariantImpliedLiterals F M'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantVarsMAfterBackjump:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail and bClause::Clause and bLiteral::Literal
  assumes "InvariantVarsM M F0 Vbl" and
  "isPrefix p M" and "var bLiteral \<in> vars F0 \<union> Vbl" and
  "M' = p @ [(bLiteral, False)]"
  shows "InvariantVarsM M' F0 Vbl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
from \<open>InvariantVarsM M F0 Vbl\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantVarsM M F0 Vbl
[PROOF STEP]
have "vars (elements M) \<subseteq> vars F0 \<union> Vbl"
[PROOF STATE]
proof (prove)
using this:
InvariantVarsM M F0 Vbl

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

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

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vars (elements M) \<subseteq> vars F0 \<union> Vbl

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

goal (1 subgoal):
 1. vars (elements p) \<subseteq> vars (elements M)
[PROOF STEP]
using varsPrefixValuation [of "elements p" "elements M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
isPrefix (elements p) (elements M) \<Longrightarrow> vars (elements p) \<subseteq> vars (elements M)

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

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vars (elements M) \<subseteq> vars F0 \<union> Vbl
vars (elements p) \<subseteq> vars (elements M)
[PROOF STEP]
have "vars (elements p) \<subseteq> vars F0 \<union> Vbl"
[PROOF STATE]
proof (prove)
using this:
vars (elements M) \<subseteq> vars F0 \<union> Vbl
vars (elements p) \<subseteq> vars (elements M)

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

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
with \<open>vars (elements p) \<subseteq> vars F0 \<union> Vbl\<close> assms
[PROOF STATE]
proof (chain)
picking this:
vars (elements p) \<subseteq> vars F0 \<union> Vbl
InvariantVarsM M F0 Vbl
isPrefix p M
var bLiteral \<in> vars F0 \<union> Vbl
M' = p @ [(bLiteral, False)]
vars (elements p) \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars (elements p) \<subseteq> vars F0 \<union> Vbl
InvariantVarsM M F0 Vbl
isPrefix p M
var bLiteral \<in> vars F0 \<union> Vbl
M' = p @ [(bLiteral, False)]
vars (elements p) \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
using InvariantVarsMAfterUnitPropagate[of  "p" "F0" "Vbl" "bLiteral" "M'"]
[PROOF STATE]
proof (prove)
using this:
vars (elements p) \<subseteq> vars F0 \<union> Vbl
InvariantVarsM M F0 Vbl
isPrefix p M
var bLiteral \<in> vars F0 \<union> Vbl
M' = p @ [(bLiteral, False)]
vars (elements p) \<subseteq> vars F0 \<union> Vbl
\<lbrakk>InvariantVarsM p F0 Vbl; var bLiteral \<in> vars F0 \<union> Vbl; M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> InvariantVarsM M' F0 Vbl

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
unfolding InvariantVarsM_def
[PROOF STATE]
proof (prove)
using this:
vars (elements p) \<subseteq> vars F0 \<union> Vbl
vars (elements M) \<subseteq> vars F0 \<union> Vbl
isPrefix p M
var bLiteral \<in> vars F0 \<union> Vbl
M' = p @ [(bLiteral, False)]
vars (elements p) \<subseteq> vars F0 \<union> Vbl
\<lbrakk>vars (elements p) \<subseteq> vars F0 \<union> Vbl; var bLiteral \<in> vars F0 \<union> Vbl; M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> vars (elements M') \<subseteq> vars F0 \<union> Vbl

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantConsistentAfterBackjump:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail and bClause::Clause and bLiteral::Literal
  assumes "InvariantConsistent M" and
  "isPrefix p M" and "isUnitClause bClause bLiteral (elements p)" and
  "M' = p @ [(bLiteral, False)]"
  shows "InvariantConsistent M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
from \<open>InvariantConsistent M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
[PROOF STEP]
have "consistent (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M

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

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with \<open>isPrefix p M\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix p M
consistent (elements M)
[PROOF STEP]
have "consistent (elements p)"
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
consistent (elements M)

goal (1 subgoal):
 1. consistent (elements p)
[PROOF STEP]
using consistentPrefix [of "elements p" "elements M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
consistent (elements M)
\<lbrakk>isPrefix (elements p) (elements M); consistent (elements M)\<rbrakk> \<Longrightarrow> consistent (elements p)

goal (1 subgoal):
 1. consistent (elements p)
[PROOF STEP]
by (simp add: isPrefixElements)
[PROOF STATE]
proof (state)
this:
consistent (elements p)

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
consistent (elements p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
consistent (elements p)

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
using InvariantConsistentAfterUnitPropagate [of "p" "bClause" "bLiteral" "M'"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
consistent (elements p)
\<lbrakk>InvariantConsistent p; isUnitClause bClause bLiteral (elements p); M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> InvariantConsistent M'

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
unfolding InvariantConsistent_def
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
consistent (elements p)
\<lbrakk>consistent (elements p); isUnitClause bClause bLiteral (elements p); M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> consistent (elements M')

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantUniqAfterBackjump:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail and bClause::Clause and bLiteral::Literal
  assumes "InvariantUniq M" and
  "isPrefix p M"  and "isUnitClause bClause bLiteral (elements p)" and
  "M' = p @ [(bLiteral, False)]"
  shows "InvariantUniq M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
from \<open>InvariantUniq M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantUniq M
[PROOF STEP]
have "uniq (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M

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

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
with \<open>isPrefix p M\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix p M
uniq (elements M)
[PROOF STEP]
have "uniq (elements p)"
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
uniq (elements M)

goal (1 subgoal):
 1. uniq (elements p)
[PROOF STEP]
using uniqElementsTrailImpliesUniqElementsPrefix [of "p" "M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
uniq (elements M)
\<lbrakk>isPrefix p M; uniq (elements M)\<rbrakk> \<Longrightarrow> uniq (elements p)

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
InvariantUniq M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
uniq (elements p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
uniq (elements p)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
using InvariantUniqAfterUnitPropagate[of "p" "bClause" "bLiteral" "M'"]
[PROOF STATE]
proof (prove)
using this:
InvariantUniq M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
uniq (elements p)
\<lbrakk>InvariantUniq p; isUnitClause bClause bLiteral (elements p); M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> InvariantUniq M'

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
unfolding InvariantUniq_def
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
isPrefix p M
isUnitClause bClause bLiteral (elements p)
M' = p @ [(bLiteral, False)]
uniq (elements p)
\<lbrakk>uniq (elements p); isUnitClause bClause bLiteral (elements p); M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> uniq (elements M')

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantReasonClausesAfterBackjump:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail and bClause::Clause and bLiteral::Literal
  assumes "InvariantReasonClauses F M" and "InvariantUniq M"  and
  "isPrefix p M"  and "isUnitClause bClause bLiteral (elements p)" and "formulaEntailsClause F bClause" and
  "M' = p @ [(bLiteral, False)]"
  shows "InvariantReasonClauses F M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
from \<open>InvariantReasonClauses F M\<close> \<open>InvariantUniq M\<close> \<open>isPrefix p M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantReasonClauses F M
InvariantUniq M
isPrefix p M
[PROOF STEP]
have "InvariantReasonClauses F p"
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M
InvariantUniq M
isPrefix p M

goal (1 subgoal):
 1. InvariantReasonClauses F p
[PROOF STEP]
by (rule InvariantReasonClausesHoldsForPrefix)
[PROOF STATE]
proof (state)
this:
InvariantReasonClauses F p

goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
InvariantReasonClauses F M
InvariantUniq M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
formulaEntailsClause F bClause
M' = p @ [(bLiteral, False)]
InvariantReasonClauses F p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M
InvariantUniq M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
formulaEntailsClause F bClause
M' = p @ [(bLiteral, False)]
InvariantReasonClauses F p

goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
using InvariantReasonClausesAfterUnitPropagate [of "F" "p" "bClause" "bLiteral" "M'"]
[PROOF STATE]
proof (prove)
using this:
InvariantReasonClauses F M
InvariantUniq M
isPrefix p M
isUnitClause bClause bLiteral (elements p)
formulaEntailsClause F bClause
M' = p @ [(bLiteral, False)]
InvariantReasonClauses F p
\<lbrakk>InvariantReasonClauses F p; formulaEntailsClause F bClause; isUnitClause bClause bLiteral (elements p); M' = p @ [(bLiteral, False)]\<rbrakk> \<Longrightarrow> InvariantReasonClauses F M'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAfterLearn:
  fixes F :: Formula and F' :: Formula and M :: LiteralTrail and C :: Clause
  assumes "InvariantImpliedLiterals F M" and
  "F' = F @ [C]"
  shows "InvariantImpliedLiterals F' M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
from \<open>InvariantImpliedLiterals F M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
[PROOF STEP]
have *: "\<forall> l. l el (elements M) \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l"
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M

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

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

goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l

goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
fix literal :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
assume "literal el (elements M)"
[PROOF STATE]
proof (state)
this:
literal el elements M

goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
literal el elements M
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal"
[PROOF STATE]
proof (prove)
using this:
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
literal el elements M

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal

goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
hence "formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal \<Longrightarrow> formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal
[PROOF STEP]
have "\<forall> clause::Clause. clause el (F @ val2form (decisionsTo literal M)) \<longrightarrow> clause el (F @ [C] @ val2form (decisionsTo literal M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
fix clause :: Clause
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
have "clause el (F @ val2form (decisionsTo literal M)) \<longrightarrow> clause el (F @ [C] @ val2form (decisionsTo literal M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clause el F @ val2form (decisionsTo literal M) \<Longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
assume "clause el (F @ val2form (decisionsTo literal M))"
[PROOF STATE]
proof (state)
this:
clause el F @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. clause el F @ val2form (decisionsTo literal M) \<Longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
thus "clause el (F @ [C] @ val2form (decisionsTo literal M))"
[PROOF STATE]
proof (prove)
using this:
clause el F @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
clause el F @ [C] @ val2form (decisionsTo literal M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?clause2 el F @ val2form (decisionsTo literal M) \<longrightarrow> ?clause2 el F @ [C] @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?clause2 el F @ val2form (decisionsTo literal M) \<longrightarrow> ?clause2 el F @ [C] @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. \<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal \<Longrightarrow> formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal
[PROOF STEP]
with \<open>formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal
\<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (F @ val2form (decisionsTo literal M)) literal
\<forall>clause. clause el F @ val2form (decisionsTo literal M) \<longrightarrow> clause el F @ [C] @ val2form (decisionsTo literal M)

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal
[PROOF STEP]
by (rule formulaEntailsLiteralSubset)
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo literal M)) literal

goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?literal2 el elements M \<Longrightarrow> formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo ?literal2 M)) ?literal2

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

goal (1 subgoal):
 1. InvariantImpliedLiterals F' M
[PROOF STEP]
unfolding InvariantImpliedLiterals_def
[PROOF STATE]
proof (prove)
using this:
?literal2 el elements M \<Longrightarrow> formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo ?literal2 M)) ?literal2

goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F' @ val2form (decisionsTo l M)) l
[PROOF STEP]
using \<open>F' = F @ [C]\<close>
[PROOF STATE]
proof (prove)
using this:
?literal2 el elements M \<Longrightarrow> formulaEntailsLiteral (F @ [C] @ val2form (decisionsTo ?literal2 M)) ?literal2
F' = F @ [C]

goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F' @ val2form (decisionsTo l M)) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
InvariantImpliedLiterals F' M

goal:
No subgoals!
[PROOF STEP]
qed