[STATEMENT]
theorem completenessForUNSAT: 
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes 
  "vars F0 \<subseteq> decisionVars" and

  "\<not> satisfiable F0" and

  "isInitialState state0 F0" and
  "(state0, state) \<in> transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"

  shows 
  "getConflictFlag state = True \<and> getC state = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
(************************************************************************)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
[PROOF STEP]
have *: "(getConflictFlag state = False \<and> 
               \<not>formulaFalse (getF state) (elements (getM state)) \<and> 
               vars (elements (getM state)) \<supseteq> decisionVars) \<or> 
           (getConflictFlag state = True \<and> 
               getC state = [])"
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars

goal (1 subgoal):
 1. getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
using finalStateCharacterization[of "state0" "F0" "state" "decisionVars"]
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
\<lbrakk>isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; isFinalState state F0 decisionVars\<rbrakk> \<Longrightarrow> getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
assume "\<not> getConflictFlag state = True"
[PROOF STATE]
proof (state)
this:
getConflictFlag state \<noteq> True

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True
[PROOF STEP]
have "getConflictFlag state = False \<and> \<not>formulaFalse (getF state) (elements (getM state)) \<and> vars (elements (getM state)) \<supseteq> decisionVars"
[PROOF STATE]
proof (prove)
using this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True

goal (1 subgoal):
 1. getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
[PROOF STEP]
have "satisfiable F0"
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))

goal (1 subgoal):
 1. satisfiable F0
[PROOF STEP]
using soundnessForSAT[of "F0" "decisionVars" "state0" "state"]
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
\<lbrakk>vars F0 \<subseteq> decisionVars; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; getConflictFlag state = False; \<not> formulaFalse (getF state) (elements (getM state)); decisionVars \<subseteq> vars (elements (getM state))\<rbrakk> \<Longrightarrow> model (elements (getM state)) F0

goal (1 subgoal):
 1. satisfiable F0
[PROOF STEP]
unfolding satisfiable_def
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<nexists>valuation. model valuation F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
\<lbrakk>vars F0 \<subseteq> decisionVars; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; getConflictFlag state = False; \<not> formulaFalse (getF state) (elements (getM state)); decisionVars \<subseteq> vars (elements (getM state))\<rbrakk> \<Longrightarrow> model (elements (getM state)) F0

goal (1 subgoal):
 1. \<exists>valuation. model valuation F0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
satisfiable F0

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with \<open>\<not> satisfiable F0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> satisfiable F0
satisfiable F0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<not> satisfiable F0
satisfiable F0

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

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
getConflictFlag state \<noteq> True \<Longrightarrow> False

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True \<Longrightarrow> False

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getConflictFlag state = True \<and> getC state = []

goal:
No subgoals!
[PROOF STEP]
qed