[STATEMENT]
lemma exec_impl_steps:
  assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t"
  shows "\<And>cs css. \<Gamma>\<turnstile>(c#cs,css,s) \<rightarrow>\<^sup>* (cs,css,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (20 subgoals):
 1. \<And>s cs css. \<Gamma>\<turnstile> (Skip # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 2. \<And>s g c t f cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 4. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 5. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 6. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 7. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 20 subgoals...
[PROOF STEP]
case Skip
[PROOF STATE]
proof (state)
this:

goal (20 subgoals):
 1. \<And>s cs css. \<Gamma>\<turnstile> (Skip # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 2. \<And>s g c t f cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 4. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 5. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 6. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 7. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 20 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Skip # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal s_)
[PROOF STEP]
by (blast intro: step.Skip)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Skip # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal s_)

goal (19 subgoals):
 1. \<And>s g c t f cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 3. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 4. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 5. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 6. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 19 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (19 subgoals):
 1. \<And>s g c t f cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 3. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 4. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 5. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 6. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 19 subgoals...
[PROOF STEP]
case Guard
[PROOF STATE]
proof (state)
this:
s_ \<in> g_
\<Gamma>\<turnstile> \<langle>c_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (19 subgoals):
 1. \<And>s g c t f cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 3. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 4. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 5. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 6. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 19 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<in> g_
\<Gamma>\<turnstile> \<langle>c_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Guard f_ g_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)
[PROOF STEP]
by (blast intro: step.Guard rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Guard f_ g_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)

goal (18 subgoals):
 1. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 2. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 3. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 4. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 5. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
A total of 18 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 2. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 3. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 4. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 5. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
A total of 18 subgoals...
[PROOF STEP]
case GuardFault
[PROOF STATE]
proof (state)
this:
s_ \<notin> g_

goal (18 subgoals):
 1. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
 2. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 3. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 4. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 5. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
A total of 18 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<notin> g_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Guard f_ g_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Fault f_)
[PROOF STEP]
by (blast intro: step.GuardFault)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Guard f_ g_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Fault f_)

goal (17 subgoals):
 1. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 2. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 3. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 4. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 10. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 2. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 3. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 4. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 10. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 17 subgoals...
[PROOF STEP]
case FaultProp
[PROOF STATE]
proof (state)
this:

goal (17 subgoals):
 1. \<And>c f cs css. \<Gamma>\<turnstile> (c # cs, css, Fault f) \<rightarrow>\<^sup>* (cs, css, Fault f)
 2. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 3. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 4. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 10. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 17 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c_ # cs, css, Fault f_) \<rightarrow>\<^sup>* (cs, css, Fault f_)
[PROOF STEP]
by (blast intro: step.FaultProp)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c_ # cs, css, Fault f_) \<rightarrow>\<^sup>* (cs, css, Fault f_)

goal (16 subgoals):
 1. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 2. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 3. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 9. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 2. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 3. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 9. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
A total of 16 subgoals...
[PROOF STEP]
case Basic
[PROOF STATE]
proof (state)
this:

goal (16 subgoals):
 1. \<And>f s cs css. \<Gamma>\<turnstile> (Basic f # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal (f s))
 2. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 3. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 9. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
A total of 16 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Basic f_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal (f_ s_))
[PROOF STEP]
by (blast intro: step.Basic)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Basic f_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal (f_ s_))

goal (15 subgoals):
 1. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 2. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 8. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 10. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 2. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 8. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 10. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
A total of 15 subgoals...
[PROOF STEP]
case Spec
[PROOF STATE]
proof (state)
this:
(s_, t_) \<in> r_

goal (15 subgoals):
 1. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal t)
 2. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 8. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 10. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
A total of 15 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(s_, t_) \<in> r_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Spec r_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal t_)
[PROOF STEP]
by (blast intro: step.Spec)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Spec r_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal t_)

goal (14 subgoals):
 1. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 7. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 9. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 10. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 7. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 9. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 10. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 14 subgoals...
[PROOF STEP]
case SpecStuck
[PROOF STATE]
proof (state)
this:
\<forall>t. (s_, t) \<notin> r_

goal (14 subgoals):
 1. \<And>s r cs css. \<forall>t. (s, t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 7. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 9. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 10. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 14 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (s_, t) \<notin> r_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Spec r_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Stuck)
[PROOF STEP]
by (blast intro: step.SpecStuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Spec r_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Stuck)

goal (13 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 6. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 9. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 6. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 9. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
A total of 13 subgoals...
[PROOF STEP]
case Seq
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c\<^sub>1_,Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> (c\<^sub>1_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, s'_)
\<Gamma>\<turnstile> \<langle>c\<^sub>2_,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c\<^sub>2_ # ?cs, ?css, s'_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (13 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 6. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 9. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
A total of 13 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c\<^sub>1_,Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> (c\<^sub>1_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, s'_)
\<Gamma>\<turnstile> \<langle>c\<^sub>2_,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c\<^sub>2_ # ?cs, ?css, s'_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Seq c\<^sub>1_ c\<^sub>2_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)
[PROOF STEP]
by (blast intro: step.Seq rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq c\<^sub>1_ c\<^sub>2_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)

goal (12 subgoals):
 1. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 5. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 10. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 5. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 10. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
A total of 12 subgoals...
[PROOF STEP]
case CondTrue
[PROOF STATE]
proof (state)
this:
s_ \<in> b_
\<Gamma>\<turnstile> \<langle>c\<^sub>1_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c\<^sub>1_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (12 subgoals):
 1. \<And>s b c\<^sub>1 t c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 5. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 8. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 10. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
A total of 12 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<in> b_
\<Gamma>\<turnstile> \<langle>c\<^sub>1_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c\<^sub>1_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Cond b_ c\<^sub>1_ c\<^sub>2_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)
[PROOF STEP]
by (blast intro: step.CondTrue rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Cond b_ c\<^sub>1_ c\<^sub>2_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)

goal (11 subgoals):
 1. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 4. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 9. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 10. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 4. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 9. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 10. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 11 subgoals...
[PROOF STEP]
case CondFalse
[PROOF STATE]
proof (state)
this:
s_ \<notin> b_
\<Gamma>\<turnstile> \<langle>c\<^sub>2_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c\<^sub>2_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (11 subgoals):
 1. \<And>s b c\<^sub>2 t c\<^sub>1 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 4. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 7. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 9. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 10. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
A total of 11 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<notin> b_
\<Gamma>\<turnstile> \<langle>c\<^sub>2_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c\<^sub>2_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Cond b_ c\<^sub>1_ c\<^sub>2_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)
[PROOF STEP]
by (blast intro: step.CondFalse rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Cond b_ c\<^sub>1_ c\<^sub>2_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)

goal (10 subgoals):
 1. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 3. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 8. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 9. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 3. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 8. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 9. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case WhileTrue
[PROOF STATE]
proof (state)
this:
s_ \<in> b_
\<Gamma>\<turnstile> \<langle>c_,Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> (c_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, s'_)
\<Gamma>\<turnstile> \<langle>While b_ c_,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (While b_ c_ # ?cs, ?css, s'_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (10 subgoals):
 1. \<And>s b c s' t cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; \<And>cs css. \<Gamma>\<turnstile> (c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'); \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (While b c # cs, css, s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 3. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 6. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 8. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 9. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 10. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<in> b_
\<Gamma>\<turnstile> \<langle>c_,Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> (c_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, s'_)
\<Gamma>\<turnstile> \<langle>While b_ c_,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (While b_ c_ # ?cs, ?css, s'_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (While b_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)
[PROOF STEP]
by (blast intro: step.WhileTrue rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (While b_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)

goal (9 subgoals):
 1. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 2. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 2. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case WhileFalse
[PROOF STATE]
proof (state)
this:
s_ \<notin> b_

goal (9 subgoals):
 1. \<And>s b c cs css. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> (While b c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal s)
 2. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 5. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 9. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<notin> b_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (While b_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal s_)
[PROOF STEP]
by (blast intro: step.WhileFalse)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (While b_ c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Normal s_)

goal (8 subgoals):
 1. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case (Call p bdy s s' cs css)
[PROOF STATE]
proof (state)
this:
\<Gamma> p = Some bdy
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'
\<Gamma>\<turnstile> (bdy # ?cs, ?css, Normal s) \<rightarrow>\<^sup>* (?cs, ?css, s')

goal (8 subgoals):
 1. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have bdy: "\<Gamma> p = Some bdy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> p = Some bdy
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> p = Some bdy

goal (8 subgoals):
 1. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have steps_body: "\<Gamma>\<turnstile>([bdy],(cs,Throw#cs)#css,Normal s) \<rightarrow>\<^sup>*
                       ([],(cs,Throw#cs)#css, s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (8 subgoals):
 1. \<And>p bdy s t cs css. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (bdy # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 4. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 8. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
proof (cases s')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case (Normal s'')
[PROOF STATE]
proof (state)
this:
s' = Normal s''

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
note steps_body
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
from Normal
[PROOF STATE]
proof (chain)
picking this:
s' = Normal s''
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,Throw#cs)#css, s') \<rightarrow> (cs,css,s')"
[PROOF STATE]
proof (prove)
using this:
s' = Normal s''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, s') \<rightarrow> (cs, css, s')
[PROOF STEP]
by (auto intro: step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, s') \<rightarrow> (cs, css, s')

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using bdy
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
\<Gamma> p = Some bdy

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (blast intro: step.Call rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case (Abrupt s'')
[PROOF STATE]
proof (state)
this:
s' = Abrupt s''

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
with steps_body
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')
s' = Abrupt s''
[PROOF STEP]
have "\<Gamma>\<turnstile>([bdy],(cs,Throw#cs)#css,Normal s) \<rightarrow>\<^sup>*
             ([],(cs,Throw#cs)#css, Abrupt s'')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')
s' = Abrupt s''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, Abrupt s'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, Abrupt s'')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, Abrupt s'')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,Throw#cs)#css, Abrupt s'') \<rightarrow> (Throw#cs,css,Normal s'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, Abrupt s'') \<rightarrow> (Throw # cs, css, Normal s'')
[PROOF STEP]
by (rule ExitBlockAbrupt)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, Abrupt s'') \<rightarrow> (Throw # cs, css, Normal s'')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, Abrupt s'') \<rightarrow> (Throw # cs, css, Normal s'')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
have "\<Gamma>\<turnstile>(Throw#cs,css,Normal s'') \<rightarrow> (cs,css,Abrupt s'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Throw # cs, css, Normal s'') \<rightarrow> (cs, css, Abrupt s'')
[PROOF STEP]
by (rule Throw)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Throw # cs, css, Normal s'') \<rightarrow> (cs, css, Abrupt s'')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using bdy Abrupt
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'')
\<Gamma> p = Some bdy
s' = Abrupt s''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (auto intro: step.Call rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case Fault
[PROOF STATE]
proof (state)
this:
s' = Fault x3_

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
note steps_body
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
from Fault
[PROOF STATE]
proof (chain)
picking this:
s' = Fault x3_
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,Throw#cs)#css, s') \<rightarrow> (cs,css,s')"
[PROOF STATE]
proof (prove)
using this:
s' = Fault x3_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, s') \<rightarrow> (cs, css, s')
[PROOF STEP]
by (auto intro: step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, s') \<rightarrow> (cs, css, s')

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using bdy
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
\<Gamma> p = Some bdy

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (blast intro: step.Call rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case Stuck
[PROOF STATE]
proof (state)
this:
s' = Stuck

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
note steps_body
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, Throw # cs) # css, s')

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
from Stuck
[PROOF STATE]
proof (chain)
picking this:
s' = Stuck
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,Throw#cs)#css, s') \<rightarrow> (cs,css,s')"
[PROOF STATE]
proof (prove)
using this:
s' = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, s') \<rightarrow> (cs, css, s')
[PROOF STEP]
by (auto intro: step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, Throw # cs) # css, s') \<rightarrow> (cs, css, s')

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using bdy
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([bdy], (cs, Throw # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
\<Gamma> p = Some bdy

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (blast intro: step.Call rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (7 subgoals):
 1. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case (CallUndefined p s cs css)
[PROOF STATE]
proof (state)
this:
\<Gamma> p = None

goal (7 subgoals):
 1. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have undef: "\<Gamma> p = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> p = None
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> p = None

goal (7 subgoals):
 1. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
hence "\<Gamma>\<turnstile>(Call p # cs, css, Normal s) \<rightarrow> (cs, css, Stuck)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> p = None

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow> (cs, css, Stuck)
[PROOF STEP]
by (rule step.CallUndefined)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow> (cs, css, Stuck)

goal (7 subgoals):
 1. \<And>p s cs css. \<Gamma> p = None \<Longrightarrow> \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 3. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 6. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 7. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow> (cs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Call p # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)

goal (6 subgoals):
 1. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 4. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 4. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case StuckProp
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. \<And>c cs css. \<Gamma>\<turnstile> (c # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
 2. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 4. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 5. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 6. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c_ # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)
[PROOF STEP]
by (blast intro: step.StuckProp rtrancl_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c_ # cs, css, Stuck) \<rightarrow>\<^sup>* (cs, css, Stuck)

goal (5 subgoals):
 1. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 3. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 4. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 3. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 4. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case DynCom
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c_ s_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c_ s_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (5 subgoals):
 1. \<And>c s t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c s,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c s # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (DynCom c # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 3. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 4. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 5. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c_ s_,Normal s_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> (c_ s_ # ?cs, ?css, Normal s_) \<rightarrow>\<^sup>* (?cs, ?css, t_)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (DynCom c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)
[PROOF STEP]
by (blast intro: step.DynCom rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (DynCom c_ # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, t_)

goal (4 subgoals):
 1. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 2. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 2. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case Throw
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>s cs css. \<Gamma>\<turnstile> (Throw # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 2. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 4. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Throw # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Abrupt s_)
[PROOF STEP]
by (blast intro: step.Throw)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Throw # cs, css, Normal s_) \<rightarrow>\<^sup>* (cs, css, Abrupt s_)

goal (3 subgoals):
 1. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case AbruptProp
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>c s cs css. \<Gamma>\<turnstile> (c # cs, css, Abrupt s) \<rightarrow>\<^sup>* (cs, css, Abrupt s)
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 3. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c_ # cs, css, Abrupt s_) \<rightarrow>\<^sup>* (cs, css, Abrupt s_)
[PROOF STEP]
by (blast intro: step.AbruptProp)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c_ # cs, css, Abrupt s_) \<rightarrow>\<^sup>* (cs, css, Abrupt s_)

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case (CatchMatch c\<^sub>1 s s' c\<^sub>2 s'' cs css)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'
\<Gamma>\<turnstile> (c\<^sub>1 # ?cs, ?css, Normal s) \<rightarrow>\<^sup>* (?cs, ?css, Abrupt s')
\<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> s''
\<Gamma>\<turnstile> (c\<^sub>2 # ?cs, ?css, Normal s') \<rightarrow>\<^sup>* (?cs, ?css, s'')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have steps_c1: "\<Gamma>\<turnstile>([c\<^sub>1],(cs,c\<^sub>2#cs)#css,Normal s) \<rightarrow>\<^sup>*
                    ([],(cs,c\<^sub>2#cs)#css,Abrupt s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Abrupt s')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Abrupt s')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Abrupt s')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,c\<^sub>2#cs)#css,Abrupt s') \<rightarrow> (c\<^sub>2#cs,css,Normal s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Abrupt s') \<rightarrow> (c\<^sub>2 # cs, css, Normal s')
[PROOF STEP]
by (rule ExitBlockAbrupt)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Abrupt s') \<rightarrow> (c\<^sub>2 # cs, css, Normal s')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Abrupt s') \<rightarrow> (c\<^sub>2 # cs, css, Normal s')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have steps_c2: "\<Gamma>\<turnstile>(c\<^sub>2#cs,css,Normal s') \<rightarrow>\<^sup>* (cs,css,s'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, s'')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, s'')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, Abrupt s'); \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>2 # cs, css, Normal s') \<rightarrow>\<^sup>* (cs, css, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
 2. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'')
[PROOF STEP]
show "\<Gamma>\<turnstile>(Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'')
[PROOF STEP]
by (blast intro: step.Catch rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s'')

goal (1 subgoal):
 1. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
case (CatchMiss c\<^sub>1 s s' c\<^sub>2 cs css)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'
\<Gamma>\<turnstile> (c\<^sub>1 # ?cs, ?css, Normal s) \<rightarrow>\<^sup>* (?cs, ?css, s')
\<not> isAbr s'

goal (1 subgoal):
 1. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
assume notAbr: "\<not> isAbr s'"
[PROOF STATE]
proof (state)
this:
\<not> isAbr s'

goal (1 subgoal):
 1. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
have steps_c1: "\<Gamma>\<turnstile>([c\<^sub>1],(cs,c\<^sub>2#cs)#css,Normal s) \<rightarrow>\<^sup>* ([],(cs,c\<^sub>2#cs)#css,s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')

goal (1 subgoal):
 1. \<And>c\<^sub>1 s t c\<^sub>2 cs css. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>cs css. \<Gamma>\<turnstile> (c\<^sub>1 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t); \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, t)
[PROOF STEP]
show "\<Gamma>\<turnstile>(Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
proof (cases s')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case (Normal w)
[PROOF STATE]
proof (state)
this:
s' = Normal w

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
with steps_c1
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
s' = Normal w
[PROOF STEP]
have "\<Gamma>\<turnstile>([c\<^sub>1],(cs,c\<^sub>2#cs)#css,Normal s) \<rightarrow>\<^sup>* ([],(cs,c\<^sub>2#cs)#css,Normal w)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
s' = Normal w

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Normal w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Normal w)

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Normal w)

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,c\<^sub>2#cs)#css,Normal w) \<rightarrow> (cs,css,Normal w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Normal w) \<rightarrow> (cs, css, Normal w)
[PROOF STEP]
by (rule ExitBlockNormal)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Normal w) \<rightarrow> (cs, css, Normal w)

goal (4 subgoals):
 1. \<And>x1. s' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 4. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal w)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal w)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using Normal
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Normal w)
s' = Normal w

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (auto intro: step.Catch rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case Abrupt
[PROOF STATE]
proof (state)
this:
s' = Abrupt x2_

goal (3 subgoals):
 1. \<And>x2. s' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 3. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
with notAbr
[PROOF STATE]
proof (chain)
picking this:
\<not> isAbr s'
s' = Abrupt x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> isAbr s'
s' = Abrupt x2_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case (Fault f)
[PROOF STATE]
proof (state)
this:
s' = Fault f

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
with steps_c1
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
s' = Fault f
[PROOF STEP]
have "\<Gamma>\<turnstile>([c\<^sub>1],(cs,c\<^sub>2#cs)#css,Normal s) \<rightarrow>\<^sup>* ([],(cs,c\<^sub>2#cs)#css,Fault f)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
s' = Fault f

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Fault f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Fault f)

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Fault f)

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,c\<^sub>2#cs)#css,Fault f) \<rightarrow> (cs,css,Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Fault f) \<rightarrow> (cs, css, Fault f)
[PROOF STEP]
by (rule FaultPropBlock)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Fault f) \<rightarrow> (cs, css, Fault f)

goal (2 subgoals):
 1. \<And>x3. s' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
 2. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using Fault
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Fault f)
s' = Fault f

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (auto intro: step.Catch rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
case Stuck
[PROOF STATE]
proof (state)
this:
s' = Stuck

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
with steps_c1
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
s' = Stuck
[PROOF STEP]
have "\<Gamma>\<turnstile>([c\<^sub>1],(cs,c\<^sub>2#cs)#css,Normal s) \<rightarrow>\<^sup>* ([],(cs,c\<^sub>2#cs)#css,Stuck)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, s')
s' = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Stuck)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Stuck)

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* ([], (cs, c\<^sub>2 # cs) # css, Stuck)

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
have "\<Gamma>\<turnstile>([],(cs,c\<^sub>2#cs)#css,Stuck) \<rightarrow> (cs,css,Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Stuck) \<rightarrow> (cs, css, Stuck)
[PROOF STEP]
by (rule StuckPropBlock)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], (cs, c\<^sub>2 # cs) # css, Stuck) \<rightarrow> (cs, css, Stuck)

goal (1 subgoal):
 1. s' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
using Stuck
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c\<^sub>1], (cs, c\<^sub>2 # cs) # css, Normal s) \<rightarrow>\<^sup>* (cs, css, Stuck)
s' = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')
[PROOF STEP]
by (auto intro: step.Catch rtranclp_trans)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2 # cs, css, Normal s) \<rightarrow>\<^sup>* (cs, css, s')

goal:
No subgoals!
[PROOF STEP]
qed