theory Ctac

lemma While_ceqv_na0:
  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,s\<rangle> \<Rightarrow> t'"
  and    beq0: "\<And>t. xf t = v \<longrightarrow> (t \<in> b) = (t \<in> b')"
  and     d: "d = While b a"
  and     s: "s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}"
  and     d': "d' = While b' a'"
  and     t: "\<not> isFault t'" "t' \<noteq> Stuck"
  shows   "\<Gamma>\<turnstile> \<langle>d',s\<rangle> \<Rightarrow> t'" using ex d s d' t 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 "s' \<in> b'" using beq xfs bv[symmetric] WhileTrue by auto show ae: "\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t" using WhileTrue ceqvD1[OF _ _ ra] by auto show "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" proof (subst d' [symmetric], rule WhileTrue.hyps(5)) obtain z where "u = Normal z \<or> u = Abrupt z" using WhileTrue.prems by (cases u, auto) then obtain z' where "t = Normal z' \<or> t = Abrupt z'" using WhileTrue.prems WhileTrue.hyps(2) WhileTrue.hyps(4) by (auto elim: Normal_resultE Abrupt_resultE) thus "t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}" using xp ae xfs by (auto dest: xpres_execs) qed fact+ qed thus ?case using WhileTrue.prems by simp next note beq = beq0 [rule_format] case WhileFalse thus ?case apply simp apply rule apply (erule disjE) apply (erule imageE, simp) apply (auto simp: beq) done qed simp_all

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',s\<rangle> \<Rightarrow> t' proof (state)
goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault u; u \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault u; u \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck

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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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:
xf ?t = v \<Longrightarrow> (?t \<in> b) = (?t \<in> b')
xf s' = v
b = b''
s' \<in> b''
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<lbrakk>c' = While b a; Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault u; u \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck

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:
s' \<in> b''
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<lbrakk>c' = While b a; Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault u; u \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck
\<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 (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u proof (state)
goal (5 subgoals):
 1. While b'' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. d' = While b' a'
 4. \<not> isFault u
 5. u \<noteq> Stuck proof (prove)
goal (1 subgoal):
 1. (\<And>z. u = Normal z \<or> u = Abrupt z \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck

goal (1 subgoal):
 1. (\<And>z. u = Normal z \<or> u = Abrupt z \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
u = Normal z \<or> u = Abrupt z

goal (5 subgoals):
 1. While b'' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. d' = While b' a'
 4. \<not> isFault u
 5. u \<noteq> Stuck proof (chain)
picking this:
u = Normal z \<or> u = Abrupt z proof (prove)
using this:
u = Normal z \<or> u = Abrupt z

goal (1 subgoal):
 1. (\<And>z'. t = Normal z' \<or> t = Abrupt z' \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
u = Normal z \<or> u = Abrupt z
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b'' c',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. (\<And>z'. t = Normal z' \<or> t = Abrupt z' \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
t = Normal z' \<or> t = Abrupt z'

goal (5 subgoals):
 1. While b'' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. d' = While b' a'
 4. \<not> isFault u
 5. u \<noteq> Stuck proof (prove)
using this:
t = Normal z' \<or> t = Abrupt z'

goal (1 subgoal):
 1. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v} proof (prove)
using this:
t = Normal z' \<or> t = Abrupt z'
xpres_strong \<Gamma> xf v a' True pabr False
\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t
xf s' = v

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

goal (4 subgoals):
 1. While b'' c' = While b a
 2. d' = While b' a'
 3. \<not> isFault u
 4. u \<noteq> Stuck 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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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 (prove)
using this:
\<Gamma>\<turnstile> \<langle>While b' a',Normal s'\<rangle> \<Rightarrow> u
While b'' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault u
u \<noteq> Stuck

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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 19 subgoals... proof (state)
goal (19 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 19 subgoals... proof (state)
this:
xf ?t = v \<Longrightarrow> (?t \<in> b) = (?t \<in> b')

goal (19 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 19 subgoals... proof (state)
this:
s_ \<notin> b_
While b_ c_ = While b a
Normal s_ \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault (Normal s_)
Normal s_ \<noteq> Stuck

goal (19 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 19 subgoals... proof (prove)
using this:
s_ \<notin> b_
While b_ c_ = While b a
Normal s_ \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
d' = While b' a'
\<not> isFault (Normal s_)
Normal s_ \<noteq> Stuck

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>d',Normal s_\<rangle> \<Rightarrow> Normal s_ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ \<notin> b; b_ = b \<and> c_ = a; Normal s_ \<in> Normal ` {s. xf s = v} \<or> Normal s_ \<in> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',Normal s_\<rangle> \<Rightarrow> Normal s_ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ \<notin> b; b_ = b \<and> c_ = a; Normal s_ \<in> Normal ` {s. xf s = v} \<or> Normal s_ \<in> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'\<rbrakk> \<Longrightarrow> s_ \<notin> b' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s_ \<notin> b; b_ = b \<and> c_ = a; d' = While b' a'; Normal s_ \<in> Normal ` {s. xf s = v}\<rbrakk> \<Longrightarrow> s_ \<notin> b'
 2. \<lbrakk>s_ \<notin> b; b_ = b \<and> c_ = a; d' = While b' a'; Normal s_ \<in> Abrupt ` {s. pabr \<longrightarrow> xf s = v}\<rbrakk> \<Longrightarrow> s_ \<notin> b' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<notin> b; b_ = b \<and> c_ = a; d' = While b' a'; s_ = x; xf x = v\<rbrakk> \<Longrightarrow> x \<notin> b'
 2. \<lbrakk>s_ \<notin> b; b_ = b \<and> c_ = a; d' = While b' a'; Normal s_ \<in> Abrupt ` {s. pabr \<longrightarrow> xf s = v}\<rbrakk> \<Longrightarrow> s_ \<notin> b' proof (prove)
goal:
No subgoals! proof (state)
this:
\<Gamma>\<turnstile> \<langle>d',Normal s_\<rangle> \<Rightarrow> Normal s_

goal (18 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal s); Normal s \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> Fault f
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Fault f); Fault f \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Fault f\<rangle> \<Rightarrow> Fault f
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal (f s)); Normal (f s) \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault (Normal t); Normal t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault Stuck; Stuck \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault s'; s' \<noteq> Stuck\<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; s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',s'\<rangle> \<Rightarrow> t; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<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; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}; d' = While b' a'; \<not> isFault t; t \<noteq> Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d',Normal s\<rangle> \<Rightarrow> t
A total of 18 subgoals...