[STATEMENT]
lemma OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_zero1[simp,code_unfold] :
"(x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) = (if \<upsilon> x and not (\<delta> x) then invalid else x endif)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) = (if \<upsilon> x and not (\<delta> x) then invalid else x endif)
[PROOF STEP]
proof (rule ext, rename_tac \<tau>, case_tac "(\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
 2. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
fix \<tau>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
 2. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
show "(\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau> \<Longrightarrow>
              (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
apply(subst OclIf_true', simp add: OclValid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = invalid \<tau>
[PROOF STEP]
by (metis OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def OclNot_defargs OclValid_def foundation5 foundation9)
[PROOF STATE]
proof (state)
this:
(\<upsilon> x and not (\<delta> x)) \<tau> = true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>

goal (1 subgoal):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
fix \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
have A: "\<And>\<tau>. (\<tau> \<Turnstile> not (\<upsilon> x and not (\<delta> x))) = (x \<tau> = invalid \<tau> \<or> \<tau> \<Turnstile> \<delta> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. (\<tau> \<Turnstile> not (\<upsilon> x and not (\<delta> x))) = (x \<tau> = invalid \<tau> \<or> \<tau> \<Turnstile> \<delta> x)
[PROOF STEP]
by (metis OclNot_not OclOr_def defined5 defined6 defined_not_I foundation11 foundation18'
            foundation6 foundation7 foundation9 invalid_def)
[PROOF STATE]
proof (state)
this:
(?\<tau> \<Turnstile> not (\<upsilon> x and not (\<delta> x))) = (x ?\<tau> = invalid ?\<tau> \<or> ?\<tau> \<Turnstile> \<delta> x)

goal (1 subgoal):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
have B: "\<tau> \<Turnstile> \<delta> x \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>
[PROOF STEP]
apply(cases "x \<tau>", metis bot_option_def foundation16)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<tau> \<Turnstile> \<delta> x; x \<tau> = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>
[PROOF STEP]
apply(rename_tac x', case_tac x', metis bot_option_def foundation16 null_option_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x' a. \<lbrakk>\<tau> \<Turnstile> \<delta> x; x \<tau> = \<lfloor>x'\<rfloor>; x' = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile> \<delta> x \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>

goal (1 subgoal):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
show "(x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>"
    when "\<tau> \<Turnstile> not (\<upsilon> x and not (\<delta> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>
[PROOF STEP]
apply(insert that, subst OclIf_false', simp, simp add: A, auto simp: OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def OclReal0_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<tau> = invalid \<tau>; (\<delta> x) \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>invalid \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = invalid \<tau>
 2. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>
 3. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> \<noteq> true \<tau>\<rbrakk> \<Longrightarrow> invalid \<tau> = x \<tau>
[PROOF STEP]
(* *)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<tau> = invalid \<tau>; (\<delta> x) \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>invalid \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = invalid \<tau>
 2. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>
 3. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> \<noteq> true \<tau>\<rbrakk> \<Longrightarrow> invalid \<tau> = x \<tau>
[PROOF STEP]
apply(simp add: foundation16'[simplified OclValid_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor> = x \<tau>
 2. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> \<noteq> true \<tau>\<rbrakk> \<Longrightarrow> invalid \<tau> = x \<tau>
[PROOF STEP]
apply(simp add: B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<delta> x; (\<delta> x) \<tau> \<noteq> true \<tau>\<rbrakk> \<Longrightarrow> invalid \<tau> = x \<tau>
[PROOF STEP]
by(simp add: OclValid_def)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile> not (\<upsilon> x and not (\<delta> x)) \<Longrightarrow> (x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l \<zero>.\<zero>) \<tau> = (if \<upsilon> x and not (\<delta> x) then invalid else x endif) \<tau>

goal (1 subgoal):
 1. \<And>\<tau>. (\<upsilon> x and not (\<delta> x)) \<tau> \<noteq> true \<tau> \<Longrightarrow> \<tau> \<Turnstile> not (\<upsilon> x and not (\<delta> x))
[PROOF STEP]
qed(metis OclValid_def defined5 defined6 defined_and_I defined_not_I foundation9)


[STATEMENT]
lemma OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_zero2[simp,code_unfold] :
"(\<zero>.\<zero> +\<^sub>r\<^sub>e\<^sub>a\<^sub>l x) = (if \<upsilon> x and not (\<delta> x) then invalid else x endif)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<zero>.\<zero> +\<^sub>r\<^sub>e\<^sub>a\<^sub>l x) = (if \<upsilon> x and not (\<delta> x) then invalid else x endif)
[PROOF STEP]
by(subst OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_commute, simp)


[STATEMENT]
lemma real_non_null [simp]: "((\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>) \<doteq> (null::('\<AA>)Real)) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>) \<doteq> null) = false
[PROOF STEP]
by(rule ext,auto simp: StrictRefEq\<^sub>R\<^sub>e\<^sub>a\<^sub>l valid_def
                         bot_fun_def bot_option_def null_fun_def null_option_def StrongEq_def)


[STATEMENT]
lemma null_non_real [simp]: "((null::('\<AA>)Real) \<doteq> (\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>)) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> (\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>)) = false
[PROOF STEP]
by(rule ext,auto simp: StrictRefEq\<^sub>R\<^sub>e\<^sub>a\<^sub>l valid_def
                         bot_fun_def bot_option_def null_fun_def null_option_def StrongEq_def)


[STATEMENT]
lemma OclReal0_non_null [simp,code_unfold]: "(\<zero>.\<zero> \<doteq> null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<zero>.\<zero> \<doteq> null) = false
[PROOF STEP]
by(simp add: OclReal0_def)


[STATEMENT]
lemma null_non_OclReal0 [simp,code_unfold]: "(null \<doteq> \<zero>.\<zero>) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> \<zero>.\<zero>) = false
[PROOF STEP]
by(simp add: OclReal0_def)


[STATEMENT]
lemma OclReal1_non_null [simp,code_unfold]: "(\<one>.\<zero> \<doteq> null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<one>.\<zero> \<doteq> null) = false
[PROOF STEP]
by(simp add: OclReal1_def)


[STATEMENT]
lemma null_non_OclReal1 [simp,code_unfold]: "(null \<doteq> \<one>.\<zero>) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> \<one>.\<zero>) = false
[PROOF STEP]
by(simp add: OclReal1_def)


[STATEMENT]
lemma OclReal2_non_null [simp,code_unfold]: "(\<two>.\<zero> \<doteq> null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<two>.\<zero> \<doteq> null) = false
[PROOF STEP]
by(simp add: OclReal2_def)


[STATEMENT]
lemma null_non_OclReal2 [simp,code_unfold]: "(null \<doteq> \<two>.\<zero>) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> \<two>.\<zero>) = false
[PROOF STEP]
by(simp add: OclReal2_def)


[STATEMENT]
lemma OclReal6_non_null [simp,code_unfold]: "(\<six>.\<zero> \<doteq> null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<six>.\<zero> \<doteq> null) = false
[PROOF STEP]
by(simp add: OclReal6_def)


[STATEMENT]
lemma null_non_OclReal6 [simp,code_unfold]: "(null \<doteq> \<six>.\<zero>) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> \<six>.\<zero>) = false
[PROOF STEP]
by(simp add: OclReal6_def)


[STATEMENT]
lemma OclReal8_non_null [simp,code_unfold]: "(\<eight>.\<zero> \<doteq> null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<eight>.\<zero> \<doteq> null) = false
[PROOF STEP]
by(simp add: OclReal8_def)


[STATEMENT]
lemma null_non_OclReal8 [simp,code_unfold]: "(null \<doteq> \<eight>.\<zero>) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> \<eight>.\<zero>) = false
[PROOF STEP]
by(simp add: OclReal8_def)


[STATEMENT]
lemma OclReal9_non_null [simp,code_unfold]: "(\<nine>.\<zero> \<doteq> null) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nine>.\<zero> \<doteq> null) = false
[PROOF STEP]
by(simp add: OclReal9_def)


[STATEMENT]
lemma null_non_OclReal9 [simp,code_unfold]: "(null \<doteq> \<nine>.\<zero>) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null \<doteq> \<nine>.\<zero>) = false
[PROOF STEP]
by(simp add: OclReal9_def)


[STATEMENT]
lemma InvariantImpliedLiteralsWeakerVariant:
  fixes M :: LiteralTrail and F :: Formula
  assumes "\<forall> l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l"
  shows "\<forall> l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
fix l :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
assume "l el elements M"
[PROOF STATE]
proof (state)
this:
l el elements M

goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
l el elements M
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l"
[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 (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
have "isPrefix (decisionsTo l M) (decisions M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPrefix (decisionsTo l M) (decisions M)
[PROOF STEP]
by (simp add: markedElementsToArePrefixOfMarkedElements)
[PROOF STATE]
proof (state)
this:
isPrefix (decisionsTo l M) (decisions M)

goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isPrefix (decisionsTo l M) (decisions M)
[PROOF STEP]
obtain s :: Valuation
      where "(decisionsTo l M) @ s = (decisions M)"
[PROOF STATE]
proof (prove)
using this:
isPrefix (decisionsTo l M) (decisions M)

goal (1 subgoal):
 1. (\<And>s. decisionsTo l M @ s = decisions M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using isPrefix_def [of "decisionsTo l M" "decisions M"]
[PROOF STATE]
proof (prove)
using this:
isPrefix (decisionsTo l M) (decisions M)
isPrefix (decisionsTo l M) (decisions M) = (\<exists>s. decisionsTo l M @ s = decisions M)

goal (1 subgoal):
 1. (\<And>s. decisionsTo l M @ s = decisions M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
decisionsTo l M @ s = decisions M

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

goal (1 subgoal):
 1. decisions M = decisionsTo l M @ s
[PROOF STEP]
by (rule sym)
[PROOF STATE]
proof (state)
this:
decisions M = decisionsTo l M @ s

goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
with \<open>formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
decisions M = decisionsTo l M @ s
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisions M)) l"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
decisions M = decisionsTo l M @ s

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
using formulaEntailsLiteralAppend [of "F @ val2form (decisionsTo l M)" "l" "val2form s"]
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
decisions M = decisionsTo l M @ s
formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l \<Longrightarrow> formulaEntailsLiteral ((F @ val2form (decisionsTo l M)) @ val2form s) l

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

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

goal (1 subgoal):
 1. \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?l2 el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) ?l2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAndElementsEntailLiteralThenDecisionsEntailLiteral:
  fixes M :: LiteralTrail and F :: Formula and literal :: Literal
  assumes "InvariantImpliedLiterals F M" and "formulaEntailsLiteral (F @ (val2form (elements M))) literal"
  shows "formulaEntailsLiteral (F @ val2form (decisions M)) literal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
fix valuation :: Valuation
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
assume "model valuation (F @ val2form (decisions M))"
[PROOF STATE]
proof (state)
this:
model valuation (F @ val2form (decisions M))

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
hence "formulaTrue F valuation" and "formulaTrue (val2form (decisions M)) valuation" and "consistent valuation"
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ val2form (decisions M))

goal (1 subgoal):
 1. formulaTrue F valuation &&& formulaTrue (val2form (decisions M)) valuation &&& consistent valuation
[PROOF STEP]
by (auto simp add: formulaTrueAppend)
[PROOF STATE]
proof (state)
this:
formulaTrue F valuation
formulaTrue (val2form (decisions M)) valuation
consistent valuation

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
formulaTrue F valuation
formulaTrue (val2form (decisions M)) valuation
consistent valuation

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
fix l :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
assume "l el (elements M)"
[PROOF STATE]
proof (state)
this:
l el elements M

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[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 (decisions 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 (decisions M)) l
[PROOF STEP]
by (simp add: InvariantImpliedLiteralsWeakerVariant InvariantImpliedLiterals_def)
[PROOF STATE]
proof (state)
this:
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l

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

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

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
with \<open>model valuation (F @ val2form (decisions M))\<close>
[PROOF STATE]
proof (chain)
picking this:
model valuation (F @ val2form (decisions M))
formulaEntailsLiteral (F @ val2form (decisions M)) l
[PROOF STEP]
have "literalTrue l valuation"
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ val2form (decisions M))
formulaEntailsLiteral (F @ val2form (decisions M)) l

goal (1 subgoal):
 1. literalTrue l valuation
[PROOF STEP]
by (simp add: formulaEntailsLiteral_def)
[PROOF STATE]
proof (state)
this:
literalTrue l valuation

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l2 el elements M \<Longrightarrow> literalTrue ?l2 valuation

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
hence "formulaTrue (val2form (elements M)) valuation"
[PROOF STATE]
proof (prove)
using this:
?l2 el elements M \<Longrightarrow> literalTrue ?l2 valuation

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

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
with \<open>formulaTrue F valuation\<close> \<open>consistent valuation\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaTrue F valuation
consistent valuation
formulaTrue (val2form (elements M)) valuation
[PROOF STEP]
have "model valuation (F @ (val2form (elements M)))"
[PROOF STATE]
proof (prove)
using this:
formulaTrue F valuation
consistent valuation
formulaTrue (val2form (elements M)) valuation

goal (1 subgoal):
 1. model valuation (F @ val2form (elements M))
[PROOF STEP]
by (auto simp add:formulaTrueAppend)
[PROOF STATE]
proof (state)
this:
model valuation (F @ val2form (elements M))

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
with \<open>formulaEntailsLiteral (F @ (val2form (elements M))) literal\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsLiteral (F @ val2form (elements M)) literal
model valuation (F @ val2form (elements M))
[PROOF STEP]
have "literalTrue literal valuation"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsLiteral (F @ val2form (elements M)) literal
model valuation (F @ val2form (elements M))

goal (1 subgoal):
 1. literalTrue literal valuation
[PROOF STEP]
by (simp add: formulaEntailsLiteral_def)
[PROOF STATE]
proof (state)
this:
literalTrue literal valuation

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
model ?valuation2 (F @ val2form (decisions M)) \<Longrightarrow> literalTrue literal ?valuation2

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
model ?valuation2 (F @ val2form (decisions M)) \<Longrightarrow> literalTrue literal ?valuation2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAndFormulaFalseThenFormulaAndDecisionsAreNotSatisfiable:
  fixes M :: LiteralTrail and F :: Formula
  assumes "InvariantImpliedLiterals F M" and "formulaFalse F (elements M)"
  shows "\<not> satisfiable (F @ val2form (decisions M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
from \<open>formulaFalse F (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaFalse F (elements M)
[PROOF STEP]
have "formulaFalse (F @ val2form (decisions M)) (elements M)"
[PROOF STATE]
proof (prove)
using this:
formulaFalse F (elements M)

goal (1 subgoal):
 1. formulaFalse (F @ val2form (decisions M)) (elements M)
[PROOF STEP]
by (simp add: formulaFalseAppend)
[PROOF STATE]
proof (state)
this:
formulaFalse (F @ val2form (decisions M)) (elements M)

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

goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
from \<open>InvariantImpliedLiterals F M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
[PROOF STEP]
have "formulaEntailsValuation (F @ val2form (decisions M)) (elements M)"
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M

goal (1 subgoal):
 1. formulaEntailsValuation (F @ val2form (decisions M)) (elements M)
[PROOF STEP]
unfolding formulaEntailsValuation_def
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M

goal (1 subgoal):
 1. \<forall>literal. literal el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) literal
[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>literal. literal el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) literal
[PROOF STEP]
using InvariantImpliedLiteralsWeakerVariant[of "M" "F"]
[PROOF STATE]
proof (prove)
using this:
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l
\<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l \<Longrightarrow> \<forall>l. l el elements M \<longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M)) l

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

goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
formulaFalse (F @ val2form (decisions M)) (elements M)
formulaEntailsValuation (F @ val2form (decisions M)) (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
formulaFalse (F @ val2form (decisions M)) (elements M)
formulaEntailsValuation (F @ val2form (decisions M)) (elements M)

goal (1 subgoal):
 1. \<not> satisfiable (F @ val2form (decisions M))
[PROOF STEP]
using formulaFalseInEntailedValuationIsUnsatisfiable [of "F @ val2form (decisions M)" "elements M"]
[PROOF STATE]
proof (prove)
using this:
formulaFalse (F @ val2form (decisions M)) (elements M)
formulaEntailsValuation (F @ val2form (decisions M)) (elements M)
\<lbrakk>formulaFalse (F @ val2form (decisions M)) (elements M); formulaEntailsValuation (F @ val2form (decisions M)) (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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsHoldsForPrefix:
  fixes M :: LiteralTrail and prefix :: LiteralTrail and F :: Formula
  assumes "InvariantImpliedLiterals F M"  and "isPrefix prefix M"
  shows "InvariantImpliedLiterals F prefix"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
fix l :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
assume *: "l el elements prefix"
[PROOF STATE]
proof (state)
this:
l el elements prefix

goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
from * \<open>isPrefix prefix M\<close>
[PROOF STATE]
proof (chain)
picking this:
l el elements prefix
isPrefix prefix M
[PROOF STEP]
have "l el elements M"
[PROOF STATE]
proof (prove)
using this:
l el elements prefix
isPrefix prefix M

goal (1 subgoal):
 1. l el elements M
[PROOF STEP]
unfolding isPrefix_def
[PROOF STATE]
proof (prove)
using this:
l el elements prefix
\<exists>s. prefix @ s = M

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

goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
from * and \<open>isPrefix prefix M\<close>
[PROOF STATE]
proof (chain)
picking this:
l el elements prefix
isPrefix prefix M
[PROOF STEP]
have "decisionsTo l prefix = decisionsTo l M"
[PROOF STATE]
proof (prove)
using this:
l el elements prefix
isPrefix prefix M

goal (1 subgoal):
 1. decisionsTo l prefix = decisionsTo l M
[PROOF STEP]
using markedElementsToPrefixElement [of "prefix" "M" "l"]
[PROOF STATE]
proof (prove)
using this:
l el elements prefix
isPrefix prefix M
\<lbrakk>isPrefix prefix M; l \<in> set (elements prefix)\<rbrakk> \<Longrightarrow> decisionsTo l M = decisionsTo l prefix

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

goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
from \<open>InvariantImpliedLiterals F M\<close> and \<open>l el elements 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]
by (simp add:InvariantImpliedLiterals_def)
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l

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

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

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

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

goal (1 subgoal):
 1. InvariantImpliedLiterals F prefix
[PROOF STEP]
by (auto simp add: InvariantImpliedLiterals_def)
[PROOF STATE]
proof (state)
this:
InvariantImpliedLiterals F prefix

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantReasonClausesHoldsForPrefix:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail
  assumes "InvariantReasonClauses F M" and "InvariantUniq M"  and
  "isPrefix p M"
  shows "InvariantReasonClauses F p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantReasonClauses F p
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F p
[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 p
[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]
by simp
[PROOF STATE]
proof (state)
this:
uniq (elements M)

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

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

goal (1 subgoal):
 1. InvariantReasonClauses F p
[PROOF STEP]
from \<open>isPrefix p M\<close> \<open>literal el (elements p)\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix p M
literal el elements p
[PROOF STEP]
have "literal el (elements M)"
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
literal el elements p

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

goal (1 subgoal):
 1. InvariantReasonClauses F p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
literal el elements M

goal (1 subgoal):
 1. InvariantReasonClauses F p
[PROOF STEP]
from \<open>isPrefix p M\<close> \<open>literal el (elements p)\<close> \<open>\<not> literal el (decisions p)\<close> \<open>uniq (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix p M
literal el elements p
\<not> literal el decisions p
uniq (elements M)
[PROOF STEP]
have "\<not> literal el decisions M"
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
literal el elements p
\<not> literal el decisions p
uniq (elements M)

goal (1 subgoal):
 1. \<not> literal el decisions M
[PROOF STEP]
using markedElementsTrailMemPrefixAreMarkedElementsPrefix [of "M" "p" "literal"]
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
literal el elements p
\<not> literal el decisions p
uniq (elements M)
\<lbrakk>uniq (elements M); isPrefix p M; literal \<in> set (elements p); literal \<in> set (decisions M)\<rbrakk> \<Longrightarrow> literal \<in> set (decisions p)

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

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

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

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

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

goal (1 subgoal):
 1. isReason clause literal (elements p)
[PROOF STEP]
using isReasonHoldsInPrefix[of "literal" "elements p" "elements M" "clause"]
[PROOF STATE]
proof (prove)
using this:
literal el elements p
\<not> literal el decisions p
isPrefix p M
formulaEntailsClause F clause
isReason clause literal (elements M)
\<lbrakk>literal el elements p; isPrefix (elements p) (elements M); isReason clause literal (elements M)\<rbrakk> \<Longrightarrow> isReason clause literal (elements p)

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantReasonClausesHoldsForPrefixElements:
  fixes F::Formula and M::LiteralTrail and p::LiteralTrail
  assumes "InvariantReasonClauses F p" and
  "isPrefix p M" and
  "literal el (elements p)" and "\<not> literal el decisions M"
  shows "\<exists> clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
from \<open>isPrefix p M\<close> \<open>\<not> literal el (decisions M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isPrefix p M
\<not> literal el decisions M
[PROOF STEP]
have "\<not> literal el (decisions p)"
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
\<not> literal el decisions M

goal (1 subgoal):
 1. \<not> literal el decisions p
[PROOF STEP]
using markedElementsPrefixAreMarkedElementsTrail[of "p" "M" "literal"]
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
\<not> literal el decisions M
\<lbrakk>isPrefix p M; literal \<in> set (decisions p)\<rbrakk> \<Longrightarrow> literal \<in> set (decisions M)

goal (1 subgoal):
 1. \<not> literal el decisions p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> literal el decisions p

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

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

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

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

goal (1 subgoal):
 1. isReason clause literal (elements M)
[PROOF STEP]
using isReasonAppend [of "clause" "literal" "elements p"]
[PROOF STATE]
proof (prove)
using this:
isPrefix p M
formulaEntailsClause F clause
isReason clause literal (elements p)
isReason clause literal (elements p) \<Longrightarrow> isReason clause literal (elements p @ ?valuation')

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

goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal (elements M)
[PROOF STEP]
with \<open>formulaEntailsClause F clause\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsClause F clause
isReason clause literal (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F clause
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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantUniqAfterDecide:
  fixes M :: LiteralTrail and literal :: Literal and M' :: LiteralTrail
  assumes "InvariantUniq M" and
  "var literal \<notin> vars (elements M)" and
  "M' = M @ [(literal, True)]"
  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]
{
[PROOF STATE]
proof (state)
this:
uniq (elements M)

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
assume "\<not> uniq (elements M')"
[PROOF STATE]
proof (state)
this:
\<not> uniq (elements M')

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
with \<open>uniq (elements M)\<close> \<open>M' = M @ [(literal, True)]\<close>
[PROOF STATE]
proof (chain)
picking this:
uniq (elements M)
M' = M @ [(literal, True)]
\<not> uniq (elements M')
[PROOF STEP]
have "literal el (elements M)"
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
M' = M @ [(literal, True)]
\<not> uniq (elements M')

goal (1 subgoal):
 1. literal el elements M
[PROOF STEP]
using uniqButlastNotUniqListImpliesLastMemButlast [of "elements M'"]
[PROOF STATE]
proof (prove)
using this:
uniq (elements M)
M' = M @ [(literal, True)]
\<not> uniq (elements M')
\<lbrakk>uniq (butlast (elements M')); \<not> uniq (elements M')\<rbrakk> \<Longrightarrow> last (elements M') \<in> set (butlast (elements M'))

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

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

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

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

goal (1 subgoal):
 1. InvariantUniq M'
[PROOF STEP]
with \<open>var literal \<notin> vars (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
var literal \<notin> vars (elements M)
var literal \<in> vars (elements M)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
var literal \<notin> vars (elements M)
var literal \<in> vars (elements M)

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAfterDecide:
  fixes F :: Formula and M :: LiteralTrail and literal :: Literal and M' :: LiteralTrail
  assumes "InvariantImpliedLiterals F M" and
  "var literal \<notin> vars (elements M)" and
  "M' = M @ [(literal, True)]"
  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]
{
[PROOF STATE]
proof (state)
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]
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 M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
 2. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l el elements M

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
have "clauseEntailsLiteral [literal] literal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clauseEntailsLiteral [literal] literal
[PROOF STEP]
by (simp add: clauseEntailsLiteral_def)
[PROOF STATE]
proof (state)
this:
clauseEntailsLiteral [literal] literal

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

goal (1 subgoal):
 1. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
have "[literal] el (F @ val2form (decisions M) @ [[literal]])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [literal] el F @ val2form (decisions M) @ [[literal]]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[literal] el F @ val2form (decisions M) @ [[literal]]

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

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

goal (1 subgoal):
 1. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
have "isDecision (last (M @ [(literal, True)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDecision (last (M @ [(literal, True)]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isDecision (last (M @ [(literal, True)]))

goal (1 subgoal):
 1. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isDecision (last (M @ [(literal, True)]))

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

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

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

goal (1 subgoal):
 1. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isDecision (last (M @ [(literal, True)]))
\<not> literal el elements M
[PROOF STEP]
have "decisionsTo literal (M @ [(literal, True)])  = ((decisions M) @ [literal])"
[PROOF STATE]
proof (prove)
using this:
isDecision (last (M @ [(literal, True)]))
\<not> literal el elements M

goal (1 subgoal):
 1. decisionsTo literal (M @ [(literal, True)]) = decisions M @ [literal]
[PROOF STEP]
using lastTrailElementMarkedImpliesMarkedElementsToLastElementAreAllMarkedElements [of "M @ [(literal, True)]"]
[PROOF STATE]
proof (prove)
using this:
isDecision (last (M @ [(literal, True)]))
\<not> literal el elements M
\<lbrakk>isDecision (last (M @ [(literal, True)])); last (elements (M @ [(literal, True)])) \<notin> set (butlast (elements (M @ [(literal, True)])))\<rbrakk> \<Longrightarrow> decisionsTo (last (elements (M @ [(literal, True)]))) (M @ [(literal, True)]) = decisions (M @ [(literal, True)])

goal (1 subgoal):
 1. decisionsTo literal (M @ [(literal, True)]) = decisions M @ [literal]
[PROOF STEP]
by (simp add:markedElementsAppend)
[PROOF STATE]
proof (state)
this:
decisionsTo literal (M @ [(literal, True)]) = decisions M @ [literal]

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

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

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
using \<open>M' = M @ [(literal, True)]\<close> \<open>l = literal\<close>
           clauseEntailsLiteralThenFormulaEntailsLiteral [of "[literal]" "F @ val2form (decisions M) @ [[literal]]" "literal"]
[PROOF STATE]
proof (prove)
using this:
clauseEntailsLiteral [literal] literal
[literal] el F @ val2form (decisions M) @ [[literal]]
decisionsTo literal (M @ [(literal, True)]) = decisions M @ [literal]
M' = M @ [(literal, True)]
l = literal
\<lbrakk>[literal] el F @ val2form (decisions M) @ [[literal]]; clauseEntailsLiteral [literal] literal\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisions M) @ [[literal]]) literal

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
by (simp add:val2formAppend)
[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:
?l2 el elements M' \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo ?l2 M')) ?l2

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantVarsMAfterDecide:
  fixes F :: Formula and F0 :: Formula and M :: LiteralTrail and literal :: Literal and M' :: LiteralTrail
  assumes "InvariantVarsM M F0 Vbl" and
  "var literal \<in> Vbl" and
  "M' = M @ [(literal, True)]"
  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]
by (simp only:InvariantVarsM_def)
[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>M' = M @ [(literal, True)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(literal, True)]
[PROOF STEP]
have "vars (elements M') = vars (elements (M @ [(literal, True)]))"
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(literal, True)]

goal (1 subgoal):
 1. vars (elements M') = vars (elements (M @ [(literal, True)]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (elements M') = vars (elements (M @ [(literal, True)]))

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vars (elements M') = vars (elements (M @ [(literal, True)]))

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
have "... = vars (elements M @ [literal])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (elements (M @ [(literal, True)])) = vars (elements M @ [literal])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (elements (M @ [(literal, True)])) = vars (elements M @ [literal])

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vars (elements (M @ [(literal, True)])) = vars (elements M @ [literal])

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
have "... = vars (elements M) \<union>  vars [literal]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (elements M @ [literal]) = vars (elements M) \<union> vars [literal]
[PROOF STEP]
using varsAppendClauses [of "elements M" "[literal]"]
[PROOF STATE]
proof (prove)
using this:
vars (elements M @ [literal]) = vars (elements M) \<union> vars [literal]

goal (1 subgoal):
 1. vars (elements M @ [literal]) = vars (elements M) \<union> vars [literal]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (elements M @ [literal]) = vars (elements M) \<union> vars [literal]

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vars (elements M') = vars (elements M) \<union> vars [literal]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars (elements M') = vars (elements M) \<union> vars [literal]

goal (1 subgoal):
 1. InvariantVarsM M' F0 Vbl
[PROOF STEP]
using \<open>vars (elements M) \<subseteq> (vars F0) \<union> Vbl\<close> \<open>var literal \<in> Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
vars (elements M') = vars (elements M) \<union> vars [literal]
vars (elements M) \<subseteq> vars F0 \<union> Vbl
var literal \<in> Vbl

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

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 InvariantConsistentAfterDecide:
  fixes M :: LiteralTrail and literal :: Literal and M' :: LiteralTrail
  assumes "InvariantConsistent M" and
  "var literal \<notin> vars (elements M)" and
  "M' = M @ [(literal, True)]"
  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]
{
[PROOF STATE]
proof (state)
this:
consistent (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 @ [(literal, True)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(literal, True)]
inconsistent (elements M')
[PROOF STEP]
have "inconsistent (elements M) \<or> inconsistent [literal] \<or> (\<exists> l. literalTrue l (elements M) \<and> literalFalse l [literal])"
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(literal, True)]
inconsistent (elements M')

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

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

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 [literal] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [literal])
[PROOF STEP]
obtain l :: Literal
      where "literalTrue l (elements M)" and "literalFalse l [literal]"
[PROOF STATE]
proof (prove)
using this:
consistent (elements M)
inconsistent (elements M) \<or> inconsistent [literal] \<or> (\<exists>l. literalTrue l (elements M) \<and> literalFalse l [literal])

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

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

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

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

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with \<open>literalTrue l (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
literalTrue l (elements M)
var literal = var l
[PROOF STEP]
have "var l \<in> vars (elements M)"
[PROOF STATE]
proof (prove)
using this:
literalTrue l (elements M)
var literal = var l

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

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

goal (1 subgoal):
 1. InvariantConsistent M'
[PROOF STEP]
with \<open>var literal = var l\<close> \<open>var literal \<notin> vars (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
var literal = var l
var literal \<notin> vars (elements M)
var l \<in> vars (elements M)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
var literal = var l
var literal \<notin> vars (elements M)
var l \<in> vars (elements M)

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 InvariantReasonClausesAfterDecide:
  fixes F :: Formula and M :: LiteralTrail and M' :: LiteralTrail
  assumes "InvariantReasonClauses F M" and "InvariantUniq M" and
  "M' = M @ [(literal, True)]"
  shows "InvariantReasonClauses F M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
fix literal' :: Literal
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
assume "literal' el elements M'" and "\<not> literal' el decisions M'"
[PROOF STATE]
proof (state)
this:
literal' el elements M'
\<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
InvariantUniq M
M' = M @ [(literal, True)]
\<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
InvariantUniq M
M' = M @ [(literal, True)]
\<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
InvariantUniq M
M' = M @ [(literal, True)]
\<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>M' = M @ [(literal, True)]\<close> \<open>literal' el elements M'\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(literal, True)]
literal' el elements M'
\<not> literal' el elements M
[PROOF STEP]
have "literal = literal'"
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(literal, True)]
literal' el elements M'
\<not> literal' el elements M

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

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 @ [(literal, True)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(literal, True)]
literal = literal'
[PROOF STEP]
have "literal' el decisions M'"
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(literal, True)]
literal = literal'

goal (1 subgoal):
 1. literal' el decisions M'
[PROOF STEP]
using markedElementIsMarkedTrue[of "literal" "M'"]
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(literal, True)]
literal = literal'
(literal \<in> set (decisions M')) = ((literal, True) \<in> set M')

goal (1 subgoal):
 1. literal' el decisions M'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
literal' el decisions 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>\<not> literal' el decisions M'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> literal' el decisions M'
literal' el decisions M'
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<not> literal' el decisions M'
literal' el decisions M'

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

goal (1 subgoal):
 1. \<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:
False

goal (1 subgoal):
 1. \<exists>clause. formulaEntailsClause F clause \<and> isReason clause literal' (elements M')
[PROOF STEP]
by simp
[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>?literal'2 el elements M'; \<not> ?literal'2 el decisions M'\<rbrakk> \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause ?literal'2 (elements M')

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

goal (1 subgoal):
 1. InvariantReasonClauses F M'
[PROOF STEP]
unfolding InvariantReasonClauses_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?literal'2 el elements M'; \<not> ?literal'2 el decisions M'\<rbrakk> \<Longrightarrow> \<exists>clause. formulaEntailsClause F clause \<and> isReason clause ?literal'2 (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 auto
[PROOF STATE]
proof (state)
this:
InvariantReasonClauses F M'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantCFalseAfterDecide:
  fixes conflictFlag::bool and M::LiteralTrail and C::Clause
  assumes "InvariantCFalse conflictFlag M C" and "M' = M @ [(literal, True)]"
  shows "InvariantCFalse conflictFlag M' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantCFalse conflictFlag M' C
[PROOF STEP]
unfolding InvariantCFalse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflictFlag \<longrightarrow> clauseFalse C (elements M')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C (elements M')
[PROOF STEP]
assume "conflictFlag"
[PROOF STATE]
proof (state)
this:
conflictFlag

goal (1 subgoal):
 1. conflictFlag \<Longrightarrow> clauseFalse C (elements M')
[PROOF STEP]
show "clauseFalse C (elements M')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clauseFalse C (elements M')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clauseFalse C (elements M')
[PROOF STEP]
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. clauseFalse C (elements M')
[PROOF STEP]
with \<open>conflictFlag\<close>
[PROOF STATE]
proof (chain)
picking this:
conflictFlag
conflictFlag \<longrightarrow> clauseFalse C (elements M)
[PROOF STEP]
have "clauseFalse C (elements M)"
[PROOF STATE]
proof (prove)
using this:
conflictFlag
conflictFlag \<longrightarrow> clauseFalse C (elements M)

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

goal (1 subgoal):
 1. clauseFalse C (elements M')
[PROOF STEP]
with \<open>M' = M @ [(literal, True)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(literal, True)]
clauseFalse C (elements M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(literal, True)]
clauseFalse C (elements M)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
clauseFalse C (elements M')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsHoldsForUnitLiteral:
  fixes M :: LiteralTrail and F :: Formula and uClause :: Clause and uLiteral :: Literal
  assumes "InvariantImpliedLiterals F M" and
  "formulaEntailsClause F uClause" and "isUnitClause uClause uLiteral (elements M)" and
  "M' = M @ [(uLiteral, False)]"
  shows "formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
have "decisionsTo uLiteral M' = decisions M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decisionsTo uLiteral M' = decisions M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decisionsTo uLiteral M' = decisions 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> uLiteral el (elements M)"
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause uLiteral (elements M)

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

goal (1 subgoal):
 1. decisionsTo uLiteral M' = decisions M
[PROOF STEP]
with \<open>M' = M @ [(uLiteral, False)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(uLiteral, False)]
\<not> uLiteral el elements M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(uLiteral, False)]
\<not> uLiteral el elements M

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
decisionsTo uLiteral M' = decisions M

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
decisionsTo uLiteral M' = decisions M

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
from \<open>formulaEntailsClause F uClause\<close> \<open>isUnitClause uClause uLiteral (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (elements M)) uLiteral"
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (elements M)) uLiteral
[PROOF STEP]
using unitLiteralIsEntailed [of "uClause" "uLiteral" "elements M" "F"]
[PROOF STATE]
proof (prove)
using this:
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
\<lbrakk>isUnitClause uClause uLiteral (elements M); formulaEntailsClause F uClause\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (F @ val2form (elements M)) uLiteral

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

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
with \<open>InvariantImpliedLiterals F M\<close>
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
formulaEntailsLiteral (F @ val2form (elements M)) uLiteral
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisions M)) uLiteral"
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
formulaEntailsLiteral (F @ val2form (elements M)) uLiteral

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisions M)) uLiteral
[PROOF STEP]
by (simp add: InvariantImpliedLiteralsAndElementsEntailLiteralThenDecisionsEntailLiteral)
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisions M)) uLiteral

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
decisionsTo uLiteral M' = decisions M
formulaEntailsLiteral (F @ val2form (decisions M)) uLiteral
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
decisionsTo uLiteral M' = decisions M
formulaEntailsLiteral (F @ val2form (decisions M)) uLiteral

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantImpliedLiteralsAfterUnitPropagate:
  fixes M :: LiteralTrail and F :: Formula and uClause :: Clause and uLiteral :: Literal
  assumes "InvariantImpliedLiterals F M" and
  "formulaEntailsClause F uClause" and "isUnitClause uClause uLiteral (elements M)" and
  "M' = M @ [(uLiteral, 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]
{
[PROOF STATE]
proof (state)
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]
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 M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
 2. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l el elements M

goal (2 subgoals):
 1. l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
 2. \<not> l el elements 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]
by (simp add:InvariantImpliedLiterals_def)
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l M)) l

goal (2 subgoals):
 1. l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
 2. \<not> l el elements 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 M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
 2. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
from \<open>M' = M @ [(uLiteral, False)]\<close>
[PROOF STATE]
proof (chain)
picking this:
M' = M @ [(uLiteral, False)]
[PROOF STEP]
have "(isPrefix M M')"
[PROOF STATE]
proof (prove)
using this:
M' = M @ [(uLiteral, False)]

goal (1 subgoal):
 1. isPrefix M M'
[PROOF STEP]
by (simp add:isPrefix_def)
[PROOF STATE]
proof (state)
this:
isPrefix M M'

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

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

goal (2 subgoals):
 1. l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
 2. \<not> l el elements 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 simp
[PROOF STATE]
proof (state)
this:
formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l

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

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

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

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

goal (1 subgoal):
 1. \<not> l el elements M \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo l M')) l
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
InvariantImpliedLiterals F M
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
M' = M @ [(uLiteral, False)]
[PROOF STEP]
have "formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral"
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
M' = M @ [(uLiteral, False)]

goal (1 subgoal):
 1. formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral
[PROOF STEP]
using InvariantImpliedLiteralsHoldsForUnitLiteral [of "F" "M" "uClause" "uLiteral" "M'"]
[PROOF STATE]
proof (prove)
using this:
InvariantImpliedLiterals F M
formulaEntailsClause F uClause
isUnitClause uClause uLiteral (elements M)
M' = M @ [(uLiteral, False)]
\<lbrakk>InvariantImpliedLiterals F M; formulaEntailsClause F uClause; isUnitClause uClause uLiteral (elements M); M' = M @ [(uLiteral, False)]\<rbrakk> \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo uLiteral M')) uLiteral

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

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

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:
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:
?l2 el elements M' \<Longrightarrow> formulaEntailsLiteral (F @ val2form (decisionsTo ?l2 M')) ?l2

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantVarsMAfterUnitPropagate:
  fixes F :: Formula and F0 :: Formula and M :: LiteralTrail and uClause :: Clause and uLiteral :: Literal and M' :: LiteralTrail
  assumes "InvariantVarsM M F0 Vbl" and
  "var uLiteral \<in> vars F0 \<union> Vbl" and
  "M' = M @ [(uLiteral, 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]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vars (elements M) \<subseteq> vars F0 \<union> Vbl

goal (1 subgoal):
 1. InvariantVarsM M' F0 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]
using \<open>var uLiteral \<in> vars F0 \<union> Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
vars (elements M) \<subseteq> vars F0 \<union> Vbl
var uLiteral \<in> vars F0 \<union> Vbl

goal (1 subgoal):
 1. vars (elements M') \<subseteq> vars F0 \<union> Vbl
[PROOF STEP]
using \<open>M' = M @ [(uLiteral, False)]\<close>
      varsAppendClauses [of "elements M" "[uLiteral]"]
[PROOF STATE]
proof (prove)
using this:
vars (elements M) \<subseteq> vars F0 \<union> Vbl
var uLiteral \<in> vars F0 \<union> Vbl
M' = M @ [(uLiteral, False)]
vars (elements M @ [uLiteral]) = vars (elements M) \<union> vars [uLiteral]

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