[STATEMENT]
lemma wf_implies_termi_reach:
assumes wf: "wf {(c2,c1). \<Gamma> \<turnstile> (cs,css,s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma> \<turnstile> c1 \<rightarrow> c2}"
shows "\<And>cs1 css1 s1. \<lbrakk>\<Gamma> \<turnstile> (cs,css,s) \<rightarrow>\<^sup>* c1;  c1=(cs1,css1,s1)\<rbrakk>\<Longrightarrow> \<Gamma>\<turnstile>cs1,css1\<Down>s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs1 css1 s1. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1; c1 = (cs1, css1, s1)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}

goal (1 subgoal):
 1. \<And>cs1 css1 s1. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1; c1 = (cs1, css1, s1)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
proof (induct c1, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x cs1 css1 s1. \<lbrakk>\<And>y cs1a css1a s1a. \<lbrakk>\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs1a, css1a, s1a); \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1a, css1a, s1a); y = (cs1a, css1a, s1a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1a,css1a \<Down> s1a; \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1); x = (cs1, css1, s1); wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
fix cs1 css1 s1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x cs1 css1 s1. \<lbrakk>\<And>y cs1a css1a s1a. \<lbrakk>\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs1a, css1a, s1a); \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1a, css1a, s1a); y = (cs1a, css1a, s1a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1a,css1a \<Down> s1a; \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1); x = (cs1, css1, s1); wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
assume reach: "\<Gamma>\<turnstile>(cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1)"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1)

goal (1 subgoal):
 1. \<And>x cs1 css1 s1. \<lbrakk>\<And>y cs1a css1a s1a. \<lbrakk>\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs1a, css1a, s1a); \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1a, css1a, s1a); y = (cs1a, css1a, s1a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1a,css1a \<Down> s1a; \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1); x = (cs1, css1, s1); wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
assume hyp_raw: "\<And>y cs2 css2 s2. \<lbrakk>\<Gamma> \<turnstile> (cs1,css1,s1) \<rightarrow> (cs2,css2,s2);
                 \<Gamma> \<turnstile> (cs,css,s) \<rightarrow>\<^sup>* (cs2,css2,s2); y=(cs2,css2,s2)\<rbrakk> \<Longrightarrow>
                 \<Gamma>\<turnstile>cs2,css2\<Down>s2"
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (?cs2.0, ?css2.0, ?s2.0); \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (?cs2.0, ?css2.0, ?s2.0); ?y = (?cs2.0, ?css2.0, ?s2.0)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>?cs2.0,?css2.0 \<Down> ?s2.0

goal (1 subgoal):
 1. \<And>x cs1 css1 s1. \<lbrakk>\<And>y cs1a css1a s1a. \<lbrakk>\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs1a, css1a, s1a); \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1a, css1a, s1a); y = (cs1a, css1a, s1a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1a,css1a \<Down> s1a; \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1); x = (cs1, css1, s1); wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
have hyp: "\<And>cs2 css2 s2. \<lbrakk>\<Gamma> \<turnstile> (cs1,css1,s1) \<rightarrow> (cs2,css2,s2)\<rbrakk> \<Longrightarrow>
                 \<Gamma>\<turnstile>cs2,css2\<Down>s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> \<Gamma>\<turnstile>cs2,css2 \<Down> s2
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> \<Gamma>\<turnstile>cs2,css2 \<Down> s2
[PROOF STEP]
apply (rule hyp_raw)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2)
 2. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs2, css2, s2)
 3. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> ?y cs2 css2 s2 = (cs2, css2, s2)
[PROOF STEP]
apply   assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs2, css2, s2)
 2. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> ?y cs2 css2 s2 = (cs2, css2, s2)
[PROOF STEP]
using reach
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1)

goal (2 subgoals):
 1. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs2, css2, s2)
 2. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> ?y cs2 css2 s2 = (cs2, css2, s2)
[PROOF STEP]
apply  simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs2 css2 s2. \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs2, css2, s2) \<Longrightarrow> ?y cs2 css2 s2 = (cs2, css2, s2)
[PROOF STEP]
apply (rule refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (?cs2.0, ?css2.0, ?s2.0) \<Longrightarrow> \<Gamma>\<turnstile>?cs2.0,?css2.0 \<Down> ?s2.0

goal (1 subgoal):
 1. \<And>x cs1 css1 s1. \<lbrakk>\<And>y cs1a css1a s1a. \<lbrakk>\<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs1a, css1a, s1a); \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1a, css1a, s1a); y = (cs1a, css1a, s1a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1a,css1a \<Down> s1a; \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs1, css1, s1); x = (cs1, css1, s1); wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
show "\<Gamma>\<turnstile>cs1,css1\<Down>s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
proof (cases s1)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. s1 = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>x2. s1 = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 3. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 4. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Normal s1')
[PROOF STATE]
proof (state)
this:
s1 = Normal s1'

goal (4 subgoals):
 1. \<And>x1. s1 = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>x2. s1 = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 3. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 4. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
proof (cases cs1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs1 = []

goal (2 subgoals):
 1. cs1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
note cs1_Nil = this
[PROOF STATE]
proof (state)
this:
cs1 = []

goal (2 subgoals):
 1. cs1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
proof (cases css1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. css1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
css1 = []

goal (2 subgoals):
 1. css1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
with cs1_Nil
[PROOF STATE]
proof (chain)
picking this:
cs1 = []
css1 = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = []
css1 = []

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by (auto intro: terminatess.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Cons nrms_abrs css1')
[PROOF STATE]
proof (state)
this:
css1 = nrms_abrs # css1'

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
css1 = nrms_abrs # css1'
[PROOF STEP]
obtain nrms abrs where nrms_abrs: "nrms_abrs=(nrms,abrs)"
[PROOF STATE]
proof (prove)
using this:
css1 = nrms_abrs # css1'

goal (1 subgoal):
 1. (\<And>nrms abrs. nrms_abrs = (nrms, abrs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "nrms_abrs")
[PROOF STATE]
proof (state)
this:
nrms_abrs = (nrms, abrs)

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
have "\<Gamma> \<turnstile> ([],(nrms,abrs)#css1',Normal s1') \<rightarrow> (nrms,css1',Normal s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (nrms, abrs) # css1', Normal s1') \<rightarrow> (nrms, css1', Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (nrms, abrs) # css1', Normal s1') \<rightarrow> (nrms, css1', Normal s1')

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
from hyp [simplified cs1_Nil Cons nrms_abrs Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>nrms,css1' \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>nrms,css1'\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>nrms,css1' \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>nrms,css1' \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms,css1' \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
from ExitBlockNormal [OF this] cs1_Nil Cons nrms_abrs Normal
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>[],(nrms, ?abrs) # css1' \<Down> Normal s1'
cs1 = []
css1 = nrms_abrs # css1'
nrms_abrs = (nrms, abrs)
s1 = Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[],(nrms, ?abrs) # css1' \<Down> Normal s1'
cs1 = []
css1 = nrms_abrs # css1'
nrms_abrs = (nrms, abrs)
s1 = Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Cons c1 cs1')
[PROOF STATE]
proof (state)
this:
cs1 = c1 # cs1'

goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
have "\<Gamma>\<turnstile>c1#cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
proof (cases c1)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. c1 = Skip \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
A total of 11 subgoals...
[PROOF STEP]
case Skip
[PROOF STATE]
proof (state)
this:
c1 = Skip

goal (11 subgoals):
 1. c1 = Skip \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
A total of 11 subgoals...
[PROOF STEP]
have "\<Gamma> \<turnstile> (Skip#cs1',css1,Normal s1') \<rightarrow> (cs1',css1,Normal s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Skip # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Skip # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal s1')

goal (11 subgoals):
 1. c1 = Skip \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
A total of 11 subgoals...
[PROOF STEP]
from hyp [simplified Cons Skip Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'

goal (11 subgoals):
 1. c1 = Skip \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
A total of 11 subgoals...
[PROOF STEP]
with Normal Skip
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Skip
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Skip
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (auto intro: terminatess.intros terminates.intros
                  elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (10 subgoals):
 1. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Basic f)
[PROOF STATE]
proof (state)
this:
c1 = Basic f

goal (10 subgoals):
 1. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma> \<turnstile> (Basic f#cs1',css1,Normal s1') \<rightarrow> (cs1',css1,Normal (f s1'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Basic f # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal (f s1'))
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Basic f # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal (f s1'))

goal (10 subgoals):
 1. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Basic Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal (f s1')
[PROOF STEP]
have "\<Gamma>\<turnstile>cs1',css1\<Down>Normal (f s1')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal (f s1')

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1',css1 \<Down> Normal (f s1')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal (f s1')

goal (10 subgoals):
 1. \<And>x2. c1 = Basic x2 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 10. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Basic
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Basic f
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal (f s1')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Basic f
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal (f s1')

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (auto intro: terminatess.intros terminates.intros
                  elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (9 subgoals):
 1. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Spec r)
[PROOF STATE]
proof (state)
this:
c1 = Spec r

goal (9 subgoals):
 1. \<And>x3. c1 = Spec x3 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 9. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Spec r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Spec r

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s1 = Normal s1'; c1 = Spec r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>Spec r # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
apply (rule terminatess.Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s1 = Normal s1'; c1 = Spec r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>Spec r \<down> Normal s1'
 2. \<lbrakk>s1 = Normal s1'; c1 = Spec r\<rbrakk> \<Longrightarrow> \<forall>t. \<Gamma>\<turnstile> \<langle>Spec r,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply  (fastforce intro: terminates.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s1 = Normal s1'; c1 = Spec r\<rbrakk> \<Longrightarrow> \<forall>t. \<Gamma>\<turnstile> \<langle>Spec r,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s1 = Normal s1'; c1 = Spec r; \<Gamma>\<turnstile> \<langle>Spec r,Normal s1'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (erule exec_Normal_elim_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t ta. \<lbrakk>s1 = Normal s1'; c1 = Spec r; t = Normal ta; (s1', ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
 2. \<And>t. \<lbrakk>s1 = Normal s1'; c1 = Spec r; t = Stuck; \<forall>t. (s1', t) \<notin> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>s1 = Normal s1'; c1 = Spec r; (s1', ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> Normal ta
 2. \<And>t. \<lbrakk>s1 = Normal s1'; c1 = Spec r; t = Stuck; \<forall>t. (s1', t) \<notin> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply  (rule hyp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>s1 = Normal s1'; c1 = Spec r; (s1', ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs1, css1, s1) \<rightarrow> (cs1', css1, Normal ta)
 2. \<And>t. \<lbrakk>s1 = Normal s1'; c1 = Spec r; t = Stuck; \<forall>t. (s1', t) \<notin> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply  (fastforce intro: step.intros simp add: Cons Spec Normal )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s1 = Normal s1'; c1 = Spec r; t = Stuck; \<forall>t. (s1', t) \<notin> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (fastforce intro: terminatess_Stuck)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (8 subgoals):
 1. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Seq c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
c1 = Seq c\<^sub>1 c\<^sub>2

goal (8 subgoals):
 1. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2#cs1',css1,Normal s1') \<rightarrow> (c\<^sub>1#c\<^sub>2#cs1',css1,Normal s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> (c\<^sub>1 # c\<^sub>2 # cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> (c\<^sub>1 # c\<^sub>2 # cs1', css1, Normal s1')

goal (8 subgoals):
 1. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Seq Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1 \<Down> Normal s1'

goal (8 subgoals):
 1. \<And>x41 x42. c1 = Seq x41 x42 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 8. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Seq
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Seq c\<^sub>1 c\<^sub>2
\<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Seq c\<^sub>1 c\<^sub>2
\<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros
                   elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (7 subgoals):
 1. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Cond b c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
c1 = Cond b c\<^sub>1 c\<^sub>2

goal (7 subgoals):
 1. \<And>x51 x52 x53. c1 = Cond x51 x52 x53 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 7. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
proof (cases "s1' \<in> b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s1' \<in> b

goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
hence "\<Gamma>\<turnstile>(Cond b c\<^sub>1 c\<^sub>2#cs1',css1,Normal s1') \<rightarrow> (c\<^sub>1#cs1',css1,Normal s1')"
[PROOF STATE]
proof (prove)
using this:
s1' \<in> b

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> (c\<^sub>1 # cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> (c\<^sub>1 # cs1', css1, Normal s1')

goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Cond Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c\<^sub>1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>c\<^sub>1 # cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c\<^sub>1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c\<^sub>1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c\<^sub>1 # cs1',css1 \<Down> Normal s1'

goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Cond True
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Cond b c\<^sub>1 c\<^sub>2
s1' \<in> b
\<Gamma>\<turnstile>c\<^sub>1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Cond b c\<^sub>1 c\<^sub>2
s1' \<in> b
\<Gamma>\<turnstile>c\<^sub>1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros
              elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s1' \<notin> b

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
hence "\<Gamma>\<turnstile>(Cond b c\<^sub>1 c\<^sub>2#cs1',css1,Normal s1') \<rightarrow> (c\<^sub>2#cs1',css1,Normal s1')"
[PROOF STATE]
proof (prove)
using this:
s1' \<notin> b

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> (c\<^sub>2 # cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> (c\<^sub>2 # cs1', css1, Normal s1')

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Cond Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c\<^sub>2 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>c\<^sub>2 # cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c\<^sub>2 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c\<^sub>2 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c\<^sub>2 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Cond False
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Cond b c\<^sub>1 c\<^sub>2
s1' \<notin> b
\<Gamma>\<turnstile>c\<^sub>2 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Cond b c\<^sub>1 c\<^sub>2
s1' \<notin> b
\<Gamma>\<turnstile>c\<^sub>2 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros
              elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (6 subgoals):
 1. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (While b c')
[PROOF STATE]
proof (state)
this:
c1 = While b c'

goal (6 subgoals):
 1. \<And>x61 x62. c1 = While x61 x62 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 6. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
proof (cases "s1' \<in> b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s1' \<in> b

goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1' \<in> b
[PROOF STEP]
have "\<Gamma>\<turnstile>(While b c' # cs1', css1, Normal s1') \<rightarrow>
                       (c' # While b c' # cs1', css1, Normal s1')"
[PROOF STATE]
proof (prove)
using this:
s1' \<in> b

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (While b c' # cs1', css1, Normal s1') \<rightarrow> (c' # While b c' # cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (While b c' # cs1', css1, Normal s1') \<rightarrow> (c' # While b c' # cs1', css1, Normal s1')

goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons While Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c' # While b c' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>c' # While b c' # cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c' # While b c' # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' # While b c' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c' # While b c' # cs1',css1 \<Down> Normal s1'

goal (2 subgoals):
 1. s1' \<in> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Cons While True Normal
[PROOF STATE]
proof (chain)
picking this:
cs1 = c1 # cs1'
c1 = While b c'
s1' \<in> b
s1 = Normal s1'
\<Gamma>\<turnstile>c' # While b c' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = c1 # cs1'
c1 = While b c'
s1' \<in> b
s1 = Normal s1'
\<Gamma>\<turnstile>c' # While b c' # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s1' \<notin> b

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1' \<notin> b
[PROOF STEP]
have "\<Gamma>\<turnstile>(While b c' # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal s1')"
[PROOF STATE]
proof (prove)
using this:
s1' \<notin> b

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (While b c' # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (While b c' # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Normal s1')

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons While Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. s1' \<notin> b \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Cons While False Normal
[PROOF STATE]
proof (chain)
picking this:
cs1 = c1 # cs1'
c1 = While b c'
s1' \<notin> b
s1 = Normal s1'
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = c1 # cs1'
c1 = While b c'
s1' \<notin> b
s1 = Normal s1'
\<Gamma>\<turnstile>cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (5 subgoals):
 1. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Call p)
[PROOF STATE]
proof (state)
this:
c1 = Call p

goal (5 subgoals):
 1. \<And>x7. c1 = Call x7 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 5. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
proof (cases "\<Gamma> p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
\<Gamma> p = None

goal (2 subgoals):
 1. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Call Normal
[PROOF STATE]
proof (chain)
picking this:
c1 = Call p
s1 = Normal s1'
\<Gamma> p = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c1 = Call p
s1 = Normal s1'
\<Gamma> p = None

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros terminatess_Stuck
                 elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Some bdy)
[PROOF STATE]
proof (state)
this:
\<Gamma> p = Some bdy

goal (1 subgoal):
 1. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> p = Some bdy
[PROOF STEP]
have "\<Gamma> \<turnstile> (Call p#cs1',css1,Normal s1') \<rightarrow>
                    ([bdy],(cs1',Throw#cs1')#css1,Normal s1')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> p = Some bdy

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs1', css1, Normal s1') \<rightarrow> ([bdy], (cs1', Throw # cs1') # css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs1', css1, Normal s1') \<rightarrow> ([bdy], (cs1', Throw # cs1') # css1, Normal s1')

goal (1 subgoal):
 1. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Call Normal Some, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>a. \<Gamma> p = Some a \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Some Call Normal
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> p = Some bdy
c1 = Call p
s1 = Normal s1'
\<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> p = Some bdy
c1 = Call p
s1 = Normal s1'
\<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>Call p # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
apply (rule terminatess.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>Call p \<down> Normal s1'
 2. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'\<rbrakk> \<Longrightarrow> \<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (blast elim: terminatess_elim_cases intro: terminates.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'\<rbrakk> \<Longrightarrow> \<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>[bdy],(cs1', Throw # cs1') # css1 \<Down> Normal s1'; \<Gamma>\<turnstile> \<langle>Call p,Normal s1'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (erule terminatess_elim_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile> \<langle>Call p,Normal s1'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<forall>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (erule exec_Normal_elim_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t bdya. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<forall>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
 2. \<And>t. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<forall>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; t = Stuck; \<Gamma> p = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<forall>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; t = Stuck; \<Gamma> p = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
 2. \<And>t bdya. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<forall>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply  simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t bdya. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<forall>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (erule_tac x=t in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t bdya. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (case_tac t)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t bdya x1. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; t = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
 2. \<And>t bdya x2. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; t = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
 3. \<And>t bdya x3. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; t = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
 4. \<And>t bdya. \<lbrakk>\<Gamma> p = Some bdy; c1 = Call p; s1 = Normal s1'; \<Gamma>\<turnstile>bdy \<down> Normal s1'; \<Gamma> p = Some bdya; \<Gamma>\<turnstile> \<langle>bdya,Normal s1'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>bdy,Normal s1'\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>[],(cs1', Throw # cs1') # css1 \<Down> t; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs1',css1 \<Down> t
[PROOF STEP]
apply (auto intro: terminatess_Stuck terminatess_Fault exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (4 subgoals):
 1. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (DynCom c')
[PROOF STATE]
proof (state)
this:
c1 = DynCom c'

goal (4 subgoals):
 1. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma> \<turnstile> (DynCom c'#cs1',css1,Normal s1') \<rightarrow> (c' s1'#cs1',css1,Normal s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (DynCom c' # cs1', css1, Normal s1') \<rightarrow> (c' s1' # cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (DynCom c' # cs1', css1, Normal s1') \<rightarrow> (c' s1' # cs1', css1, Normal s1')

goal (4 subgoals):
 1. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons DynCom Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c' s1' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>c' s1'#cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c' s1' # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' s1' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c' s1' # cs1',css1 \<Down> Normal s1'

goal (4 subgoals):
 1. \<And>x8. c1 = DynCom x8 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 4. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal DynCom
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = DynCom c'
\<Gamma>\<turnstile>c' s1' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = DynCom c'
\<Gamma>\<turnstile>c' s1' # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (3 subgoals):
 1. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Guard f g c')
[PROOF STATE]
proof (state)
this:
c1 = Guard f g c'

goal (3 subgoals):
 1. \<And>x91 x92 x93. c1 = Guard x91 x92 x93 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 3. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
proof (cases "s1' \<in> g")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s1' \<in> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s1' \<in> g

goal (2 subgoals):
 1. s1' \<in> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1' \<in> g
[PROOF STEP]
have "\<Gamma> \<turnstile> (Guard f g c'#cs1',css1,Normal s1') \<rightarrow> (c'#cs1',css1,Normal s1')"
[PROOF STATE]
proof (prove)
using this:
s1' \<in> g

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Guard f g c' # cs1', css1, Normal s1') \<rightarrow> (c' # cs1', css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Guard f g c' # cs1', css1, Normal s1') \<rightarrow> (c' # cs1', css1, Normal s1')

goal (2 subgoals):
 1. s1' \<in> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Guard Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>c'#cs1',css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c' # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c' # cs1',css1 \<Down> Normal s1'

goal (2 subgoals):
 1. s1' \<in> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Guard True
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Guard f g c'
s1' \<in> g
\<Gamma>\<turnstile>c' # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Guard f g c'
s1' \<in> g
\<Gamma>\<turnstile>c' # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s1' \<notin> g

goal (1 subgoal):
 1. s1' \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Guard Normal
[PROOF STATE]
proof (chain)
picking this:
c1 = Guard f g c'
s1 = Normal s1'
s1' \<notin> g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c1 = Guard f g c'
s1 = Normal s1'
s1' \<notin> g

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminatess_Fault
                                terminates.intros
                 elim:  exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (2 subgoals):
 1. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case Throw
[PROOF STATE]
proof (state)
this:
c1 = Throw

goal (2 subgoals):
 1. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma> \<turnstile> (Throw#cs1',css1,Normal s1') \<rightarrow> (cs1',css1,Abrupt s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Throw # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Abrupt s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Throw # cs1', css1, Normal s1') \<rightarrow> (cs1', css1, Abrupt s1')

goal (2 subgoals):
 1. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Throw Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>cs1',css1\<Down>Abrupt s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'

goal (2 subgoals):
 1. c1 = Throw \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
 2. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Throw
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Throw
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Throw
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (auto intro: terminatess.intros terminates.intros
                  elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
case (Catch c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
c1 = Catch c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2#cs1',css1,Normal s1') \<rightarrow>
                  ([c\<^sub>1], (cs1',c\<^sub>2#cs1')# css1,Normal s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> ([c\<^sub>1], (cs1', c\<^sub>2 # cs1') # css1, Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs1', css1, Normal s1') \<rightarrow> ([c\<^sub>1], (cs1', c\<^sub>2 # cs1') # css1, Normal s1')

goal (1 subgoal):
 1. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
from hyp [simplified Cons Catch Normal, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1 \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1 \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>x111 x112. c1 = Catch x111 x112 \<Longrightarrow> \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
with Normal Catch
[PROOF STATE]
proof (chain)
picking this:
s1 = Normal s1'
c1 = Catch c\<^sub>1 c\<^sub>2
\<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Normal s1'
c1 = Catch c\<^sub>1 c\<^sub>2
\<Gamma>\<turnstile>[c\<^sub>1],(cs1', c\<^sub>2 # cs1') # css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
with Cons Normal
[PROOF STATE]
proof (chain)
picking this:
cs1 = c1 # cs1'
s1 = Normal s1'
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = c1 # cs1'
s1 = Normal s1'
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (3 subgoals):
 1. \<And>x2. s1 = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 3. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. s1 = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 3. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Abrupt s1')
[PROOF STATE]
proof (state)
this:
s1 = Abrupt s1'

goal (3 subgoals):
 1. \<And>x2. s1 = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 3. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
proof (cases cs1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs1 = []

goal (2 subgoals):
 1. cs1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
note cs1_Nil = this
[PROOF STATE]
proof (state)
this:
cs1 = []

goal (2 subgoals):
 1. cs1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
proof (cases css1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. css1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
css1 = []

goal (2 subgoals):
 1. css1 = [] \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
with cs1_Nil
[PROOF STATE]
proof (chain)
picking this:
cs1 = []
css1 = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = []
css1 = []

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by (auto intro: terminatess.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Cons nrms_abrs css1')
[PROOF STATE]
proof (state)
this:
css1 = nrms_abrs # css1'

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
css1 = nrms_abrs # css1'
[PROOF STEP]
obtain nrms abrs where nrms_abrs: "nrms_abrs=(nrms,abrs)"
[PROOF STATE]
proof (prove)
using this:
css1 = nrms_abrs # css1'

goal (1 subgoal):
 1. (\<And>nrms abrs. nrms_abrs = (nrms, abrs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "nrms_abrs")
[PROOF STATE]
proof (state)
this:
nrms_abrs = (nrms, abrs)

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
have "\<Gamma> \<turnstile> ([],(nrms,abrs)#css1',Abrupt s1') \<rightarrow> (abrs,css1',Normal s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (nrms, abrs) # css1', Abrupt s1') \<rightarrow> (abrs, css1', Normal s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (nrms, abrs) # css1', Abrupt s1') \<rightarrow> (abrs, css1', Normal s1')

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
from hyp [simplified cs1_Nil Cons nrms_abrs Abrupt, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>abrs,css1' \<Down> Normal s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>abrs,css1'\<Down>Normal s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>abrs,css1' \<Down> Normal s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>abrs,css1' \<Down> Normal s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>abrs,css1' \<Down> Normal s1'

goal (1 subgoal):
 1. \<And>a list. css1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
from ExitBlockAbrupt [OF this] cs1_Nil Cons nrms_abrs Abrupt
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>[],(?nrms, abrs) # css1' \<Down> Abrupt s1'
cs1 = []
css1 = nrms_abrs # css1'
nrms_abrs = (nrms, abrs)
s1 = Abrupt s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[],(?nrms, abrs) # css1' \<Down> Abrupt s1'
cs1 = []
css1 = nrms_abrs # css1'
nrms_abrs = (nrms, abrs)
s1 = Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Cons c1 cs1')
[PROOF STATE]
proof (state)
this:
cs1 = c1 # cs1'

goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
have "\<Gamma>\<turnstile>c1#cs1',css1\<Down>Abrupt s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
have "\<Gamma> \<turnstile> (c1#cs1',css1,Abrupt s1') \<rightarrow> (cs1',css1,Abrupt s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c1 # cs1', css1, Abrupt s1') \<rightarrow> (cs1', css1, Abrupt s1')
[PROOF STEP]
by (rule step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c1 # cs1', css1, Abrupt s1') \<rightarrow> (cs1', css1, Abrupt s1')

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
from hyp [simplified Cons Abrupt, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
have "\<Gamma>\<turnstile>cs1',css1\<Down>Abrupt s1'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
with Cons Abrupt
[PROOF STATE]
proof (chain)
picking this:
cs1 = c1 # cs1'
s1 = Abrupt s1'
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = c1 # cs1'
s1 = Abrupt s1'
\<Gamma>\<turnstile>cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros exec.intros
                    elim: terminatess_elim_cases exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<And>a list. cs1 = a # list \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
with Cons Abrupt
[PROOF STATE]
proof (chain)
picking this:
cs1 = c1 # cs1'
s1 = Abrupt s1'
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs1 = c1 # cs1'
s1 = Abrupt s1'
\<Gamma>\<turnstile>c1 # cs1',css1 \<Down> Abrupt s1'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (2 subgoals):
 1. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case (Fault f)
[PROOF STATE]
proof (state)
this:
s1 = Fault f

goal (2 subgoals):
 1. \<And>x3. s1 = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
 2. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Fault f

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by (auto intro: terminatess_Fault)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal (1 subgoal):
 1. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
case Stuck
[PROOF STATE]
proof (state)
this:
s1 = Stuck

goal (1 subgoal):
 1. s1 = Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs1,css1 \<Down> s1
[PROOF STEP]
by (auto intro: terminatess_Stuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs1,css1 \<Down> s1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_inf_impl_terminatess:
  assumes not_inf: "\<not> inf \<Gamma> cs css s"
  shows "\<Gamma>\<turnstile>cs,css\<Down>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
from not_inf_implies_wf [OF not_inf]
[PROOF STATE]
proof (chain)
picking this:
wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}
[PROOF STEP]
have wf: "wf {(c2, c1). \<Gamma>\<turnstile>(cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile>c1 \<rightarrow> c2}"
[PROOF STATE]
proof (prove)
using this:
wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}

goal (1 subgoal):
 1. wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
by (rule wf_implies_termi_reach [OF wf]) auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_inf_impl_terminates:
  assumes not_inf: "\<not> inf \<Gamma> [c] [] s"
  shows "\<Gamma>\<turnstile>c\<down>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c \<down> s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c \<down> s
[PROOF STEP]
from not_inf_impl_terminatess [OF not_inf]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>[c],[] \<Down> s
[PROOF STEP]
have "\<Gamma>\<turnstile>[c],[]\<Down>s"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[c],[] \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[c],[] \<Down> s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[c],[] \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c \<down> s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[c],[] \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c \<down> s
[PROOF STEP]
by (auto elim: terminatess_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c \<down> s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem terminatess_iff_not_inf:
  "\<Gamma>\<turnstile>cs,css\<Down>s = (\<not> inf \<Gamma> cs css s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s = (\<not> AlternativeSmallStep.inf \<Gamma> cs css s)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> cs css s
 2. \<not> AlternativeSmallStep.inf \<Gamma> cs css s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
apply  (erule terminatess_impl_not_inf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> cs css s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
apply (erule not_inf_impl_terminatess)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ConseqMGT:
  assumes modif: "\<forall>Z::'a. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z::'a assn) c (Q' Z),(A' Z)"
  assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and>
                                            (\<forall>t. t \<in> A' s \<longrightarrow> t \<in> A)"
  shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A
[PROOF STEP]
using impl
[PROOF STATE]
proof (prove)
using this:
?s \<in> P \<Longrightarrow> ?s \<in> P' ?s \<and> (\<forall>t. t \<in> Q' ?s \<longrightarrow> t \<in> Q) \<and> (\<forall>t. t \<in> A' ?s \<longrightarrow> t \<in> A)

goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A
[PROOF STEP]
by - (rule conseq [OF modif],blast)


[STATEMENT]
lemma conseq_extract_state_indep_prop:
  assumes state_indep_prop:"\<forall>s \<in> P. R"
  assumes to_show: "R \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A
[PROOF STEP]
apply (rule Conseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P \<Longrightarrow> \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A
[PROOF STEP]
apply (rule_tac x="P" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P \<Longrightarrow> \<exists>Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q',A' \<and> s \<in> P \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A
[PROOF STEP]
apply (rule_tac x="Q" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P \<Longrightarrow> \<exists>A'. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A' \<and> s \<in> P \<and> Q \<subseteq> Q \<and> A' \<subseteq> A
[PROOF STEP]
apply (rule_tac x="A" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<and> s \<in> P \<and> Q \<subseteq> Q \<and> A \<subseteq> A
[PROOF STEP]
using state_indep_prop to_show
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>P. R
R \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A

goal (1 subgoal):
 1. \<And>s. s \<in> P \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<and> s \<in> P \<and> Q \<subseteq> Q \<and> A \<subseteq> A
[PROOF STEP]
by blast