theory Corres_UL_C

lemma ccorres_Catch:
  "ccorres_underlying sr \<Gamma> r xf r xf P P' (d#hs) a c \<Longrightarrow>
  ccorres_underlying sr \<Gamma> r xf r xf P P' hs a (Catch c d)" apply (clarsimp simp: ccorres_underlying_def split_def) apply (drule (1) bspec) apply clarsimp apply (erule exec_handlers.cases) apply clarsimp apply (erule_tac x=na in allE) apply (erule_tac x=ta in allE) apply (erule impE) apply (erule exec_elim_cases, simp_all)[1] apply (erule EHAbrupt) apply (erule EHAbrupt) apply simp apply (clarsimp split: xstate.splits) apply (simp add: unif_rrel_def) apply fastforce apply clarsimp apply (erule exec_elim_cases, simp_all)[1] apply (erule_tac x="length hs" in allE) apply (erule_tac x=ta in allE) apply (erule impE) apply (erule EHAbrupt) apply (erule (1) EHOther) apply (clarsimp simp: unif_rrel_def split: xstate.splits) apply (erule_tac x="length (d#hs)" in allE) apply (erule_tac x=ta in allE) apply (erule impE) apply (erule (1) EHOther) apply (clarsimp simp: unif_rrel_def split: xstate.splits) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' (d # hs) a c \<Longrightarrow> ccorresG sr \<Gamma> r xf P P' hs a (TRY
  c
CATCH d
END) proof (prove)
goal (1 subgoal):
 1. \<And>aa b n t. \<lbrakk>\<forall>x\<in>sr. P (fst x) \<and> snd x \<in> P' \<and> \<not> snd (a (fst x)) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)); (aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>TRY
  c
CATCH d
END # hs,b\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa b n t. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>TRY
  c
CATCH d
END # hs,b\<rangle> \<Rightarrow> (n, t); P (fst (aa, b)) \<and> snd (aa, b) \<in> P' \<and> \<not> snd (a (fst (aa, b))) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,snd (aa, b)\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa b n t. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>TRY
  c
CATCH d
END # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa b n t h s z hsa na ta. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = na; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); \<forall>t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,s\<rangle> \<Rightarrow> (na, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,s\<rangle> \<Rightarrow> (na, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,s\<rangle> \<Rightarrow> (na, ta)
 2. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 4. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>aa s z na ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (na, ta)
 2. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 4. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>aa s z na ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); s = sa; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (na, ta)
 2. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 4. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>aa s z na ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); s = sa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta)
 2. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 4. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s z na ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta); case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s z na x1 aaa b. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x1); (aaa, b) \<in> fst (a aa); (b, x1) \<in> sr; unif_rrel (na = Suc (length hs)) r xf r xf aaa x1\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, x1) \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra x1
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s z na x1 aaa b. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x1); (aaa, b) \<in> fst (a aa); (b, x1) \<in> sr; r aaa (xf x1)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, x1) \<in> sr \<and> r ra (xf x1)
 2. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa b n t h s ta hsa. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa s ta. \<lbrakk>(aa, s) \<in> sr; P aa; s \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta; \<forall>t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (length hs, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta; \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (length hs, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (length hs, ta)
 2. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta; case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 4. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (length hs, ta)
 2. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta; case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 4. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s ta sa s'. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<not> isAbr ta; s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> ta; case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta; \<forall>t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (length (d # hs), t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length (d # hs) = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta; \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (length (d # hs), ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length (d # hs) = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,sa\<rangle> \<Rightarrow> (length (d # hs), ta)
 2. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta; case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length (d # hs) = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 3. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa s ta sa. \<lbrakk>(aa, sa) \<in> sr; P aa; sa \<in> P'; \<not> snd (a aa); s = sa; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta; case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length (d # hs) = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, s))). (t, s'') \<in> sr \<and> unif_rrel (length hs = length hs) r xf r xf ra s'' | _ \<Rightarrow> False
 2. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa b n t s. \<lbrakk>(aa, b) \<in> sr; P aa; b \<in> P'; \<not> snd (a aa); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # d # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length (d # hs)) r xf r xf ra s'' | _ \<Rightarrow> False); b = s; TRY
  c
CATCH d
END # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a (fst (aa, b))). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!