theory XPres

lemma xpres_strong_while0:
  assumes ex: "\<Gamma>\<turnstile> \<langle>d,s\<rangle> \<Rightarrow> t"
  and     xp: "xpres_strong \<Gamma> xf v a pres_norm pres_abr abnormal"
  and      d: "d = While b a"
  and      s: "s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}"
  and      t: "pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'"
  shows    "xf t' = v" using ex d s t proof (induct) case (WhileTrue s' b' c' t u) hence eqs: "b' = b" "c' = a" and xfs: "xf s' = v" by auto { fix w assume tv: "t = Normal w" and "\<Gamma> \<turnstile> \<langle>a, Normal s'\<rangle> \<Rightarrow> Normal w" and pres_norm have ?thesis proof (rule WhileTrue.hyps(5)) have "xf w = v" by (rule xpres_exec_Normal) fact+ thus "t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}" using tv by simp qed fact+ } moreover { fix w assume tv: "t = Abrupt w" and "\<Gamma> \<turnstile> \<langle>a, Normal s'\<rangle> \<Rightarrow> Abrupt w" and pres_abr have ?thesis proof (rule WhileTrue.hyps(5)) have "xf w = v" by (rule xpres_exec_Abrupt) fact+ thus "t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}" using tv by simp qed fact+ } ultimately show ?thesis using WhileTrue.prems(3) WhileTrue.hyps(2) WhileTrue.hyps(4) unfolding eqs apply - by (elim disjE conjE; simp; erule Normal_resultE Abrupt_resultE; simp) qed auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xf t' = v 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. xf s = v}
pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'

goal (1 subgoal):
 1. xf t' = v proof (state)
goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal s = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal s = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal (f s) = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal (f s) = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Normal t = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Stuck = Normal t' \<or> pres_norm \<and> pres_abr \<and> Stuck = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> s' = Normal t' \<or> pres_norm \<and> pres_abr \<and> s' = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; \<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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
\<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. xf s = v}; pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
While b' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}
pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal s = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal s = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal (f s) = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal (f s) = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Normal t = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Stuck = Normal t' \<or> pres_norm \<and> pres_abr \<and> Stuck = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> s' = Normal t' \<or> pres_norm \<and> pres_abr \<and> s' = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; \<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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
\<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. xf s = v}; pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
While b' c' = While b a
Normal s' \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}
pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'

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

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal s = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal s = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal (f s) = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal (f s) = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Normal t = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Stuck = Normal t' \<or> pres_norm \<and> pres_abr \<and> Stuck = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> s' = Normal t' \<or> pres_norm \<and> pres_abr \<and> s' = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; \<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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. xf t' = v proof (state)
goal (3 subgoals):
 1. While b' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}
 3. pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t' proof (prove)
goal (1 subgoal):
 1. xf w = v proof (state)
this:
xf w = v

goal (3 subgoals):
 1. While b' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}
 3. pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t' proof (prove)
using this:
xf w = v

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

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

goal (2 subgoals):
 1. While b' c' = While b a
 2. pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t' proof (state)
this:
xf t' = v

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

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

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

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

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal s = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal s = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal (f s) = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal (f s) = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Normal t = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Stuck = Normal t' \<or> pres_norm \<and> pres_abr \<and> Stuck = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> s' = Normal t' \<or> pres_norm \<and> pres_abr \<and> s' = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; \<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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. xf t' = v proof (state)
goal (3 subgoals):
 1. While b' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}
 3. pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t' proof (prove)
goal (1 subgoal):
 1. xf w = v proof (state)
this:
xf w = v

goal (3 subgoals):
 1. While b' c' = While b a
 2. t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}
 3. pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t' proof (prove)
using this:
xf w = v

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

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

goal (2 subgoals):
 1. While b' c' = While b a
 2. pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t' proof (state)
this:
xf t' = v

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

goal (20 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal s = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal s = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal (f s) = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal (f s) = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Normal t = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Stuck = Normal t' \<or> pres_norm \<and> pres_abr \<and> Stuck = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> s' = Normal t' \<or> pres_norm \<and> pres_abr \<and> s' = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; \<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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
A total of 20 subgoals... proof (chain)
picking this:
\<lbrakk>t = Normal ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Normal ?w2; pres_norm\<rbrakk> \<Longrightarrow> xf t' = v
\<lbrakk>t = Abrupt ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Abrupt ?w2; pres_abr\<rbrakk> \<Longrightarrow> xf t' = v proof (prove)
using this:
\<lbrakk>t = Normal ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Normal ?w2; pres_norm\<rbrakk> \<Longrightarrow> xf t' = v
\<lbrakk>t = Abrupt ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Abrupt ?w2; pres_abr\<rbrakk> \<Longrightarrow> xf t' = v

goal (1 subgoal):
 1. xf t' = v proof (prove)
using this:
\<lbrakk>t = Normal ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Normal ?w2; pres_norm\<rbrakk> \<Longrightarrow> xf t' = v
\<lbrakk>t = Abrupt ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Abrupt ?w2; pres_abr\<rbrakk> \<Longrightarrow> xf t' = v
pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'
\<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b' c',t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. xf t' = v proof (prove)
using this:
\<lbrakk>t = Normal ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Normal ?w2; pres_norm\<rbrakk> \<Longrightarrow> xf t' = v
\<lbrakk>t = Abrupt ?w2; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Abrupt ?w2; pres_abr\<rbrakk> \<Longrightarrow> xf t' = v
pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'
\<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> t
\<Gamma>\<turnstile> \<langle>While b a,t\<rangle> \<Rightarrow> u

goal (1 subgoal):
 1. xf t' = v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>w. \<lbrakk>t = Normal w; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Normal w; pres_norm\<rbrakk> \<Longrightarrow> xf t' = v; \<And>w. \<lbrakk>t = Abrupt w; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> Abrupt w; pres_abr\<rbrakk> \<Longrightarrow> xf t' = v; pres_norm \<and> u = Normal t' \<or> pres_norm \<and> pres_abr \<and> u = Abrupt t'; \<Gamma>\<turnstile> \<langle>a,Normal s'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While b a,t\<rangle> \<Rightarrow> u\<rbrakk> \<Longrightarrow> xf t' = v proof (state)
this:
xf t' = v

goal (19 subgoals):
 1. \<And>s. \<lbrakk>SKIP = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal s = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal s = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Guard f g c = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 4. \<And>c f. \<lbrakk>c = While b a; Fault f \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Fault f = Normal t' \<or> pres_norm \<and> pres_abr \<and> Fault f = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 5. \<And>f s. \<lbrakk>Basic f = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> Normal (f s) = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal (f s) = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Normal t = Normal t' \<or> pres_norm \<and> pres_abr \<and> Normal t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> Stuck = Normal t' \<or> pres_norm \<and> pres_abr \<and> Stuck = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> s' = Normal t' \<or> pres_norm \<and> pres_abr \<and> s' = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; \<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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; (c\<^sub>1;;
c\<^sub>2) = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
 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. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v; Cond ba c\<^sub>1 c\<^sub>2 = While b a; Normal s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}; pres_norm \<and> t = Normal t' \<or> pres_norm \<and> pres_abr \<and> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v
A total of 19 subgoals...