theory Ctac

lemma While_ceqv_fs0:
  assumes ra: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'"
  and     xp: "xpres_strong \<Gamma> xf v a True pabr abnormal"
  and     ex: "\<Gamma>\<turnstile> \<langle>d,x\<rangle> \<Rightarrow> t'"
  and     d: "d = While b a"
  and     d': "d' = While b' a'"
  and     beq0: "\<And>t. xf t = v \<longrightarrow> (t \<in> b) = (t \<in> b')"
  and     t: "isFault t' \<or> t' = Stuck"
  and     s: "x \<in> Normal ` {s. xf s = v}"
  shows   "\<Gamma>\<turnstile> \<langle>d',x\<rangle> \<Rightarrow> t'" using ex d d' t s proof (induct) case (WhileTrue s' b'' c' t u) hence bv: "b'' = b" and cv: "c' = a" and xfs: "xf s' = v" by auto note xp = xpres_ceqv [OF xp ra] note beq = beq0 [rule_format] have "\<Gamma> \<turnstile> \<langle>While b' a', Normal s'\<rangle> \<Rightarrow> u" proof (rule exec.WhileTrue) show sb: "s' \<in> b'" using WhileTrue beq by auto show ae: "\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t" using xfs WhileTrue ceqvD1[OF _ _ ra] by auto { fix f assume "u = Fault f" and "t = Fault f" hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" by simp } moreover { fix f z assume uv: "u = Fault f" and tv: "t = Normal z" have "\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u" proof (rule WhileTrue.hyps(5)) show "isFault u \<or> u = Stuck" using uv by simp have "xf z = v" using ae unfolding tv by (rule xpres_exec_Normal[OF xp TrueI _ xfs]) thus "t \<in> Normal ` {s. xf s = v}" by (simp add: tv) qed fact+ hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" using d' by simp } moreover { assume "u = Stuck" and "t = Stuck" hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" by simp } moreover { fix z assume uv: "u = Stuck" and tv: "t = Normal z" 
      (* clag *)
       have "\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u" proof (rule WhileTrue.hyps(5)) show "isFault u \<or> u = Stuck" using uv by simp have "xf z = v" using ae unfolding tv by (rule xpres_exec_Normal[OF xp TrueI _ xfs]) thus "t \<in> Normal ` {s. xf s = v}" by (simp add: tv) qed fact+ hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" using d' by simp } ultimately show "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" using WhileTrue.prems WhileTrue.hyps(4) by (auto elim: Fault_resultE Stuck_resultE elim!: isFaultE) qed thus ?case by (simp add: d') qed simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',x\<rangle> \<Rightarrow> t' proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>d,x\<rangle> \<Rightarrow> t'
d = While b a
d' = While b' a'
isFault t' \<or> t' = Stuck
x \<in> Normal ` {s. xf s = v}

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',x\<rangle> \<Rightarrow> t' proof (state)
goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 20 subgoals... proof (state)
this:
s' \<in> b''
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<lbrakk>c' = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b'' c',t\<rangle> \<Rightarrow> u
\<lbrakk>While b'' c' = While b a; d' = While b' a'; isFault u \<or> u = Stuck; t \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
d' = While b' a'
isFault u \<or> u = Stuck
Normal s' \<in> Normal ` {s. xf s = v}

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 20 subgoals... proof (prove)
using this:
s' \<in> b''
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<lbrakk>c' = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b'' c',t\<rangle> \<Rightarrow> u
\<lbrakk>While b'' c' = While b a; d' = While b' a'; isFault u \<or> u = Stuck; t \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
d' = While b' a'
isFault u \<or> u = Stuck
Normal s' \<in> Normal ` {s. xf s = v}

goal (1 subgoal):
 1. b'' = b &&& c' = a &&& xf s' = v proof (state)
this:
b'' = b
c' = a
xf s' = v

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 20 subgoals... proof (state)
this:
xpres_strong \<Gamma> xf v a' True pabr False

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 20 subgoals... proof (state)
this:
xf ?t = v \<Longrightarrow> (?t \<in> b) = (?t \<in> b')

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',Normal s'\<rangle> \<Rightarrow> u proof (state)
goal (3 subgoals):
 1. s' \<in> b'
 2. \<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> ?s'
 3. \<Gamma>\<turnstile> \<langle>While b' a',?s'\<rangle> \<Rightarrow> u proof (prove)
goal (1 subgoal):
 1. s' \<in> b' proof (prove)
using this:
s' \<in> b''
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<lbrakk>c' = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b'' c',t\<rangle> \<Rightarrow> u
\<lbrakk>While b'' c' = While b a; d' = While b' a'; isFault u \<or> u = Stuck; t \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
d' = While b' a'
isFault u \<or> u = Stuck
Normal s' \<in> Normal ` {s. xf s = v}
xf ?t = v \<Longrightarrow> (?t \<in> b) = (?t \<in> b')

goal (1 subgoal):
 1. s' \<in> b' proof (state)
this:
s' \<in> b'

goal (2 subgoals):
 1. \<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> ?s'
 2. \<Gamma>\<turnstile> \<langle>While b' a',?s'\<rangle> \<Rightarrow> u proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t proof (prove)
using this:
xf s' = v
s' \<in> b''
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<lbrakk>c' = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b'' c',t\<rangle> \<Rightarrow> u
\<lbrakk>While b'' c' = While b a; d' = While b' a'; isFault u \<or> u = Stuck; t \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
d' = While b' a'
isFault u \<or> u = Stuck
Normal s' \<in> Normal ` {s. xf s = v}
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal ?s\<rangle> \<Rightarrow> ?s'; xf ?s = v\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal ?s\<rangle> \<Rightarrow> ?s'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t proof (state)
this:
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
u = Fault f
t = Fault f

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
u = Fault f
t = Fault f

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Fault ?f2; t = Fault ?f2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Fault ?f2; t = Fault ?f2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Fault ?f2; t = Fault ?f2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
u = Fault f
t = Normal z

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u proof (state)
goal (4 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. isFault u \<or> u = Stuck
 4. t \<in> Normal ` {s. xf s = v} proof (prove)
goal (1 subgoal):
 1. isFault u \<or> u = Stuck proof (prove)
using this:
u = Fault f

goal (1 subgoal):
 1. isFault u \<or> u = Stuck proof (state)
this:
isFault u \<or> u = Stuck

goal (3 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. t \<in> Normal ` {s. xf s = v} proof (prove)
goal (1 subgoal):
 1. xf z = v proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. xf z = v proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> Normal z

goal (1 subgoal):
 1. xf z = v proof (state)
this:
xf z = v

goal (3 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. t \<in> Normal ` {s. xf s = v} proof (prove)
using this:
xf z = v

goal (1 subgoal):
 1. t \<in> Normal ` {s. xf s = v} proof (state)
this:
t \<in> Normal ` {s. xf s = v}

goal (2 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a' proof (state)
this:
\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
d' = While b' a'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Fault ?f2; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Fault ?f2; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Fault ?f2; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
u = Stuck
t = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
u = Stuck
t = Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
u = Stuck
t = Normal z

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
u = Stuck
t = Normal z

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u proof (state)
goal (4 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. isFault u \<or> u = Stuck
 4. t \<in> Normal ` {s. xf s = v} proof (prove)
goal (1 subgoal):
 1. isFault u \<or> u = Stuck proof (prove)
using this:
u = Stuck

goal (1 subgoal):
 1. isFault u \<or> u = Stuck proof (state)
this:
isFault u \<or> u = Stuck

goal (3 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. t \<in> Normal ` {s. xf s = v} proof (prove)
goal (1 subgoal):
 1. xf z = v proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. xf z = v proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> Normal z

goal (1 subgoal):
 1. xf z = v proof (state)
this:
xf z = v

goal (3 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. t \<in> Normal ` {s. xf s = v} proof (prove)
using this:
xf z = v

goal (1 subgoal):
 1. t \<in> Normal ` {s. xf s = v} proof (state)
this:
t \<in> Normal ` {s. xf s = v}

goal (2 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a' proof (state)
this:
\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
d' = While b' a'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<lbrakk>u = Stuck; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (chain)
picking this:
\<lbrakk>u = Fault ?f2; t = Fault ?f2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Fault ?f2; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Stuck; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
\<lbrakk>u = Fault ?f2; t = Fault ?f2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Fault ?f2; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Stuck; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (prove)
using this:
\<lbrakk>u = Fault ?f2; t = Fault ?f2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Fault ?f2; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
\<lbrakk>u = Stuck; t = Normal ?z2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
d' = While b' a'
isFault u \<or> u = Stuck
Normal s' \<in> Normal ` {s. xf s = v}
\<Gamma>\<turnstile> \<langle>While b'' c',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u

goal:
No subgoals! proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b' a',Normal s'\<rangle> \<Rightarrow> u

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 20 subgoals... proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>While b' a',Normal s'\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',Normal s'\<rangle> \<Rightarrow> u proof (state)
this:
\<Gamma>\<turnstile> \<langle>d',Normal s'\<rangle> \<Rightarrow> u

goal (19 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; d' = While b' a'; isFault (Normal s) \<or> Normal s = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal s
 2. \<And>s g c t f. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s g f c. \<lbrakk>s \<notin> g; Guard f g c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; d' = While b' a'; isFault (Fault f) \<or> Fault f = Stuck; Fault f \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; d' = While b' a'; isFault (Normal (f s)) \<or> Normal (f s) = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal (f s)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; Spec r = While b a; d' = While b' a'; isFault (Normal t) \<or> Normal t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Normal t
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; Spec r = While b a; d' = While b' a'; isFault Stuck \<or> Stuck = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault s' \<or> s' = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; s' \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 9. \<And>s ba c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>1 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
 10. \<And>s ba c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> ba; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<lbrakk>c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; d' = While b' a'; isFault t \<or> t = Stuck; Normal s \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 19 subgoals...