[STATEMENT]
lemma steps_Fault: "\<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
[PROOF STEP]
proof (induct c)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
case (Seq c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
\<Gamma> \<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
have steps_c\<^sub>1: "\<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
have steps_c\<^sub>2: "\<Gamma> \<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
from SeqSteps [OF steps_c\<^sub>1 refl refl]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 ?c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip ?c\<^sub>2, Fault f)
[PROOF STEP]
have "\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Fault f)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 ?c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip ?c\<^sub>2, Fault f)

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Fault f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
have "\<Gamma> \<turnstile> (Seq Skip c\<^sub>2, Fault f) \<rightarrow> (c\<^sub>2, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Fault f) \<rightarrow> (c\<^sub>2, Fault f)
[PROOF STEP]
by (rule SeqSkip)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Fault f) \<rightarrow> (c\<^sub>2, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Fault f) \<rightarrow> (c\<^sub>2, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
note steps_c\<^sub>2
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 13 subgoals...
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

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

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
case (Catch c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
\<Gamma> \<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
have steps_c\<^sub>1: "\<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
from CatchSteps [OF steps_c\<^sub>1 refl refl]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 ?c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip ?c\<^sub>2, Fault f)
[PROOF STEP]
have "\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Fault f)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 ?c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip ?c\<^sub>2, Fault f)

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Fault f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Fault f)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Fault f)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
have "\<Gamma> \<turnstile> (Catch Skip c\<^sub>2, Fault f) \<rightarrow> (Skip, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Fault f) \<rightarrow> (Skip, Fault f)
[PROOF STEP]
by (rule CatchSkip)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Fault f) \<rightarrow> (Skip, Fault f)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 12 subgoals...
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)

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

goal (11 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f); \<Gamma> \<turnstile> (c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 9. \<Gamma> \<turnstile> (Throw, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
 10. \<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)) \<Longrightarrow> \<Gamma> \<turnstile> (Parallel x, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)
A total of 11 subgoals...
[PROOF STEP]
qed (fastforce intro: step.intros)+


[STATEMENT]
lemma steps_Stuck: "\<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
[PROOF STEP]
proof (induct c)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
case (Seq c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
\<Gamma> \<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
have steps_c\<^sub>1: "\<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
have steps_c\<^sub>2: "\<Gamma> \<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
from SeqSteps [OF steps_c\<^sub>1 refl refl]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 ?c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip ?c\<^sub>2, Stuck)
[PROOF STEP]
have "\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Stuck)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 ?c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip ?c\<^sub>2, Stuck)

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Stuck)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
have "\<Gamma> \<turnstile> (Seq Skip c\<^sub>2, Stuck) \<rightarrow> (c\<^sub>2, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Stuck) \<rightarrow> (c\<^sub>2, Stuck)
[PROOF STEP]
by (rule SeqSkip)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Stuck) \<rightarrow> (c\<^sub>2, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Stuck) \<rightarrow> (c\<^sub>2, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
note steps_c\<^sub>2
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

goal (13 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 13 subgoals...
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

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

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
case (Catch c\<^sub>1 c\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
\<Gamma> \<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
have steps_c\<^sub>1: "\<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
from CatchSteps [OF steps_c\<^sub>1 refl refl]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 ?c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip ?c\<^sub>2, Stuck)
[PROOF STEP]
have "\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Stuck)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 ?c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip ?c\<^sub>2, Stuck)

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Stuck)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Stuck)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Stuck)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
have "\<Gamma> \<turnstile> (Catch Skip c\<^sub>2, Stuck) \<rightarrow> (Skip, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Stuck) \<rightarrow> (Skip, Stuck)
[PROOF STEP]
by (rule CatchSkip)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Stuck) \<rightarrow> (Skip, Stuck)

goal (12 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 12 subgoals...
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)

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

goal (11 subgoals):
 1. \<Gamma> \<turnstile> (Skip, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 2. \<And>x. \<Gamma> \<turnstile> (Basic x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 3. \<And>x. \<Gamma> \<turnstile> (Spec x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 4. \<And>x1 c1 c2. \<lbrakk>\<Gamma> \<turnstile> (c1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck); \<Gamma> \<turnstile> (c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Cond x1 c1 c2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 5. \<And>x1 c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (While x1 c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 6. \<And>x. \<Gamma> \<turnstile> (Call x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 7. \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (DynCom x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 8. \<And>x1 x2a c. \<Gamma> \<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck) \<Longrightarrow> \<Gamma> \<turnstile> (Guard x1 x2a c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 9. \<Gamma> \<turnstile> (Throw, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
 10. \<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> \<Gamma> \<turnstile> (xa, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)) \<Longrightarrow> \<Gamma> \<turnstile> (Parallel x, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)
A total of 11 subgoals...
[PROOF STEP]
qed (fastforce intro: step.intros)+


[STATEMENT]
lemma step_Fault_prop:
  assumes step: "\<Gamma> \<turnstile> (c, s) \<rightarrow> (c', s')"
  shows "\<And>f. s=Fault f \<Longrightarrow> s'=Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. s = Fault f \<Longrightarrow> s' = Fault f
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')

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


[STATEMENT]
lemma step_Stuck_prop:
  assumes step: "\<Gamma> \<turnstile> (c, s) \<rightarrow> (c', s')"
  shows "s=Stuck \<Longrightarrow> s'=Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = Stuck \<Longrightarrow> s' = Stuck
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')

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


[STATEMENT]
lemma steps_Fault_prop:
  assumes step: "\<Gamma> \<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')"
  shows "s=Fault f \<Longrightarrow> s'=Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = Fault f \<Longrightarrow> s' = Fault f
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')

goal (1 subgoal):
 1. s = Fault f \<Longrightarrow> s' = Fault f
[PROOF STEP]
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s' = Fault f \<Longrightarrow> s' = Fault f
 2. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Fault f \<Longrightarrow> s' = Fault f; b = Fault f\<rbrakk> \<Longrightarrow> s' = Fault f
[PROOF STEP]
case Refl
[PROOF STATE]
proof (state)
this:
s' = Fault f

goal (2 subgoals):
 1. s' = Fault f \<Longrightarrow> s' = Fault f
 2. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Fault f \<Longrightarrow> s' = Fault f; b = Fault f\<rbrakk> \<Longrightarrow> s' = Fault f
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s' = Fault f

goal (1 subgoal):
 1. s' = Fault f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s' = Fault f

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Fault f \<Longrightarrow> s' = Fault f; b = Fault f\<rbrakk> \<Longrightarrow> s' = Fault f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Fault f \<Longrightarrow> s' = Fault f; b = Fault f\<rbrakk> \<Longrightarrow> s' = Fault f
[PROOF STEP]
case (Trans c s c'' s'')
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c'', s'')
\<Gamma> \<turnstile> (c'', s'') \<rightarrow>\<^sup>* (c', s')
s'' = Fault f \<Longrightarrow> s' = Fault f
s = Fault f

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Fault f \<Longrightarrow> s' = Fault f; b = Fault f\<rbrakk> \<Longrightarrow> s' = Fault f
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c'', s'')
\<Gamma> \<turnstile> (c'', s'') \<rightarrow>\<^sup>* (c', s')
s'' = Fault f \<Longrightarrow> s' = Fault f
s = Fault f

goal (1 subgoal):
 1. s' = Fault f
[PROOF STEP]
by (auto intro: step_Fault_prop)
[PROOF STATE]
proof (state)
this:
s' = Fault f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps_Stuck_prop:
  assumes step: "\<Gamma> \<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')"
  shows "s=Stuck \<Longrightarrow> s'=Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = Stuck \<Longrightarrow> s' = Stuck
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')

goal (1 subgoal):
 1. s = Stuck \<Longrightarrow> s' = Stuck
[PROOF STEP]
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s' = Stuck \<Longrightarrow> s' = Stuck
 2. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Stuck \<Longrightarrow> s' = Stuck; b = Stuck\<rbrakk> \<Longrightarrow> s' = Stuck
[PROOF STEP]
case Refl
[PROOF STATE]
proof (state)
this:
s' = Stuck

goal (2 subgoals):
 1. s' = Stuck \<Longrightarrow> s' = Stuck
 2. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Stuck \<Longrightarrow> s' = Stuck; b = Stuck\<rbrakk> \<Longrightarrow> s' = Stuck
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s' = Stuck

goal (1 subgoal):
 1. s' = Stuck
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s' = Stuck

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Stuck \<Longrightarrow> s' = Stuck; b = Stuck\<rbrakk> \<Longrightarrow> s' = Stuck
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Stuck \<Longrightarrow> s' = Stuck; b = Stuck\<rbrakk> \<Longrightarrow> s' = Stuck
[PROOF STEP]
case (Trans c s c'' s'')
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c'', s'')
\<Gamma> \<turnstile> (c'', s'') \<rightarrow>\<^sup>* (c', s')
s'' = Stuck \<Longrightarrow> s' = Stuck
s = Stuck

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba); \<Gamma> \<turnstile> (aa, ba) \<rightarrow>\<^sup>* (c', s'); ba = Stuck \<Longrightarrow> s' = Stuck; b = Stuck\<rbrakk> \<Longrightarrow> s' = Stuck
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c'', s'')
\<Gamma> \<turnstile> (c'', s'') \<rightarrow>\<^sup>* (c', s')
s'' = Stuck \<Longrightarrow> s' = Stuck
s = Stuck

goal (1 subgoal):
 1. s' = Stuck
[PROOF STEP]
by (auto intro: step_Stuck_prop)
[PROOF STATE]
proof (state)
this:
s' = Stuck

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llast_strict[simp]: "llast\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llast\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma llast_llast_body: "llast = fix\<cdot>llast_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llast = fix\<cdot>llast_body
[PROOF STEP]
by (rule cfun_eqI, subst llast_def, subst llast_body.unfold, simp)


[STATEMENT]
lemma unwrap_strict[simp]: "unwrap\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrap\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding unwrap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f x xs. f\<cdot>(x :@ xs))\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by ((rule cfun_eqI)+, simp)


[STATEMENT]
lemma wrap_unwrap_ID: "wrap oo unwrap oo llast_body = llast_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap oo unwrap oo llast_body = llast_body
[PROOF STEP]
unfolding llast_body_def wrap_def unwrap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs) oo (\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))) = (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys))))
[PROOF STEP]
apply (rule cfun_eqI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. ((\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs) oo (\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))))\<cdot>x\<cdot>xa = (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys))))\<cdot>x\<cdot>xa
[PROOF STEP]
apply (case_tac xa)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa = \<bottom> \<Longrightarrow> ((\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs) oo (\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))))\<cdot>x\<cdot>xa = (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys))))\<cdot>x\<cdot>xa
 2. \<And>x xa. xa = lnil \<Longrightarrow> ((\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs) oo (\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))))\<cdot>x\<cdot>xa = (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys))))\<cdot>x\<cdot>xa
 3. \<And>x xa a llist. xa = a :@ llist \<Longrightarrow> ((\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs) oo (\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))))\<cdot>x\<cdot>xa = (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys))))\<cdot>x\<cdot>xa
[PROOF STEP]
apply (simp_all add: fix_const)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma llast_worker_llast_body: "llast_worker = unwrap oo llast_body oo wrap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llast_worker = unwrap oo llast_body oo wrap
[PROOF STEP]
unfolding llast_worker_def llast_body_def wrap_def unwrap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r x yys. case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> r\<cdot>y\<cdot>ys) = (\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))) oo (\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs)
[PROOF STEP]
apply (rule cfun_eqI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. (\<Lambda> r x yys. case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> r\<cdot>y\<cdot>ys)\<cdot>x\<cdot>xa\<cdot>xb = ((\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))) oo (\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs))\<cdot>x\<cdot>xa\<cdot>xb
[PROOF STEP]
apply (case_tac xb)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb. xb = \<bottom> \<Longrightarrow> (\<Lambda> r x yys. case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> r\<cdot>y\<cdot>ys)\<cdot>x\<cdot>xa\<cdot>xb = ((\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))) oo (\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs))\<cdot>x\<cdot>xa\<cdot>xb
 2. \<And>x xa xb. xb = lnil \<Longrightarrow> (\<Lambda> r x yys. case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> r\<cdot>y\<cdot>ys)\<cdot>x\<cdot>xa\<cdot>xb = ((\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))) oo (\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs))\<cdot>x\<cdot>xa\<cdot>xb
 3. \<And>x xa xb a llist. xb = a :@ llist \<Longrightarrow> (\<Lambda> r x yys. case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> r\<cdot>y\<cdot>ys)\<cdot>x\<cdot>xa\<cdot>xb = ((\<Lambda> f x xs. f\<cdot>(x :@ xs)) oo (\<mu> llast_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lcons\<cdot>v\<cdot>(\<Lambda> x yys. Fixrec.succeed\<cdot>(case yys of lnil \<Rightarrow> x | y :@ ys \<Rightarrow> f\<cdot>yys)))) oo (\<Lambda> f (x :@ xs). f\<cdot>x\<cdot>xs))\<cdot>x\<cdot>xa\<cdot>xb
[PROOF STEP]
apply (simp_all add: fix_const)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma llast'_llast: "llast' = llast" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
have "?rhs = fix\<cdot>llast_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llast = fix\<cdot>llast_body
[PROOF STEP]
by (simp only: llast_llast_body)
[PROOF STATE]
proof (state)
this:
llast = fix\<cdot>llast_body

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
llast = fix\<cdot>llast_body

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
have "\<dots> = wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>llast_body = wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap))
[PROOF STEP]
by (simp only: worker_wrapper_body[OF wrap_unwrap_ID])
[PROOF STATE]
proof (state)
this:
fix\<cdot>llast_body = wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap))

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fix\<cdot>llast_body = wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap))

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
have "\<dots> = wrap\<cdot>(fix\<cdot>(llast_worker))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap)) = wrap\<cdot>(fix\<cdot>llast_worker)
[PROOF STEP]
by (simp only: llast_worker_llast_body)
[PROOF STATE]
proof (state)
this:
wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap)) = wrap\<cdot>(fix\<cdot>llast_worker)

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wrap\<cdot>(fix\<cdot>(unwrap oo llast_body oo wrap)) = wrap\<cdot>(fix\<cdot>llast_worker)

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
have "... = ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap\<cdot>(fix\<cdot>llast_worker) = llast'
[PROOF STEP]
unfolding llast'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap\<cdot>(fix\<cdot>llast_worker) = wrap\<cdot>(fix\<cdot>llast_worker)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wrap\<cdot>(fix\<cdot>llast_worker) = llast'

goal (1 subgoal):
 1. llast' = llast
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
llast = llast'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
llast = llast'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WTs1_same_size: "P,E \<turnstile>1 es [::] Ts \<Longrightarrow> size es = size Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>1 es [::] Ts \<Longrightarrow> length es = length Ts
[PROOF STEP]
by (induct es arbitrary: Ts) auto


[STATEMENT]
lemma WTs1_snoc_cases:
  assumes wt: "P,E \<turnstile>1 es @ [e] [::] Ts"
  obtains T Ts' where "P,E \<turnstile>1 es [::] Ts'" "P,E \<turnstile>1 e :: T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ts' T. \<lbrakk>P,E \<turnstile>1 es [::] Ts'; P,E \<turnstile>1 e :: T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>Ts' T. \<lbrakk>P,E \<turnstile>1 es [::] Ts'; P,E \<turnstile>1 e :: T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile>1 es @ [e] [::] Ts
[PROOF STEP]
have "\<exists>T Ts'. P,E \<turnstile>1 es [::] Ts' \<and> P,E \<turnstile>1 e :: T"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile>1 es @ [e] [::] Ts

goal (1 subgoal):
 1. \<exists>T Ts'. P,E \<turnstile>1 es [::] Ts' \<and> P,E \<turnstile>1 e :: T
[PROOF STEP]
by(induct es arbitrary: Ts) auto
[PROOF STATE]
proof (state)
this:
\<exists>T Ts'. P,E \<turnstile>1 es [::] Ts' \<and> P,E \<turnstile>1 e :: T

goal (1 subgoal):
 1. (\<And>Ts' T. \<lbrakk>P,E \<turnstile>1 es [::] Ts'; P,E \<turnstile>1 e :: T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>T Ts'. P,E \<turnstile>1 es [::] Ts' \<and> P,E \<turnstile>1 e :: T

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(auto intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WTs1_append:
  assumes wt: "P,Env \<turnstile>1 es @ es' [::] Ts"
  obtains Ts' Ts'' where "P,Env \<turnstile>1 es [::] Ts'" "P,Env \<turnstile>1 es' [::] Ts''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ts' Ts''. \<lbrakk>P,Env \<turnstile>1 es [::] Ts'; P,Env \<turnstile>1 es' [::] Ts''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>Ts' Ts''. \<lbrakk>P,Env \<turnstile>1 es [::] Ts'; P,Env \<turnstile>1 es' [::] Ts''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,Env \<turnstile>1 es @ es' [::] Ts
[PROOF STEP]
have "\<exists>Ts' Ts''. P,Env \<turnstile>1 es [::] Ts' \<and> P,Env \<turnstile>1 es' [::] Ts''"
[PROOF STATE]
proof (prove)
using this:
P,Env \<turnstile>1 es @ es' [::] Ts

goal (1 subgoal):
 1. \<exists>Ts' Ts''. P,Env \<turnstile>1 es [::] Ts' \<and> P,Env \<turnstile>1 es' [::] Ts''
[PROOF STEP]
by(induct es arbitrary: Ts) auto
[PROOF STATE]
proof (state)
this:
\<exists>Ts' Ts''. P,Env \<turnstile>1 es [::] Ts' \<and> P,Env \<turnstile>1 es' [::] Ts''

goal (1 subgoal):
 1. (\<And>Ts' Ts''. \<lbrakk>P,Env \<turnstile>1 es [::] Ts'; P,Env \<turnstile>1 es' [::] Ts''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>Ts' Ts''. P,Env \<turnstile>1 es [::] Ts' \<and> P,Env \<turnstile>1 es' [::] Ts''

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(auto intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WT1_not_contains_insync: "P,E \<turnstile>1 e :: T \<Longrightarrow> \<not> contains_insync e"
  and WTs1_not_contains_insyncs: "P,E \<turnstile>1 es [::] Ts \<Longrightarrow> \<not> contains_insyncs es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile>1 e :: T \<Longrightarrow> \<not> contains_insync e) &&& (P,E \<turnstile>1 es [::] Ts \<Longrightarrow> \<not> contains_insyncs es)
[PROOF STEP]
by(induct rule: WT1_WTs1.inducts) auto


[STATEMENT]
lemma WT1_expr_locks: "P,E \<turnstile>1 e :: T \<Longrightarrow> expr_locks e = (\<lambda>a. 0)"
  and WTs1_expr_lockss: "P,E \<turnstile>1 es [::] Ts \<Longrightarrow> expr_lockss es = (\<lambda>a. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile>1 e :: T \<Longrightarrow> expr_locks e = (\<lambda>a. 0)) &&& (P,E \<turnstile>1 es [::] Ts \<Longrightarrow> expr_lockss es = (\<lambda>a. 0))
[PROOF STEP]
by(induct rule: WT1_WTs1.inducts)(auto)