[STATEMENT]
lemma execs_Fault_end:
  assumes execs: "\<Gamma>\<turnstile>\<langle>cs,css,s\<rangle> \<Rightarrow> t" shows "s=Fault f\<Longrightarrow> t=Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = Fault f \<Longrightarrow> t = Fault f
[PROOF STEP]
using execs
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. s = Fault f \<Longrightarrow> t = Fault f
[PROOF STEP]
by (induct) (auto dest: Fault_end)


[STATEMENT]
lemma execs_Stuck_end:
  assumes execs: "\<Gamma>\<turnstile>\<langle>cs,css,s\<rangle> \<Rightarrow> t" shows "s=Stuck \<Longrightarrow> t=Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = Stuck \<Longrightarrow> t = Stuck
[PROOF STEP]
using execs
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. s = Stuck \<Longrightarrow> t = Stuck
[PROOF STEP]
by (induct) (auto dest: Stuck_end)


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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
[PROOF STEP]
proof (induct rule: converse_rtrancl_induct3 [consumes 1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> \<langle>[],[],t\<rangle> \<Rightarrow> t
 2. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (ab, ac, ba) \<rightarrow>\<^sup>* ([], [], t); \<Gamma>\<turnstile> \<langle>ab,ac,ba\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,aa,b\<rangle> \<Rightarrow> t
[PROOF STEP]
show "\<Gamma>\<turnstile>\<langle>[],[],t\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>[],[],t\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Nil)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>[],[],t\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (ab, ac, ba) \<rightarrow>\<^sup>* ([], [], t); \<Gamma>\<turnstile> \<langle>ab,ac,ba\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,aa,b\<rangle> \<Rightarrow> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (ab, ac, ba) \<rightarrow>\<^sup>* ([], [], t); \<Gamma>\<turnstile> \<langle>ab,ac,ba\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,aa,b\<rangle> \<Rightarrow> t
[PROOF STEP]
fix cs css s cs' css' w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (ab, ac, ba) \<rightarrow>\<^sup>* ([], [], t); \<Gamma>\<turnstile> \<langle>ab,ac,ba\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,aa,b\<rangle> \<Rightarrow> t
[PROOF STEP]
assume step: "\<Gamma>\<turnstile>(cs,css, s) \<rightarrow> (cs',css', w)"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', w)

goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (ab, ac, ba) \<rightarrow>\<^sup>* ([], [], t); \<Gamma>\<turnstile> \<langle>ab,ac,ba\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,aa,b\<rangle> \<Rightarrow> t
[PROOF STEP]
assume execs: "\<Gamma>\<turnstile>\<langle>cs',css',w\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs',css',w\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (ab, ac, ba) \<rightarrow>\<^sup>* ([], [], t); \<Gamma>\<turnstile> \<langle>ab,ac,ba\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,aa,b\<rangle> \<Rightarrow> t
[PROOF STEP]
from step
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', w)
[PROOF STEP]
show "\<Gamma>\<turnstile>\<langle>cs,css,s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', w)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (23 subgoals):
 1. \<And>s. \<lbrakk>cs = Skip # cs'; s = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>cs = Guard f g c # cs; s = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>cs = Guard f g c # cs'; s = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>cs = c # cs'; s = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>cs = []; css = (cs', abrs) # css'; s = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>cs = c # cs'; s = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>cs = []; css = (cs', abrs) # css'; s = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>cs = []; css = (nrms, cs') # css'; s = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>cs = Basic f # cs'; s = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>cs = Spec r # cs'; s = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
A total of 23 subgoals...
[PROOF STEP]
case (Catch c1 c2 cs s)
[PROOF STATE]
proof (state)
this:
csa__ = Catch c1 c2 # cs
sa__ = Normal s
cs' = [c1]
css' = (cs, c2 # cs) # css
w = Normal s

goal (23 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 23 subgoals...
[PROOF STEP]
with execs
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>cs',css',w\<rangle> \<Rightarrow> t
csa__ = Catch c1 c2 # cs
sa__ = Normal s
cs' = [c1]
css' = (cs, c2 # cs) # css
w = Normal s
[PROOF STEP]
obtain t' where
      exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> t'" and
      execs_rest: "\<Gamma>\<turnstile>\<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>cs',css',w\<rangle> \<Rightarrow> t
csa__ = Catch c1 c2 # cs
sa__ = Normal s
cs' = [c1]
css' = (cs, c2 # cs) # css
w = Normal s

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp elim!: execs_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t'
\<Gamma>\<turnstile> \<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t

goal (23 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 23 subgoals...
[PROOF STEP]
have  "\<Gamma>\<turnstile>\<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
proof (cases t')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. t' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> 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> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> 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.CatchMiss)
[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> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[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> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
from execs_rest Normal
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Normal t''
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>cs,css,t'\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Normal t''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,t'\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,t'\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c2 # cs,css,Normal t''\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c2 # cs,css,Normal t''\<rangle> \<Rightarrow> t

goal (3 subgoals):
 1. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>c2 # cs,css,Normal t''\<rangle> \<Rightarrow> t
[PROOF STEP]
obtain v where
          exec_c2: "\<Gamma>\<turnstile>\<langle>c2,Normal t''\<rangle> \<Rightarrow> v" and
          rest: "\<Gamma>\<turnstile>\<langle>cs,css,v\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c2 # cs,css,Normal t''\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>\<Gamma>\<turnstile> \<langle>c2,Normal t''\<rangle> \<Rightarrow> v; \<Gamma>\<turnstile> \<langle>cs,css,v\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c2,Normal t''\<rangle> \<Rightarrow> v
\<Gamma>\<turnstile> \<langle>cs,css,v\<rangle> \<Rightarrow> t

goal (3 subgoals):
 1. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[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> v
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> v"
[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> v

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

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t

goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
case (Fault f)
[PROOF STATE]
proof (state)
this:
t' = Fault f

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

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

goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> Fault f

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,Fault f\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,Fault f\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
case Stuck
[PROOF STATE]
proof (state)
this:
t' = Stuck

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
with exec_c1
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t'
t' = Stuck
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> Stuck"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> t'
t' = Stuck

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

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> Stuck

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
from execs_rest Stuck
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Stuck
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>cs,css,Stuck\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>[],(cs, c2 # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> Stuck
\<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> Stuck
\<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t

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

goal (23 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 23 subgoals...
[PROOF STEP]
with Catch
[PROOF STATE]
proof (chain)
picking this:
csa__ = Catch c1 c2 # cs
sa__ = Normal s
cs' = [c1]
css' = (cs, c2 # cs) # css
w = Normal s
\<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
csa__ = Catch c1 c2 # cs
sa__ = Normal s
cs' = [c1]
css' = (cs, c2 # cs) # css
w = Normal s
\<Gamma>\<turnstile> \<langle>Catch c1 c2 # cs,css,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t

goal (22 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 22 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (22 subgoals):
 1. \<And>s. \<lbrakk>cs = Skip # cs'; s = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>cs = Guard f g c # cs; s = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>cs = Guard f g c # cs'; s = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>cs = c # cs'; s = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>cs = []; css = (cs', abrs) # css'; s = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>cs = c # cs'; s = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>cs = []; css = (cs', abrs) # css'; s = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>cs = []; css = (nrms, cs') # css'; s = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>cs = Basic f # cs'; s = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>cs = Spec r # cs'; s = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t
A total of 22 subgoals...
[PROOF STEP]
case (Call p bdy cs s)
[PROOF STATE]
proof (state)
this:
csa__ = Call p # cs
sa__ = Normal s
cs' = [bdy]
css' = (cs, Throw # cs) # css
w = Normal s
\<Gamma> p = Some bdy

goal (22 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 22 subgoals...
[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 (22 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 22 subgoals...
[PROOF STEP]
from Call execs
[PROOF STATE]
proof (chain)
picking this:
csa__ = Call p # cs
sa__ = Normal s
cs' = [bdy]
css' = (cs, Throw # cs) # css
w = Normal s
\<Gamma> p = Some bdy
\<Gamma>\<turnstile> \<langle>cs',css',w\<rangle> \<Rightarrow> t
[PROOF STEP]
obtain t' where
      exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> \<Rightarrow> t'" and
      execs_rest:
            "\<Gamma>\<turnstile>\<langle>[],(cs,Throw#cs)#css ,t'\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
csa__ = Call p # cs
sa__ = Normal s
cs' = [bdy]
css' = (cs, Throw # cs) # css
w = Normal s
\<Gamma> p = Some bdy
\<Gamma>\<turnstile> \<langle>cs',css',w\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>[],(cs, Throw # cs) # css,t'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp elim!: execs_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t'
\<Gamma>\<turnstile> \<langle>[],(cs, Throw # cs) # css,t'\<rangle> \<Rightarrow> t

goal (22 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 22 subgoals...
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
proof (cases t')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. t' = Normal x1 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> 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> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> 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> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[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> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 4. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
from execs_rest Normal
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>[],(cs, Throw # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Normal t''
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>cs,css ,Normal t''\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>[],(cs, Throw # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Normal t''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,Normal t''\<rangle> \<Rightarrow> t
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,Normal t''\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t

goal (3 subgoals):
 1. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> 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> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> 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> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[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> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
from execs_rest Abrupt
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>[],(cs, Throw # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Abrupt t''
[PROOF STEP]
have
        "\<Gamma>\<turnstile>\<langle>Throw # cs,css,Normal t''\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>[],(cs, Throw # cs) # css,t'\<rangle> \<Rightarrow> t
t' = Abrupt t''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Throw # cs,css,Normal t''\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Throw # cs,css,Normal t''\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>\<Gamma>\<turnstile> \<langle>Throw,Normal t''\<rangle> \<Rightarrow> v; \<Gamma>\<turnstile> \<langle>cs,css,v\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp elim!: execs_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Throw,Normal t''\<rangle> \<Rightarrow> v
\<Gamma>\<turnstile> \<langle>cs,css,v\<rangle> \<Rightarrow> t

goal (3 subgoals):
 1. \<And>x2. t' = Abrupt x2 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 3. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Throw,Normal t''\<rangle> \<Rightarrow> v
\<Gamma>\<turnstile> \<langle>cs,css,v\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. v = Abrupt t''
[PROOF STEP]
by (auto elim: exec_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
v = Abrupt t''

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

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

goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
case (Fault f)
[PROOF STATE]
proof (state)
this:
t' = Fault f

goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> 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' = Fault f
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault f"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t'
\<Gamma> p = Some bdy
t' = Fault f

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

goal (2 subgoals):
 1. \<And>x3. t' = Fault x3 \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
 2. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault f

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,Fault f\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) (auto elim: execs_elim_cases dest: Fault_end)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,Fault f\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t

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

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> 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' = Stuck
[PROOF STEP]
have "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> Stuck"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t'
\<Gamma> p = Some bdy
t' = Stuck

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

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Stuck

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t
[PROOF STEP]
by (cases) (auto elim: execs_elim_cases dest: Stuck_end)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. t' = Stuck \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Stuck
\<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Stuck
\<Gamma>\<turnstile> \<langle>cs,css,Stuck\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (rule execs.Cons)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t

goal (22 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 22 subgoals...
[PROOF STEP]
with Call
[PROOF STATE]
proof (chain)
picking this:
csa__ = Call p # cs
sa__ = Normal s
cs' = [bdy]
css' = (cs, Throw # cs) # css
w = Normal s
\<Gamma> p = Some bdy
\<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
csa__ = Call p # cs
sa__ = Normal s
cs' = [bdy]
css' = (cs, Throw # cs) # css
w = Normal s
\<Gamma> p = Some bdy
\<Gamma>\<turnstile> \<langle>Call p # cs,css,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t

goal (21 subgoals):
 1. \<And>s. \<lbrakk>csa__ = Skip # cs'; sa__ = Normal s; css' = css; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 2. \<And>s g f c cs. \<lbrakk>csa__ = Guard f g c # cs; sa__ = Normal s; cs' = c # cs; css' = css; w = Normal s; s \<in> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>csa__ = Guard f g c # cs'; sa__ = Normal s; css' = css; w = Fault f; s \<notin> g\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 4. \<And>c f. \<lbrakk>csa__ = c # cs'; sa__ = Fault f; css' = css; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 5. \<And>abrs f. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Fault f; w = Fault f\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 6. \<And>c s. \<lbrakk>csa__ = c # cs'; sa__ = Abrupt s; css' = css; w = Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 7. \<And>abrs s. \<lbrakk>csa__ = []; css = (cs', abrs) # css'; sa__ = Normal s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 8. \<And>nrms s. \<lbrakk>csa__ = []; css = (nrms, cs') # css'; sa__ = Abrupt s; w = Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 9. \<And>f s. \<lbrakk>csa__ = Basic f # cs'; sa__ = Normal s; css' = css; w = Normal (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
 10. \<And>s ta r. \<lbrakk>csa__ = Spec r # cs'; sa__ = Normal s; css' = css; w = Normal ta; (s, ta) \<in> r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>csa__,css,sa__\<rangle> \<Rightarrow> t
A total of 21 subgoals...
[PROOF STEP]
qed (insert execs,
      (blast intro:execs.intros exec.intros elim!: execs_elim_cases)+)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>cs,css,s\<rangle> \<Rightarrow> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem steps_impl_exec:
  assumes steps: "\<Gamma>\<turnstile>([c],[],s) \<rightarrow>\<^sup>* ([],[],t)"
  shows "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t
[PROOF STEP]
using steps_impl_execs [OF steps]
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>[c],[],s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t
[PROOF STEP]
by (blast elim: execs_elim_cases)


[STATEMENT]
lemma not_infI: "\<lbrakk>\<And>f. \<lbrakk>f 0 = (cs,css,s); \<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False\<rbrakk>
                \<Longrightarrow> \<not>inf \<Gamma> cs css s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (cs, css, s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> cs css s
[PROOF STEP]
by (auto simp add: inf_def)


[STATEMENT]
lemma terminatess_Fault: "\<And>cs. \<Gamma>\<turnstile>cs,css\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f
[PROOF STEP]
proof (induct css)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f
 2. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f
 2. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
show "\<Gamma>\<turnstile>cs,[]\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,[] \<Down> Fault f
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],[] \<Down> Fault f
 2. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Fault f
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],[] \<Down> Fault f
 2. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Fault f
[PROOF STEP]
show "\<Gamma>\<turnstile>[],[]\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],[] \<Down> Fault f
[PROOF STEP]
by (rule terminatess.Nil)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],[] \<Down> Fault f

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Fault f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Fault f
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,[] \<Down> Fault f

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Fault f
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs,[] \<Down> Fault f

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c # cs,[] \<Down> Fault f
[PROOF STEP]
by (auto intro: terminatess.intros terminates.intros dest: Fault_end)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c # cs,[] \<Down> Fault f

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

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
case (Cons d css)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>?cs,css \<Down> Fault f

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
have hyp: "\<And>cs. \<Gamma>\<turnstile>cs,css\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>?cs,css \<Down> Fault f

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
obtain nrms abrs where d: "d=(nrms,abrs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nrms abrs. d = (nrms, abrs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases d) auto
[PROOF STATE]
proof (state)
this:
d = (nrms, abrs)

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
have "\<Gamma>\<turnstile>cs,(nrms,abrs)#css\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f
 2. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f
 2. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
show "\<Gamma>\<turnstile>[],(nrms, abrs) # css\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
by (rule terminatess.ExitBlockFault) (rule hyp)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Fault f

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
have hyp1: "\<Gamma>\<turnstile>cs,(nrms, abrs) # css\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
show "\<Gamma>\<turnstile>c#cs,(nrms, abrs)#css\<Down>Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c # cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
by (auto intro: hyp1 terminatess.Cons terminates.intros dest: Fault_end)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c # cs,(nrms, abrs) # css \<Down> Fault f

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

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Fault f) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Fault f
[PROOF STEP]
with d
[PROOF STATE]
proof (chain)
picking this:
d = (nrms, abrs)
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
d = (nrms, abrs)
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Fault f

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma terminatess_Stuck: "\<And>cs. \<Gamma>\<turnstile>cs,css\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck
[PROOF STEP]
proof (induct css)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck
 2. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck
 2. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
show "\<Gamma>\<turnstile>cs,[]\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,[] \<Down> Stuck
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],[] \<Down> Stuck
 2. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Stuck
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],[] \<Down> Stuck
 2. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Stuck
[PROOF STEP]
show "\<Gamma>\<turnstile>[],[]\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],[] \<Down> Stuck
[PROOF STEP]
by (rule terminatess.Nil)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],[] \<Down> Stuck

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Stuck
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Stuck
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,[] \<Down> Stuck

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,[] \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,[] \<Down> Stuck
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs,[] \<Down> Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c # cs,[] \<Down> Stuck
[PROOF STEP]
by (auto intro: terminatess.intros terminates.intros dest: Stuck_end)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c # cs,[] \<Down> Stuck

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

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
case (Cons d css)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>?cs,css \<Down> Stuck

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
have hyp: "\<And>cs. \<Gamma>\<turnstile>cs,css\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>?cs,css \<Down> Stuck

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
obtain nrms abrs where d: "d=(nrms,abrs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nrms abrs. d = (nrms, abrs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases d) auto
[PROOF STATE]
proof (state)
this:
d = (nrms, abrs)

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
have "\<Gamma>\<turnstile>cs,(nrms,abrs)#css\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck
 2. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck
 2. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
show "\<Gamma>\<turnstile>[],(nrms, abrs) # css\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
by (rule terminatess.ExitBlockStuck) (rule hyp)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[],(nrms, abrs) # css \<Down> Stuck

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
have hyp1: "\<Gamma>\<turnstile>cs,(nrms, abrs) # css\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck \<Longrightarrow> \<Gamma>\<turnstile>a # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
show "\<Gamma>\<turnstile>c#cs,(nrms, abrs)#css\<Down>Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c # cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
by (auto intro: hyp1 terminatess.Cons terminates.intros dest: Stuck_end)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c # cs,(nrms, abrs) # css \<Down> Stuck

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

goal (1 subgoal):
 1. \<And>a css cs. (\<And>cs. \<Gamma>\<turnstile>cs,css \<Down> Stuck) \<Longrightarrow> \<Gamma>\<turnstile>cs,a # css \<Down> Stuck
[PROOF STEP]
with d
[PROOF STATE]
proof (chain)
picking this:
d = (nrms, abrs)
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
d = (nrms, abrs)
\<Gamma>\<turnstile>cs,(nrms, abrs) # css \<Down> Stuck

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Basic_terminates: "\<Gamma>\<turnstile>Basic f \<down> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>Basic f \<down> t
[PROOF STEP]
by (cases t) (auto intro: terminates.intros)