theory Corres_UL_C

lemma ccorres_master_split:
  assumes ac: "ccorres_underlying sr \<Gamma> r' xf' arrel' axf' P P' hs' a c"
  and    hsw: "hs' \<noteq> [] \<Longrightarrow> hs' = hs"
  and     bd: "\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (R rv) (R' rv) hs (b rv) d"
  and  abort: "\<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorres_underlying sr \<Gamma> arrel axf arrel axf (E rv) (E' rv)
                                      [] (b rv) Skip"
  and  valid: "\<lbrace>Q\<rbrace> a \<lbrace>\<lambda>rv. R rv and E rv\<rbrace>"
  and valid': "exec_handlers_Hoare \<Gamma> Q' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. R' a))
                               {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel' axf' (\<lambda>a b. E' a)}"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs (a >>= (\<lambda>rv. b rv)) (c ;; d)" apply (rule ccorresI') apply (erule exec_handlers_Seq_cases') apply (clarsimp simp add: bind_def) apply (erule(3) ccorresE [OF ac]) apply (erule(1) EHOther) apply simp apply (frule exec_handlers_Hoare_NormalD[OF valid']) apply (erule EHOther, simp) apply simp apply (frule(1) use_valid [OF _ valid]) apply (clarsimp simp: unif_rrel_simps ccHoarePost_def) apply (drule spec, drule(1) mp) apply (erule_tac x=z in ccorresE [OF bd], assumption+) apply (clarsimp simp: split_def image_image) apply force apply (case_tac "isAbr za") apply (clarsimp elim!: isAbrE) apply (erule EHAbrupt) apply (erule disjE) apply clarsimp apply (rule EHEmpty) apply assumption apply (simp add: isAbr_def) apply (erule EHOther) apply (clarsimp simp: isAbr_def split_def) apply (clarsimp simp: split_def) apply force apply (clarsimp simp: bind_def) apply (cases "hs' = []") apply (erule(3) ccorresE [OF ac]) apply simp apply (erule EHAbrupt, rule EHEmpty) apply simp apply (frule hsw) apply (erule(3) ccorresE [OF ac]) apply simp apply (erule(1) EHAbrupt) apply (frule(1) use_valid [OF _ valid]) apply (cases hs, simp_all)[1] apply (frule exec_handlers_Cons_le) apply (frule exec_handlers_Hoare_CatchD[OF valid']) apply (erule EHAbrupt) apply simp apply clarsimp apply (simp add: unif_rrel_simps ccHoarePost_def) apply (elim conjE) apply (drule spec, drule(1) mp) apply (rule ccorresE [OF abort], simp, assumption+) apply (clarsimp simp: split_def image_image) apply force apply (rule EHOther) apply (rule exec.intros) apply simp apply (clarsimp simp add: unif_rrel_simps split_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs (a >>= b) (c;;
d) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>(c;;
d) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>d,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>d,t'\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z za t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>d,t'\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs',s'\<rangle> \<Rightarrow> (?n26 s s' n z za t', ?x26 s s' n z za t')
 2. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>d,t'\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); ?x26 s s' n z za t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n26 s s' n z za t' = length hs') r' xf' arrel' axf' ra t'a; ?n26 s s' n z za t' \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>d,t'\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (length hs' = length hs') r' xf' arrel' axf' ra t'a; length hs' \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' ra t'a\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z za t' t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' r t'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n34 s s' n z za t' t'a r t, Normal (?t34 s s' n z za t' t'a r t))
 2. \<And>s s' n z za t' t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' r t'a\<rbrakk> \<Longrightarrow> ?n34 s s' n z za t' t'a r t = length (c # hs) - 1
 3. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' ra t'a; ?t34 s s' n z za t' t'a ra t \<in> ccHoarePost r' xf' (\<lambda>a b. R' a)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z za t' t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' r t'a\<rbrakk> \<Longrightarrow> length hs = length (c # hs) - 1
 2. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' ra t'a; t'a \<in> ccHoarePost r' xf' (\<lambda>a b. R' a)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' ra t'a; t'a \<in> ccHoarePost r' xf' (\<lambda>a b. R' a)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True r' xf' arrel' axf' ra t'a; t'a \<in> ccHoarePost r' xf' (\<lambda>a b. R' a); (R ra and E ra) t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; r' ra (xf' t'a); \<forall>rv. r' rv (xf' t'a) \<longrightarrow> t'a \<in> R' rv; R ra t; E ra t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r\<rbrakk> \<Longrightarrow> \<not> snd (b r t)
 2. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 3. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (b (fst x) (snd x)); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; snd (b r t)\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 3. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 2. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 2. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 3. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> Abrupt sa; hs = [] \<and> n = length hs \<and> Abrupt sa = z \<or> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z (Abrupt sa) t'a r t, z)
 2. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 3. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; hs = [] \<and> n = length hs \<and> Abrupt sa = z \<or> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (?n52 s s' n z (Abrupt sa) t'a r t, z)
 2. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 3. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' n z t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; hs = [] \<and> n = length hs \<and> Abrupt sa = z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (?n52 s s' n z (Abrupt sa) t'a r t, z)
 2. \<And>s s' n z t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (?n52 s s' n z (Abrupt sa) t'a r t, z)
 3. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 4. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 5. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; hs = []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[],sa\<rangle> \<Rightarrow> (?n52 s s' 0 (Abrupt sa) (Abrupt sa) t'a r t, Abrupt sa)
 2. \<And>s s' n z t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (?n52 s s' n z (Abrupt sa) t'a r t, z)
 3. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (?n52 s s' n z za t'a r t, z)
 4. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (?n52 s s' n z za t'a ra t = length hs) r xf arrel axf raa t'; ?n52 s s' n z za t'a ra t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 5. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z t'a r t sa. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,sa\<rangle> \<Rightarrow> (n, z)
 2. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (n, z)
 3. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf raa t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z za t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<not> isAbr za\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (n, z)
 2. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf raa t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> z; n = length hs; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<forall>s. z \<noteq> Abrupt s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,t'a\<rangle> \<Rightarrow> (length hs, z)
 2. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf raa t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t'a r t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; n = length hs; P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (r, t) \<in> fst (a s); r' r (xf' t'a); R r t; E r t; t'a \<in> R' r; \<forall>s. z \<noteq> Abrupt s\<rbrakk> \<Longrightarrow> \<not> isAbr z
 2. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf raa t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, z)); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; z = Normal t'; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf raa t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n za t'a ra t t' raa ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>d,Normal t'a\<rangle> \<Rightarrow> za; (isAbr za \<longrightarrow> hs = []) \<and> n = length hs \<and> za = Normal t' \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, Normal t')); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (b (fst x) (snd x)); \<not> snd (a s); (ra, t) \<in> fst (a s); r' ra (xf' t'a); R ra t; E ra t; t'a \<in> R' ra; (raa, ta) \<in> fst (b ra t); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf raa t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (b (fst y) (snd y)). (snd x, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf (fst x) t'
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<not> snd ((a >>= b) s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs',s'\<rangle> \<Rightarrow> (?n118 s s' n z t', ?x118 s s' n z t')
 2. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = []; ?x118 s s' n z t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n118 s s' n z t' = length hs') r' xf' arrel' axf' ra t'a; ?n118 s s' n z t' \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (?n118 s s' n z t', ?x118 s s' n z t')
 2. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = []; ?x118 s s' n z t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n118 s s' n z t' = length hs') r' xf' arrel' axf' ra t'a; ?n118 s s' n z t' \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = []; Abrupt t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (0 = length hs') r' xf' arrel' axf' ra t'a; 0 \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []; hs' = hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []; hs' = hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs',s'\<rangle> \<Rightarrow> (?n129 s s' n z t', ?x129 s s' n z t')
 2. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []; hs' = hs; ?x129 s s' n z t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n129 s s' n z t' = length hs') r' xf' arrel' axf' ra t'a; ?n129 s s' n z t' \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs \<noteq> []; hs' = hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n129 s s' n z t', ?x129 s s' n z t')
 2. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []; hs' = hs; ?x129 s s' n z t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n129 s s' n z t' = length hs') r' xf' arrel' axf' ra t'a; ?n129 s s' n z t' \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []; hs' = hs; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = length hs') r' xf' arrel' axf' ra t'a; n \<le> length hs'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a ra t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, z); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' \<noteq> []; hs' = hs; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = length hs') r' xf' arrel' axf' ra t'a; n \<le> length hs'; (R ra and E ra) t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a ra t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' ra t'a; n \<le> Suc (length list); R ra t \<and> E ra t; hs = aa # list\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t'a) \<in> sr \<and> unif_rrel (n = Suc (length list)) r xf arrel axf ra t'a proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a ra t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' ra t'a; n \<le> Suc (length list); R ra t \<and> E ra t; hs = aa # list; n \<le> length list\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t'a) \<in> sr \<and> unif_rrel (n = Suc (length list)) r xf arrel axf ra t'a proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' r t'a; n \<le> Suc (length list); R r t \<and> E r t; hs = aa # list; n \<le> length list\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n145 s s' n z t' t'a r t aa list, Normal (?a145 s s' n z t' t'a r t aa list))
 2. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' r t'a; n \<le> Suc (length list); R r t \<and> E r t; hs = aa # list; n \<le> length list\<rbrakk> \<Longrightarrow> ?n145 s s' n z t' t'a r t aa list \<noteq> length (c # hs) - 1
 3. \<And>s s' n z t' t'a ra t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' ra t'a; n \<le> Suc (length list); R ra t \<and> E ra t; hs = aa # list; n \<le> length list; ?a145 s s' n z t' t'a ra t aa list \<in> {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel' axf' (\<lambda>a b. E' a)}\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t'a) \<in> sr \<and> unif_rrel (n = Suc (length list)) r xf arrel axf ra t'a proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' r t'a; n \<le> Suc (length list); R r t \<and> E r t; hs = aa # list; n \<le> length list\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (?n145 s s' n z t' t'a r t aa list, Normal (?a145 s s' n z t' t'a r t aa list))
 2. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' r t'a; n \<le> Suc (length list); R r t \<and> E r t; hs = aa # list; n \<le> length list\<rbrakk> \<Longrightarrow> ?n145 s s' n z t' t'a r t aa list \<noteq> length (c # hs) - 1
 3. \<And>s s' n z t' t'a ra t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' ra t'a; n \<le> Suc (length list); R ra t \<and> E ra t; hs = aa # list; n \<le> length list; ?a145 s s' n z t' t'a ra t aa list \<in> {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel' axf' (\<lambda>a b. E' a)}\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t'a) \<in> sr \<and> unif_rrel (n = Suc (length list)) r xf arrel axf ra t'a proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' r t'a; n \<le> Suc (length list); R r t \<and> E r t; hs = aa # list; n \<le> length list\<rbrakk> \<Longrightarrow> n \<noteq> length (c # hs) - 1
 2. \<And>s s' n z t' t'a ra t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' ra t'a; n \<le> Suc (length list); R ra t \<and> E ra t; hs = aa # list; n \<le> length list; t'a \<in> {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel' axf' (\<lambda>a b. E' a)}\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t'a) \<in> sr \<and> unif_rrel (n = Suc (length list)) r xf arrel axf ra t'a proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a ra t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = Suc (length list)) r' xf' arrel' axf' ra t'a; n \<le> Suc (length list); R ra t \<and> E ra t; hs = aa # list; n \<le> length list; t'a \<in> {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel' axf' (\<lambda>a b. E' a)}\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t'a) \<in> sr \<and> unif_rrel (n = Suc (length list)) r xf arrel axf ra t'a proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); R r t \<and> E r t; hs = aa # list; n \<le> length list; \<forall>rv. arrel' rv (axf' t'a) \<longrightarrow> t'a \<in> E' rv\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; \<forall>rv. arrel' rv (axf' t'a) \<longrightarrow> t'a \<in> E' rv; R r t; E r t\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<not> snd (b r t)
 2. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[SKIP],t'a\<rangle> \<Rightarrow> (?n157 s s' n z t' t'a r t aa list, ?x157 s s' n z t' t'a r t aa list)
 3. \<And>s s' n z t' t'a r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; ?x157 s s' n z t' t'a r t aa list = Normal t'b; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; unif_rrel (?n157 s s' n z t' t'a r t aa list = length []) arrel axf arrel axf ra t'b; ?n157 s s' n z t' t'a r t aa list \<le> length []\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (3 subgoals):
 1. \<And>s s' n t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (b (fst x) (snd x)); \<not> snd (a s); hs' = aa # list; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; snd (b r t)\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[SKIP],t'a\<rangle> \<Rightarrow> (?n157 s s' n z t' t'a r t aa list, ?x157 s s' n z t' t'a r t aa list)
 3. \<And>s s' n z t' t'a r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; ?x157 s s' n z t' t'a r t aa list = Normal t'b; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; unif_rrel (?n157 s s' n z t' t'a r t aa list = length []) arrel axf arrel axf ra t'b; ?n157 s s' n z t' t'a r t aa list \<le> length []\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[SKIP],t'a\<rangle> \<Rightarrow> (?n157 s s' n z t' t'a r t aa list, ?x157 s s' n z t' t'a r t aa list)
 2. \<And>s s' n z t' t'a r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; ?x157 s s' n z t' t'a r t aa list = Normal t'b; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; unif_rrel (?n157 s s' n z t' t'a r t aa list = length []) arrel axf arrel axf ra t'b; ?n157 s s' n z t' t'a r t aa list \<le> length []\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP,Normal t'a\<rangle> \<Rightarrow> ?x157 s s' n z t' t'a r t aa list
 2. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<not> isAbr (?x157 s s' n z t' t'a r t aa list)
 3. \<And>s s' n z t' t'a r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; ?x157 s s' n z t' t'a r t aa list = Normal t'b; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; unif_rrel (length [] = length []) arrel axf arrel axf ra t'b; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' t'a r t aa list. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r\<rbrakk> \<Longrightarrow> \<not> isAbr (Normal t'a)
 2. \<And>s s' n z t' t'a r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; Normal t'a = Normal t'b; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; unif_rrel (length [] = length []) arrel axf arrel axf ra t'b; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' t'a r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'a); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa); \<not> snd (a s); hs' = aa # list; z = Normal t'a; (r, t) \<in> fst (a s); (t, t'a) \<in> sr; arrel' r (axf' t'a); hs = aa # list; n \<le> length list; R r t; E r t; t'a \<in> E' r; Normal t'a = Normal t'b; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; unif_rrel (length [] = length []) arrel axf arrel axf ra t'b; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (r, t) \<Rightarrow> (t, t'a) \<in> sr \<and> arrel r (axf t'a) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n t' r t aa list t'b ra ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>aa # list,t'\<rangle> \<Rightarrow> (n, Normal t'b); P s; Q s; s' \<in> P'; s' \<in> Q'; \<forall>x\<in>fst (a s). \<not> snd (b (fst x) (snd x)); \<not> snd (a s); hs' = aa # list; (r, t) \<in> fst (a s); (t, t'b) \<in> sr; arrel' r (axf' t'b); hs = aa # list; n \<le> length list; R r t; E r t; t'b \<in> E' r; (ra, ta) \<in> fst (b r t); (ta, t'b) \<in> sr; arrel ra (axf t'b)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a s). \<exists>x\<in>fst (b (fst y) (snd y)). (snd x, t'b) \<in> sr \<and> arrel (fst x) (axf t'b) proof (prove)
goal:
No subgoals!