theory Ctac

lemma While_ceqv:
  assumes beq: "\<And>t. xf t = v \<longrightarrow> (t \<in> b) = (t \<in> b')"
  and      ra: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'"
  and      xp: "xpres_strong \<Gamma> xf v a True pabr abnormal"   (* So we fail as early as possible *)
  shows   "ceqv \<Gamma> xf v t t' (While b a) (While b' a')"  (* b is a set, doesn't rewrite nicely *)
   using xp apply - apply (rule ceqvI) apply (cases t') apply rule apply (erule (1) While_ceqv_na [OF ra]) apply (rule beq) apply simp apply simp apply simp apply (rule While_ceqv_na [OF ceqv_sym [OF ra]]) apply (erule (1) xpres_ceqv [OF _ ra]) apply (rule impI) apply (erule beq [rule_format, symmetric]) apply simp apply simp apply simp 
    (* clag *)
     apply rule apply (erule (1) While_ceqv_na [OF ra]) apply (rule beq) apply simp apply simp apply simp apply simp apply (rule While_ceqv_na [OF ceqv_sym [OF ra]]) apply (erule (1) xpres_ceqv [OF _ ra]) apply (rule impI) apply (erule beq [rule_format, symmetric]) apply simp apply simp apply simp apply rule apply (erule While_ceqv_fs [OF ra xp]) apply (rule beq) apply simp apply simp apply (rule While_ceqv_fs [OF ceqv_sym [OF ra]]) apply (erule (1) xpres_ceqv [OF _ ra]) apply (rule impI) apply (erule beq [rule_format, symmetric]) apply simp apply simp 
(* clag *)
   apply rule apply (erule While_ceqv_fs [OF ra xp]) apply (rule beq) apply simp apply simp apply (rule While_ceqv_fs [OF ceqv_sym [OF ra]]) apply (erule (1) xpres_ceqv [OF _ ra]) apply (rule impI) apply (rule beq [rule_format, symmetric]) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (While b a) (While b' a') proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (While b a) (While b' a') proof (prove)
using this:
xpres_strong \<Gamma> xf v a True pabr abnormal

goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (While b a) (While b' a') proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v a True pabr abnormal \<Longrightarrow> ceqv \<Gamma> xf v t t' (While b a) (While b' a') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (8 subgoals):
 1. \<And>x1 ta. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b) = (ta \<in> b')
 2. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 4. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 5. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 6. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 7. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 8. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 2. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 3. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 4. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 5. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 2. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 3. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (9 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v a' True (?pabr15 x1) (?abnormal15 x1)
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While (?b15 x1) a',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x1 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> ?b15 x1) = (ta \<in> b)
 4. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. ?pabr15 x1 \<longrightarrow> xf s = v}
 5. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 6. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 7. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 8. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 9. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>x1 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 4. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 5. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>x1 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'; xf ta = v\<rbrakk> \<Longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 4. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 5. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 3. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 4. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 2. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Normal x1; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>x2 ta. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b) = (ta \<in> b')
 2. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 4. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 5. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 6. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 2. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 3. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 4. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 5. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<not> isFault t'
 2. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> t' \<noteq> Stuck
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> Abrupt x2
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (8 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v a' True (?pabr41 x2) (?abnormal41 x2)
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While (?b41 x2) a',Normal t\<rangle> \<Rightarrow> Abrupt x2
 3. \<And>x2 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> ?b41 x2) = (ta \<in> b)
 4. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. ?pabr41 x2 \<longrightarrow> xf s = v}
 5. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<not> isFault (Abrupt x2)
 6. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Abrupt x2 \<noteq> Stuck
 7. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 8. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>x2 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<not> isFault (Abrupt x2)
 4. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Abrupt x2 \<noteq> Stuck
 5. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>x2 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2; xf ta = v\<rbrakk> \<Longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<not> isFault (Abrupt x2)
 4. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Abrupt x2 \<noteq> Stuck
 5. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. pabr \<longrightarrow> xf s = v}
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<not> isFault (Abrupt x2)
 3. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Abrupt x2 \<noteq> Stuck
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> \<not> isFault (Abrupt x2)
 2. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Abrupt x2 \<noteq> Stuck
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Abrupt x2; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> Abrupt x2 \<noteq> Stuck
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>x3 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b) = (ta \<in> b')
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v a' True (?pabr65 x3) (?abnormal65 x3)
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While (?b65 x3) a',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>x3 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> ?b65 x3) = (ta \<in> b)
 4. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 5. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x3 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>x3 ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'; xf ta = v\<rbrakk> \<Longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 2. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Fault x3; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b) = (ta \<in> b')
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v}
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v a' True ?pabr88 ?abnormal88
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While ?b88 a',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> ?b88) = (ta \<in> b)
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} proof (prove)
goal (3 subgoals):
 1. \<And>ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} proof (prove)
goal (3 subgoals):
 1. \<And>ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'; xf ta = v\<rbrakk> \<Longrightarrow> (ta \<in> b') = (ta \<in> b)
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} proof (prove)
goal (3 subgoals):
 1. \<And>ta. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'; xf ta = v\<rbrakk> \<Longrightarrow> xf ta = v
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> isFault t' \<or> t' = Stuck
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pabr abnormal; xf t = v; t' = Stuck; \<Gamma>\<turnstile> \<langle>While b' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> Normal t \<in> Normal ` {s. xf s = v} proof (prove)
goal:
No subgoals!