theory Corres_UL_C

lemma ccorres_trim_redundant_throw':
  assumes cc: "ccorres_underlying sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c"
  and    xfg: "\<And>s. axf (f s) = axf s"
  and    sr:  "\<And>t t'. (t, t') \<in> sr \<Longrightarrow> (t, f t') \<in> sr"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf G G' (SKIP # hs)
              a (c;; Basic f;; THROW)" apply (rule ccorres_rhs_assoc) apply (rule ccorresI') apply clarsimp apply (erule exec_handlers_Seq_cases') apply simp apply (erule disjE)
    \<comment> \<open>Non-abrupt case\<close> apply clarsimp apply (erule_tac x = "t'" in ccorresE [OF cc]) apply assumption apply assumption apply assumption apply (erule (1) EHOther) apply simp apply (erule exec_Normal_elim_cases | simp)+
   \<comment> \<open>Abrupt case\<close> apply clarsimp apply (erule_tac x = "t'" in ccorresE [OF cc]) apply assumption apply assumption apply assumption apply (erule (1) EHOther) apply clarsimp apply (frule exec_handlers_Cons_le) apply (erule exec_Normal_elim_cases | simp)+ apply (frule exec_handlers_SkipD) apply (clarsimp simp: xfg unif_rrel_simps elim!: bexI [rotated] sr) apply (frule exec_handlers_SkipD) apply (erule_tac x = "Normal t'" in ccorresE [OF cc]) apply assumption apply assumption apply assumption apply (erule EHAbrupt) apply simp apply (clarsimp simp: xfg unif_rrel_simps elim!: bexI [rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
Basic f;;
THROW) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
(Basic f;;
THROW)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<Gamma>\<turnstile>\<^sub>h \<langle>(c;;
(Basic f;;
THROW)) # SKIP # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length (SKIP # hs)) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<Gamma>\<turnstile>\<^sub>h \<langle>(c;;
(Basic f;;
THROW)) # SKIP # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (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; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> SKIP # hs = []) \<and> n = length (SKIP # hs) \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (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; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr za \<and> n = Suc (length hs) \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<not> isAbr za \<and> n = Suc (length hs) \<and> za = z\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 2. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (7 subgoals):
 1. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> G s
 2. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> s' \<in> G'
 3. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 4. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n20 s s' z t', t')
 5. \<And>s s' z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z; t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n20 s s' z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n20 s s' z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 6. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 7. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (6 subgoals):
 1. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> s' \<in> G'
 2. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 3. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n20 s s' z t', t')
 4. \<And>s s' z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z; t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n20 s s' z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n20 s s' z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 5. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 6. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 2. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n20 s s' z t', t')
 3. \<And>s s' z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z; t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n20 s s' z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n20 s s' z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 4. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 5. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n20 s s' z t', t')
 2. \<And>s s' z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z; t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n20 s s' z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n20 s s' z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 3. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> z; \<not> isAbr t'; \<not> isAbr z; t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (length (SKIP # hs) = length (SKIP # hs)) arrel axf arrel axf ra t'a; length (SKIP # hs) \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 2. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,Normal t'a\<rangle> \<Rightarrow> z; \<not> isAbr z; t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True arrel axf arrel axf ra t'a\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t')
 2. \<And>s s' n z za t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (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; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> za; \<not> isAbr t'; \<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' q. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (6 subgoals):
 1. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> G s
 2. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> s' \<in> G'
 3. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 4. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n34 s s' n z t' q, t')
 5. \<And>s s' n z t' q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n34 s s' n z t' q = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n34 s s' n z t' q \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 6. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> s' \<in> G'
 2. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 3. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n34 s s' n z t' q, t')
 4. \<And>s s' n z t' q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n34 s s' n z t' q = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n34 s s' n z t' q \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 5. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 2. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n34 s s' n z t' q, t')
 3. \<And>s s' n z t' q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n34 s s' n z t' q = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n34 s s' n z t' q \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 4. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t' q. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n34 s s' n z t' q, t')
 2. \<And>s s' n z t' q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n34 s s' n z t' q = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n34 s s' n z t' q \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 3. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,t'\<rangle> \<Rightarrow> Abrupt q; \<not> isAbr t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (length (SKIP # hs) = length (SKIP # hs)) arrel axf arrel axf ra t'a; length (SKIP # hs) \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,Normal t'a\<rangle> \<Rightarrow> Abrupt q; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True arrel axf arrel axf ra t'a\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z q t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>Basic f;;
THROW,Normal t'a\<rangle> \<Rightarrow> Abrupt q; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,q\<rangle> \<Rightarrow> (n, z); (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True arrel axf arrel axf ra t'a; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z q t'a ra t s'a. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,f t'a\<rangle> \<Rightarrow> (n, z); (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True arrel axf arrel axf ra t'a; n \<le> length hs; s'a = Normal (f t'a); q = f t'a\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z q t'a ra t s'a. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,f t'a\<rangle> \<Rightarrow> (n, z); (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel True arrel axf arrel axf ra t'a; n \<le> length hs; s'a = Normal (f t'a); q = f t'a; z = Normal (f t'a) \<and> n = length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf arrel axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (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; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (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; G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> G s
 2. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> s' \<in> G'
 3. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 4. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n60 s s' n z t', Normal t')
 5. \<And>s s' n z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n60 s s' n z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n60 s s' n z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> s' \<in> G'
 2. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 3. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n60 s s' n z t', Normal t')
 4. \<And>s s' n z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n60 s s' n z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n60 s s' n z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 2. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n60 s s' n z t', Normal t')
 3. \<And>s s' n z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n60 s s' n z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n60 s s' n z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (?n60 s s' n z t', Normal t')
 2. \<And>s s' n z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n60 s s' n z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n60 s s' n z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (?n60 s s' n z t', Normal t')
 2. \<And>s s' n z t' t'a ra t. \<lbrakk>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n60 s s' n z t' = length (SKIP # hs)) arrel axf arrel axf ra t'a; ?n60 s s' n z t' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (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>G s; s' \<in> G'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,t'\<rangle> \<Rightarrow> (n, z); z = Normal t' \<and> n = length hs; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = length (SKIP # hs)) arrel axf arrel axf ra t'a; n \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!