theory VSpace_C

lemma ccorres_from_vcg_might_throw:
  "(\<forall>\<sigma>. Gamm \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c
                 {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> r rv (xf s)},
                 {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)})
     \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' (SKIP # hs) a c" apply (rule ccorresI') apply (drule_tac x=s in spec) apply (erule exec_handlers.cases, simp_all) apply clarsimp apply (erule exec_handlers.cases, simp_all)[1] apply (auto elim!: exec_Normal_elim_cases)[1] apply (drule(1) exec_abrupt[rotated]) apply simp apply (clarsimp simp: unif_rrel_simps elim!: exec_Normal_elim_cases) apply fastforce apply (clarsimp simp: unif_rrel_simps) apply (drule hoare_sound) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. Gamm\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> r rv (xf s)},{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' (SKIP # hs) a c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<forall>\<sigma>. Gamm\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> r rv (xf s)},{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>c # 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; P s; s' \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>c # SKIP # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); Gamm\<turnstile> {sa. P s \<and> sa \<in> P' \<and> (s, sa) \<in> sr} c {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}\<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 (2 subgoals):
 1. \<And>s s' n z h sa za na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = na; z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; Gamm\<turnstile>\<^sub>h \<langle>SKIP # hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (2 subgoals):
 1. \<And>s sa za na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt za; Gamm\<turnstile>\<^sub>h \<langle>SKIP # hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t h sb z n ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt sb; za = sb; SKIP = h; na = n; t = ta; Gamm\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> Abrupt z; Gamm\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, ta)\<rbrakk> \<Longrightarrow> \<exists>t'. ta = 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 sa za na t h sb ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt sb; za = sb; SKIP = h; na = length hs; t = ta; Gamm\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<exists>t'. ta = 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')
 3. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (2 subgoals):
 1. \<And>s sa za na t h sb ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt sb; za = sb; SKIP = h; na = length hs; t = ta; Gamm\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<exists>t'. ta = 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 h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t h sb ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; za = sb; SKIP = h; na = length hs; t = ta; Gamm\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> sa \<in> {sa \<in> P'. (s, sa) \<in> sr}
 2. \<And>s sa za na t h sb ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; za = sb; SKIP = h; na = length hs; t = ta; Gamm\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> ta; \<not> isAbr ta; sb \<in> {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. ta = 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')
 3. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (2 subgoals):
 1. \<And>s sa za na t h sb ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; za = sb; SKIP = h; na = length hs; t = ta; Gamm\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> ta; \<not> isAbr ta; sb \<in> {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. ta = 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 h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (2 subgoals):
 1. \<And>s sa sb aa b. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; (aa, b) \<in> fst (a s); (b, sb) \<in> sr; arrel aa (axf sb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, sb) \<in> sr \<and> arrel r (axf sb)
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} h {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; s' = sa; c = h; n = Suc (length hs); z = t; Gamm\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = 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') proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}; Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra (xf t')) proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t; Gamm,{}\<Turnstile>\<^bsub>/{}\<^esub> {sa \<in> P'. (s, sa) \<in> sr} c {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)},{sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra (xf t')) proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); Gamm\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t; \<forall>sa t. Gamm\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> sr} \<longrightarrow> t \<in> Normal ` {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> r rv (xf sa)} \<or> t \<in> Abrupt ` {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> sr \<and> arrel rv (axf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra (xf t')) proof (prove)
goal:
No subgoals!