[STATEMENT]
lemma wellFoundedLexLessState1:
assumes
  "finite Vbl"
shows
  "wf (lexLessState1 Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (lexLessState1 Vbl)
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessState1 Vbl \<longrightarrow> y \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessState1 Vbl \<longrightarrow> y \<notin> Q)
[PROOF STEP]
show "\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
fix Q :: "State set" and state :: State
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
assume "state \<in> Q"
[PROOF STATE]
proof (state)
this:
state \<in> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
let ?Q1 = "{M::LiteralTrail. \<exists> state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> (getM state) = M}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
have "\<exists> stateMin \<in> Q. (\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof (cases "?Q1 \<noteq> {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}
[PROOF STEP]
obtain M::LiteralTrail
          where "M \<in> ?Q1"
[PROOF STATE]
proof (prove)
using this:
{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

goal (1 subgoal):
 1. (\<And>M. M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
obtain MMin::LiteralTrail
          where "MMin \<in> ?Q1" "\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> ?Q1"
[PROOF STATE]
proof (prove)
using this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (\<And>MMin. \<lbrakk>MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfLexLessRestricted[of "Vbl"] \<open>finite Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
finite Vbl \<Longrightarrow> wf (lexLessRestricted Vbl)
finite Vbl

goal (1 subgoal):
 1. (\<And>MMin. \<lbrakk>MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
using this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
finite Vbl \<Longrightarrow> \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> y \<notin> Q)
finite Vbl

goal (1 subgoal):
 1. (\<And>MMin. \<lbrakk>MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>MMin. \<lbrakk>\<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = MMin; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> (\<forall>state. getSATFlag state = UNDEF \<longrightarrow> state \<in> Q \<longrightarrow> getM state \<noteq> M')\<rbrakk> \<Longrightarrow> thesis; \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> y \<notin> Q); finite Vbl\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule_tac x="?Q1" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>MMin. \<lbrakk>\<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = MMin; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> (\<forall>state. getSATFlag state = UNDEF \<longrightarrow> state \<in> Q \<longrightarrow> getM state \<noteq> M')\<rbrakk> \<Longrightarrow> thesis; \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M; finite Vbl; (\<exists>x. x \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}) \<longrightarrow> (\<exists>z\<in>{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}. \<forall>y. (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> y \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M})\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
from \<open>MMin \<in> ?Q1\<close>
[PROOF STATE]
proof (chain)
picking this:
MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
obtain stateMin
          where "stateMin \<in> Q" "(getM stateMin) = MMin" "getSATFlag stateMin = UNDEF"
[PROOF STATE]
proof (prove)
using this:
MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (\<And>stateMin. \<lbrakk>stateMin \<in> Q; getM stateMin = MMin; getSATFlag stateMin = UNDEF\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stateMin \<in> Q
getM stateMin = MMin
getSATFlag stateMin = UNDEF

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
have "\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
fix state'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
show "(state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
assume "(state', stateMin) \<in> lexLessState1 Vbl"
[PROOF STATE]
proof (state)
this:
(state', stateMin) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "getSATFlag state' = UNDEF" "(getM state', getM stateMin) \<in> lexLessRestricted Vbl"
[PROOF STATE]
proof (prove)
using this:
(state', stateMin) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. getSATFlag state' = UNDEF &&& (getM state', getM stateMin) \<in> lexLessRestricted Vbl
[PROOF STEP]
unfolding lexLessState1_def
[PROOF STATE]
proof (prove)
using this:
(state', stateMin) \<in> {(state1, state2). getSATFlag state1 = UNDEF \<and> getSATFlag state2 = UNDEF \<and> (getM state1, getM state2) \<in> lexLessRestricted Vbl}

goal (1 subgoal):
 1. getSATFlag state' = UNDEF &&& (getM state', getM stateMin) \<in> lexLessRestricted Vbl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "getM state' \<notin> ?Q1"
[PROOF STATE]
proof (prove)
using this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
using \<open>\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> ?Q1\<close>
[PROOF STATE]
proof (prove)
using this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl
\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
using \<open>(getM stateMin) = MMin\<close>
[PROOF STATE]
proof (prove)
using this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl
\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
getM stateMin = MMin

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
thus "state' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
using \<open>getSATFlag state' = UNDEF\<close>
[PROOF STATE]
proof (prove)
using this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
getSATFlag state' = UNDEF

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
using \<open>stateMin \<in> Q\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
stateMin \<in> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
have "\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
fix state'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
show "(state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
assume "(state', state) \<in> lexLessState1 Vbl"
[PROOF STATE]
proof (state)
this:
(state', state) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "getSATFlag state = UNDEF"
[PROOF STATE]
proof (prove)
using this:
(state', state) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. getSATFlag state = UNDEF
[PROOF STEP]
unfolding lexLessState1_def
[PROOF STATE]
proof (prove)
using this:
(state', state) \<in> {(state1, state2). getSATFlag state1 = UNDEF \<and> getSATFlag state2 = UNDEF \<and> (getM state1, getM state2) \<in> lexLessRestricted Vbl}

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

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "(getM state) \<in> ?Q1"
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF

goal (1 subgoal):
 1. getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
using \<open>state \<in> Q\<close>
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF
state \<in> Q

goal (1 subgoal):
 1. getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
\<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

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

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
thus "state' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
using \<open>state \<in> Q\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
state \<in> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?state2 \<in> ?Q2 \<Longrightarrow> \<exists>stateMin\<in>?Q2. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?state2 \<in> ?Q2 \<Longrightarrow> \<exists>stateMin\<in>?Q2. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed