theory Syscall_C

lemma ccorres_return_void_catchbrk:
  "ccorres_underlying sr G r xf ar axf P P' hs
     f return_void_C
  \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' (catchbrk_C # hs)
     f return_void_C" apply (simp add: return_void_C_def catchbrk_C_def) apply (rule ccorresI') apply clarsimp apply (erule exec_handlers_Seq_cases') prefer 2 apply (clarsimp elim!: exec_Normal_elim_cases) apply (clarsimp elim!: exec_Normal_elim_cases) apply (erule exec_handlers.cases, simp_all) prefer 2 apply (auto elim!: exec_Normal_elim_cases)[1] apply (clarsimp elim!: exec_Normal_elim_cases) apply (erule exec_Normal_elim_cases, simp_all) apply (clarsimp elim!: exec_Normal_elim_cases) apply (erule(4) ccorresE) apply (rule EHAbrupt) apply (fastforce intro: exec.intros) apply assumption apply clarsimp apply (frule exec_handlers_less) apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf P P' hs f return_void_C \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' (catchbrk_C # hs) f return_void_C proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW) \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' (IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs) f (\<acute>global_exn_var :== Return;;
THROW) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; G\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Return;;
THROW) # IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> unif_rrel (n = length (IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; G\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Return;;
THROW) # IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z za t'. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s'\<rangle> \<Rightarrow> t'; G\<turnstile> \<langle>THROW,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs = []) \<and> n = length (IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs) \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> G\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t')
 2. \<And>s s' n z t'. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s'\<rangle> \<Rightarrow> Abrupt t'; G\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t'. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s'\<rangle> \<Rightarrow> Abrupt t'; G\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,t'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t')
 2. \<And>s s' n z za t'. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s'\<rangle> \<Rightarrow> t'; G\<turnstile> \<langle>THROW,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs = []) \<and> n = length (IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs) \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> G\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z za t'. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s'\<rangle> \<Rightarrow> t'; G\<turnstile> \<langle>THROW,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs = []) \<and> n = length (IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs) \<and> za = z \<or> (\<exists>q. za = Abrupt q \<and> G\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,q\<rangle> \<Rightarrow> (n, z)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z h sa za na t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); s'\<lparr>global_exn_var_' := Return\<rparr> = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; n = na; z = t; G\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; G\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); s'\<lparr>global_exn_var_' := Return\<rparr> = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; n = length hs; z = t; G\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf ar axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z h sa t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); s'\<lparr>global_exn_var_' := Return\<rparr> = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; n = length hs; z = t; G\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf ar axf ra t')
 2. \<And>s s' n z h sa za na t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); s'\<lparr>global_exn_var_' := Return\<rparr> = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; n = na; z = t; G\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; G\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z h sa za na t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); s'\<lparr>global_exn_var_' := Return\<rparr> = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; n = na; z = t; G\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; G\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' za na t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile> \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI,Normal (s'\<lparr>global_exn_var_' := Return\<rparr>)\<rangle> \<Rightarrow> Abrupt za; G\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' za na t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); G\<turnstile> \<langle>THROW,Normal (s'\<lparr>global_exn_var_' := Return\<rparr>)\<rangle> \<Rightarrow> Abrupt za\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' na t. \<lbrakk>ccorres_underlying sr G r xf ar axf P P' hs f (\<acute>global_exn_var :== Return;;
THROW); (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' na t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> G\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Return;;
THROW) # hs,s'\<rangle> \<Rightarrow> (?n49 s s' na t, ?x49 s s' na t)
 2. \<And>s s' na t t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); ?x49 s s' na t = Normal t'; (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (?n49 s s' na t = length hs) r xf ar axf ra t'; ?n49 s s' na t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' na t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> G\<turnstile> \<langle>\<acute>global_exn_var :== Return;;
THROW,Normal s'\<rangle> \<Rightarrow> Abrupt (?z56 s s' na t)
 2. \<And>s s' na t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> G\<turnstile>\<^sub>h \<langle>hs,?z56 s s' na t\<rangle> \<Rightarrow> (?n49 s s' na t, ?x49 s s' na t)
 3. \<And>s s' na t t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); ?x49 s s' na t = Normal t'; (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (?n49 s s' na t = length hs) r xf ar axf ra t'; ?n49 s s' na t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' na t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (?n49 s s' na t, ?x49 s s' na t)
 2. \<And>s s' na t t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); ?x49 s s' na t = Normal t'; (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (?n49 s s' na t = length hs) r xf ar axf ra t'; ?n49 s s' na t \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' na t t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); t = Normal t'; (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf ar axf ra t'; na \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' na t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, Normal t'); (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf ar axf ra t'; na \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf ar axf ra t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' na t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, Normal t'); (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf ar axf ra t'; na \<le> length hs\<rbrakk> \<Longrightarrow> Normal t' \<notin> range Abrupt
 2. \<And>s s' na t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, Normal t'); (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf ar axf ra t'; na \<le> length hs; na < length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf ar axf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' na t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (f s); G\<turnstile>\<^sub>h \<langle>hs,s'\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, Normal t'); (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf ar axf ra t'; na \<le> length hs; na < length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel False r xf ar axf ra t' proof (prove)
goal:
No subgoals!