theory Ctac

lemma Seq_ceqv:
  assumes ra: "\<And>t'. ceqv \<Gamma> xf v t t' a a'"
  and     rb: "\<And>t. ceqv \<Gamma> xf v t t' b b'"
  and     xp: "xpres_strong \<Gamma> xf v a True pres_abr abnormal" (* Check that a does preserve xf first *)
  shows   "ceqv \<Gamma> xf v t t' (a ;; b) (a' ;; b')" using xp apply - apply (rule ceqvI) apply rule apply (erule exec_Normal_elim_cases) apply rule apply (erule (1) ceqvD1 [OF _ _ ra]) apply (case_tac s') apply simp apply (erule ceqvD1) prefer 2 apply (rule assms) apply (erule (2) xpres_execs[OF _ TrueI]) apply (fastforce dest: Abrupt_end Fault_end Stuck_end)+ 
  (* clag *)
    apply (erule exec_Normal_elim_cases) apply rule apply (erule (1) ceqvD2 [OF _ _ ra]) apply (case_tac s') apply simp apply (erule ceqvD2) prefer 2 apply (rule assms) apply (rule xpres_execs[OF _ TrueI], assumption) apply (erule (1) ceqvD2 [OF _ _ ra]) apply (fastforce dest: Abrupt_end Fault_end Stuck_end)+ done

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

goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (a;;
b) (a';;
b') proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v a True pres_abr abnormal \<Longrightarrow> ceqv \<Gamma> xf v t t' (a;;
b) (a';;
b') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> ?s'8 s'
 2. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',?s'8 s'\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Normal x1; \<Gamma>\<turnstile> \<langle>b,Normal x1\<rangle> \<Rightarrow> t'; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',Normal x1\<rangle> \<Rightarrow> t'
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ?xf17 s' x1 x1 = ?v17 s' x1
 2. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf17 s' x1) (?v17 s' x1) x1 t' b b'
 3. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 4. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 5. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf17 s' x1) (?v17 s' x1) x1 t' b b'
 2. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ?xf17 s' x1 x1 = ?v17 s' x1
 3. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 4. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 5. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> xf x1 = v
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 2. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 3. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> ?s'77 s'
 2. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,?s'77 s'\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; \<Gamma>\<turnstile> \<langle>b',Normal x1\<rangle> \<Rightarrow> t'; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal x1\<rangle> \<Rightarrow> t'
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ?xf86 s' x1 x1 = ?v86 s' x1
 2. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf86 s' x1) (?v86 s' x1) x1 t' b b'
 3. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 5. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf86 s' x1) (?v86 s' x1) x1 t' b b'
 2. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> ?xf86 s' x1 x1 = ?v86 s' x1
 3. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 5. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> xf x1 = v
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal (?s90 s' x1)\<rangle> \<Rightarrow> Normal x1
 2. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> xf (?s90 s' x1) = v
 3. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 5. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>s' x1. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> xf t = v
 2. \<And>s' x2. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 3. \<And>s' x3. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'
 4. \<And>s'. \<lbrakk>xpres_strong \<Gamma> xf v a True pres_abr abnormal; xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b',s'\<rangle> \<Rightarrow> t'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t' proof (prove)
goal:
No subgoals!