[STATEMENT]
lemma step_preserves_terminations:
  assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css',t)"
  shows "\<Gamma>\<turnstile>cs,css\<Down>s \<Longrightarrow> \<Gamma>\<turnstile>cs',css'\<Down>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs',css' \<Down> t
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', t)

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs',css' \<Down> t
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (23 subgoals):
 1. \<And>cs css s. \<Gamma>\<turnstile>Skip # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 2. \<And>s g f c cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # cs,css \<Down> Normal s
 3. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 4. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 5. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 6. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 8. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 9. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 10. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
A total of 23 subgoals...
[PROOF STEP]
case Skip
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>Skip # cs_,css_ \<Down> Normal s_

goal (23 subgoals):
 1. \<And>cs css s. \<Gamma>\<turnstile>Skip # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 2. \<And>s g f c cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # cs,css \<Down> Normal s
 3. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 4. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 5. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 6. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 8. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 9. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 10. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
A total of 23 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>Skip # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (auto elim: terminates_Normal_elim_cases terminatess_elim_cases
             intro: exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Normal s_

goal (22 subgoals):
 1. \<And>s g f c cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # cs,css \<Down> Normal s
 2. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 3. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 4. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 5. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 6. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 7. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 8. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 9. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 10. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
A total of 22 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (22 subgoals):
 1. \<And>s g f c cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # cs,css \<Down> Normal s
 2. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 3. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 4. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 5. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 6. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 7. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 8. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 9. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 10. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
A total of 22 subgoals...
[PROOF STEP]
case Guard
[PROOF STATE]
proof (state)
this:
s_ \<in> g_
\<Gamma>\<turnstile>Guard f_ g_ c_ # cs_,css_ \<Down> Normal s_

goal (22 subgoals):
 1. \<And>s g f c cs css. \<lbrakk>s \<in> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # cs,css \<Down> Normal s
 2. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 3. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 4. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 5. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 6. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 7. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 8. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 9. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 10. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
A total of 22 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<in> g_
\<Gamma>\<turnstile>Guard f_ g_ c_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c_ # cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
             intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c_ # cs_,css_ \<Down> Normal s_

goal (21 subgoals):
 1. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 2. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 3. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 4. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 5. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 6. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 7. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 8. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 9. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 10. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
A total of 21 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (21 subgoals):
 1. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 2. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 3. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 4. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 5. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 6. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 7. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 8. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 9. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 10. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
A total of 21 subgoals...
[PROOF STEP]
case GuardFault
[PROOF STATE]
proof (state)
this:
s_ \<notin> g_
\<Gamma>\<turnstile>Guard f_ g_ c_ # cs_,css_ \<Down> Normal s_

goal (21 subgoals):
 1. \<And>s g f c cs css. \<lbrakk>s \<notin> g; \<Gamma>\<turnstile>Guard f g c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 2. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 3. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 4. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 5. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 6. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 7. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 8. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 9. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 10. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
A total of 21 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<notin> g_
\<Gamma>\<turnstile>Guard f_ g_ c_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Fault f_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Fault f_

goal (20 subgoals):
 1. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 2. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 3. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 4. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 5. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 6. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 7. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 8. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 9. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 10. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
A total of 20 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (20 subgoals):
 1. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 2. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 3. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 4. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 5. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 6. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 7. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 8. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 9. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 10. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
A total of 20 subgoals...
[PROOF STEP]
case FaultProp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c_ # cs_,css_ \<Down> Fault f_

goal (20 subgoals):
 1. \<And>c cs css f. \<Gamma>\<turnstile>c # cs,css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Fault f
 2. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 3. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 4. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 5. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 6. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 7. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 8. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 9. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 10. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
A total of 20 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Fault f_
[PROOF STEP]
by (rule terminatess_Fault)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Fault f_

goal (19 subgoals):
 1. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 2. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 3. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 4. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 5. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 6. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 7. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 9. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 10. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
A total of 19 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (19 subgoals):
 1. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 2. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 3. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 4. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 5. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 6. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 7. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 9. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 10. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
A total of 19 subgoals...
[PROOF STEP]
case FaultPropBlock
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(nrms_, abrs_) # css_ \<Down> Fault f_

goal (19 subgoals):
 1. \<And>nrms abrs css f. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Fault f
 2. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 3. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 4. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 5. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 6. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 7. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 9. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 10. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
A total of 19 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>nrms_,css_ \<Down> Fault f_
[PROOF STEP]
by (rule terminatess_Fault)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms_,css_ \<Down> Fault f_

goal (18 subgoals):
 1. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 2. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 3. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 4. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 5. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 6. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 8. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 9. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 10. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
A total of 18 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 2. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 3. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 4. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 5. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 6. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 8. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 9. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 10. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
A total of 18 subgoals...
[PROOF STEP]
case AbruptProp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c_ # cs_,css_ \<Down> Abrupt s_

goal (18 subgoals):
 1. \<And>c cs css s. \<Gamma>\<turnstile>c # cs,css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 2. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 3. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 4. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 5. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 6. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 8. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 9. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 10. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
A total of 18 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c_ # cs_,css_ \<Down> Abrupt s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Abrupt s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases
              intro: terminatess.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Abrupt s_

goal (17 subgoals):
 1. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 2. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 3. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 4. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 5. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 7. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 8. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 9. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 10. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 2. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 3. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 4. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 5. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 7. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 8. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 9. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 10. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
A total of 17 subgoals...
[PROOF STEP]
case ExitBlockNormal
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(nrms_, abrs_) # css_ \<Down> Normal s_

goal (17 subgoals):
 1. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Normal s
 2. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 3. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 4. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 5. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 7. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 8. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 9. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 10. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
A total of 17 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[],(nrms_, abrs_) # css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>nrms_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases
              intro: terminatess.intros )
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms_,css_ \<Down> Normal s_

goal (16 subgoals):
 1. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 2. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 3. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 4. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 6. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 7. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 8. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 9. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 10. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 2. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 3. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 4. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 6. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 7. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 8. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 9. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 10. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
A total of 16 subgoals...
[PROOF STEP]
case ExitBlockAbrupt
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(nrms_, abrs_) # css_ \<Down> Abrupt s_

goal (16 subgoals):
 1. \<And>nrms abrs css s. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Abrupt s \<Longrightarrow> \<Gamma>\<turnstile>abrs,css \<Down> Normal s
 2. \<And>f cs css s. \<Gamma>\<turnstile>Basic f # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal (f s)
 3. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal t
 4. \<And>s r cs css. \<lbrakk>\<forall>t. (s, t) \<notin> r; \<Gamma>\<turnstile>Spec r # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 6. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 7. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 8. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 9. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 10. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
A total of 16 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>[],(nrms_, abrs_) # css_ \<Down> Abrupt s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>abrs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases
              intro: terminatess.intros )
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>abrs_,css_ \<Down> Normal s_

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

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Normal (f_ s_)
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Normal (f_ s_)

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

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Normal t_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Normal t_

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

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Stuck
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Stuck

goal (12 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 2. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 3. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 4. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 5. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 6. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 7. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 9. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 10. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 2. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 3. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 4. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 5. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 6. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 7. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 9. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 10. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
A total of 12 subgoals...
[PROOF STEP]
case Seq
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>Seq c\<^sub>1_ c\<^sub>2_ # cs_,css_ \<Down> Normal s_

goal (12 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # c\<^sub>2 # cs,css \<Down> Normal s
 2. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 3. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 4. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 5. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 6. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 7. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 9. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 10. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
A total of 12 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>Seq c\<^sub>1_ c\<^sub>2_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c\<^sub>1_ # c\<^sub>2_ # cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c\<^sub>1_ # c\<^sub>2_ # cs_,css_ \<Down> Normal s_

goal (11 subgoals):
 1. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 2. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 3. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 4. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 5. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 6. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 9. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 10. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>1 # cs,css \<Down> Normal s
 2. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 3. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 4. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 5. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 6. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 8. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 9. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 10. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
A total of 11 subgoals...
[PROOF STEP]
case CondTrue
[PROOF STATE]
proof (state)
this:
s_ \<in> b_
\<Gamma>\<turnstile>Cond b_ c\<^sub>1_ c\<^sub>2_ # cs_,css_ \<Down> Normal s_

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c\<^sub>1_ # cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c\<^sub>1_ # cs_,css_ \<Down> Normal s_

goal (10 subgoals):
 1. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 2. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 3. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 4. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 5. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 8. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 9. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 10. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 2. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 3. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 4. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 5. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 8. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 9. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 10. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case CondFalse
[PROOF STATE]
proof (state)
this:
s_ \<notin> b_
\<Gamma>\<turnstile>Cond b_ c\<^sub>1_ c\<^sub>2_ # cs_,css_ \<Down> Normal s_

goal (10 subgoals):
 1. \<And>s b c\<^sub>1 c\<^sub>2 cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 # cs,css \<Down> Normal s
 2. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 3. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 4. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 5. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 7. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 8. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 9. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 10. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<notin> b_
\<Gamma>\<turnstile>Cond b_ c\<^sub>1_ c\<^sub>2_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c\<^sub>2_ # cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c\<^sub>2_ # cs_,css_ \<Down> Normal s_

goal (9 subgoals):
 1. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 2. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 3. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 4. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 7. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 8. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 9. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 2. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 3. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 4. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 7. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 8. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 9. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case WhileTrue
[PROOF STATE]
proof (state)
this:
s_ \<in> b_
\<Gamma>\<turnstile>While b_ c_ # cs_,css_ \<Down> Normal s_

goal (9 subgoals):
 1. \<And>s b c cs css. \<lbrakk>s \<in> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c # While b c # cs,css \<Down> Normal s
 2. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 3. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 4. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 6. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 7. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 8. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 9. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<in> b_
\<Gamma>\<turnstile>While b_ c_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c_ # While b_ c_ # cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c_ # While b_ c_ # cs_,css_ \<Down> Normal s_

goal (8 subgoals):
 1. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 2. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 3. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 6. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 7. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 8. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 2. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 3. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 6. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 7. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 8. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case WhileFalse
[PROOF STATE]
proof (state)
this:
s_ \<notin> b_
\<Gamma>\<turnstile>While b_ c_ # cs_,css_ \<Down> Normal s_

goal (8 subgoals):
 1. \<And>s b c cs css. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile>While b c # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Normal s
 2. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 3. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 5. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 6. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 7. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 8. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s_ \<notin> b_
\<Gamma>\<turnstile>While b_ c_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Normal s_

goal (7 subgoals):
 1. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 2. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 5. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 6. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 2. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 5. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 6. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case (Call p bdy cs css s)
[PROOF STATE]
proof (state)
this:
\<Gamma> p = Some bdy
\<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s

goal (7 subgoals):
 1. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 2. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 5. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 6. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[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 (7 subgoals):
 1. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 2. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 5. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 6. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
from Call
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> p = Some bdy
\<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s
[PROOF STEP]
obtain
    term_body: "\<Gamma>\<turnstile>bdy \<down> Normal s" and
    term_rest: "\<forall>t. \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css\<Down>t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> p = Some bdy
\<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s

goal (1 subgoal):
 1. (\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal s; \<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce elim!: terminatess_elim_cases terminates_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>bdy \<down> Normal s
\<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t

goal (7 subgoals):
 1. \<And>p bdy cs css s. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
 2. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 4. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 5. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 6. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 7. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
show "\<Gamma>\<turnstile>[bdy],(cs,Throw # cs)#css\<Down>Normal s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s
[PROOF STEP]
proof (rule terminatess.Cons [OF term_body],clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<And>t. \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
show "\<Gamma>\<turnstile>[],(cs,Throw # cs) # css\<Down>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
case (Normal t')
[PROOF STATE]
proof (state)
this:
t = Normal t'

goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
with exec_body bdy
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
\<Gamma> p = Some bdy
t = Normal t'
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> Normal t'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
\<Gamma> p = Some bdy
t = Normal t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Normal t'
[PROOF STEP]
by (auto intro: exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Normal t'

goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
with term_rest
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Normal t'
[PROOF STEP]
have "\<Gamma>\<turnstile>cs,css\<Down>Normal t'"
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Normal t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> Normal t'
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> Normal t'

goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
with Normal
[PROOF STATE]
proof (chain)
picking this:
t = Normal t'
\<Gamma>\<turnstile>cs,css \<Down> Normal t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Normal t'
\<Gamma>\<turnstile>cs,css \<Down> Normal t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
by (auto intro: terminatess.intros terminates.intros
                 elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t

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

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
with exec_body bdy
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
\<Gamma> p = Some bdy
t = Abrupt t'
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> Abrupt t'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
\<Gamma> p = Some bdy
t = Abrupt t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Abrupt t'
[PROOF STEP]
by (auto intro: exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Abrupt t'

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
with term_rest
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Abrupt t'
[PROOF STEP]
have "\<Gamma>\<turnstile>cs,css\<Down>Abrupt t'"
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Abrupt t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> Abrupt t'
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> Abrupt t'

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
with Abrupt
[PROOF STATE]
proof (chain)
picking this:
t = Abrupt t'
\<Gamma>\<turnstile>cs,css \<Down> Abrupt t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Abrupt t'
\<Gamma>\<turnstile>cs,css \<Down> Abrupt t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
by (fastforce intro: terminatess.intros terminates.intros
                     elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t

goal (2 subgoals):
 1. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
case Fault
[PROOF STATE]
proof (state)
this:
t = Fault x3_

goal (2 subgoals):
 1. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
 2. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Fault x3_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
by (iprover intro: terminatess_Fault)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t

goal (1 subgoal):
 1. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
case Stuck
[PROOF STATE]
proof (state)
this:
t = Stuck

goal (1 subgoal):
 1. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t
[PROOF STEP]
by (iprover intro: terminatess_Stuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, Throw # cs) # css \<Down> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[bdy],(cs, Throw # cs) # css \<Down> Normal s

goal (6 subgoals):
 1. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 2. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 4. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 5. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 6. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 2. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 4. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 5. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 6. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case CallUndefined
[PROOF STATE]
proof (state)
this:
\<Gamma> p_ = None
\<Gamma>\<turnstile>Call p_ # cs_,css_ \<Down> Normal s_

goal (6 subgoals):
 1. \<And>p cs css s. \<lbrakk>\<Gamma> p = None; \<Gamma>\<turnstile>Call p # cs,css \<Down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 2. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 3. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 4. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 5. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 6. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> p_ = None
\<Gamma>\<turnstile>Call p_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Stuck
[PROOF STEP]
by (iprover intro: terminatess_Stuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Stuck

goal (5 subgoals):
 1. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 2. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 3. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 4. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 5. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 2. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 3. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 4. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 5. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case StuckProp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c_ # cs_,css_ \<Down> Stuck

goal (5 subgoals):
 1. \<And>c cs css. \<Gamma>\<turnstile>c # cs,css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Stuck
 2. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 3. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 4. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 5. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Stuck
[PROOF STEP]
by (rule terminatess_Stuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Stuck

goal (4 subgoals):
 1. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 2. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 3. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 4. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 2. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 3. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 4. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case StuckPropBlock
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(nrms_, abrs_) # css_ \<Down> Stuck

goal (4 subgoals):
 1. \<And>nrms abrs css. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>nrms,css \<Down> Stuck
 2. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 3. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 4. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>nrms_,css_ \<Down> Stuck
[PROOF STEP]
by (rule terminatess_Stuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms_,css_ \<Down> Stuck

goal (3 subgoals):
 1. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 2. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 3. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 2. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 3. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case DynCom
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>DynCom c_ # cs_,css_ \<Down> Normal s_

goal (3 subgoals):
 1. \<And>c cs css s. \<Gamma>\<turnstile>DynCom c # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>c s # cs,css \<Down> Normal s
 2. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 3. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>DynCom c_ # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c_ s_ # cs_,css_ \<Down> Normal s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c_ s_ # cs_,css_ \<Down> Normal s_

goal (2 subgoals):
 1. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 2. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 2. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case Throw
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>Throw # cs_,css_ \<Down> Normal s_

goal (2 subgoals):
 1. \<And>cs css s. \<Gamma>\<turnstile>Throw # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> Abrupt s
 2. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>Throw # cs_,css_ \<Down> Normal s_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs_,css_ \<Down> Abrupt s_
[PROOF STEP]
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
              intro: terminatess.intros terminates.intros exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs_,css_ \<Down> Abrupt s_

goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
case (Catch c1 c2 cs css s)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>Catch c1 c2 # cs,css \<Down> Normal s

goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>Catch c1 c2 # cs,css \<Down> Normal s
[PROOF STEP]
obtain
    term_c1: "\<Gamma>\<turnstile>c1 \<down> Normal s" and
    term_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2 \<down> Normal s'"and
    term_rest: "\<forall>t. \<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css\<Down>t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>Catch c1 c2 # cs,css \<Down> Normal s

goal (1 subgoal):
 1. (\<lbrakk>\<Gamma>\<turnstile>c1 \<down> Normal s; \<forall>s'. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2 \<down> Normal s'; \<forall>t. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp elim!: terminatess_elim_cases terminates_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c1 \<down> Normal s
\<forall>s'. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2 \<down> Normal s'
\<forall>t. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t

goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2 cs css s. \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 # cs,css \<Down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>[c\<^sub>1],(cs, c\<^sub>2 # cs) # css \<Down> Normal s
[PROOF STEP]
show "\<Gamma>\<turnstile>[c1],(cs, c2 # cs) # css\<Down>Normal s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[c1],(cs, c2 # cs) # css \<Down> Normal s
[PROOF STEP]
proof (rule terminatess.Cons [OF term_c1],clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<And>t. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
show "\<Gamma>\<turnstile>[],(cs, c2 # cs) # css\<Down>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
case (Normal t')
[PROOF STATE]
proof (state)
this:
t = Normal t'

goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
with exec_c1
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t
t = Normal t'
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t
t = Normal t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (auto intro: exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t

goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
with term_rest
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
have "\<Gamma>\<turnstile>cs,css\<Down>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> t
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> t

goal (4 subgoals):
 1. \<And>x1. t = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 4. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
with Normal
[PROOF STATE]
proof (chain)
picking this:
t = Normal t'
\<Gamma>\<turnstile>cs,css \<Down> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Normal t'
\<Gamma>\<turnstile>cs,css \<Down> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
by (iprover intro: terminatess.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t

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

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
with exec_c1 term_c2
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t
\<forall>s'. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2 \<down> Normal s'
t = Abrupt t'
[PROOF STEP]
have "\<Gamma>\<turnstile>c2 \<down> Normal t'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t
\<forall>s'. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2 \<down> Normal s'
t = Abrupt t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c2 \<down> Normal t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c2 \<down> Normal t'

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c2 \<down> Normal t'

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c2 \<down> Normal t'

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
assume exec_c2: "\<Gamma>\<turnstile>\<langle>c2,Normal t'\<rangle> \<Rightarrow> w"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> w

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
have "\<Gamma>\<turnstile>cs,css\<Down>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> w
[PROOF STEP]
from exec_c1 Abrupt exec_c2
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t
t = Abrupt t'
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> w
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> w"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t
t = Abrupt t'
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> w

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> w
[PROOF STEP]
by (auto intro: exec.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> w

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> w
[PROOF STEP]
with term_rest
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> w

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> w

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> ?w2 \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> ?w2

goal (3 subgoals):
 1. \<And>x2. t = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 3. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c2 \<down> Normal t'
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> ?w2 \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> ?w2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c2 \<down> Normal t'
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> ?w2 \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> ?w2

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
using Abrupt
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c2 \<down> Normal t'
\<Gamma>\<turnstile> \<langle>c2,Normal t'\<rangle> \<Rightarrow> ?w2 \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> ?w2
t = Abrupt t'

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
by (auto intro: terminatess.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t

goal (2 subgoals):
 1. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
case Fault
[PROOF STATE]
proof (state)
this:
t = Fault x3_

goal (2 subgoals):
 1. \<And>x3. t = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
 2. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Fault x3_

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
by (iprover intro: terminatess_Fault)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t

goal (1 subgoal):
 1. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
case Stuck
[PROOF STATE]
proof (state)
this:
t = Stuck

goal (1 subgoal):
 1. t = Stuck \<Longrightarrow> \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t
[PROOF STEP]
by (iprover intro: terminatess_Stuck)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(cs, c2 # cs) # css \<Down> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[c1],(cs, c2 # cs) # css \<Down> Normal s

goal:
No subgoals!
[PROOF STEP]
qed