theory Corres_UL_C

lemma ccorres_call:
  assumes  cul: "ccorres_underlying sr \<Gamma> r xf' rrel xf' P (i ` P') [] a (Call f)"
  and      gsr: "\<And>a b x s t. (x, t) \<in> sr \<Longrightarrow> (x, g a b (clean s t)) \<in> sr"
  and      res: "\<And>a s t rv. r rv (xf' t) \<Longrightarrow> r rv (xf (g a t (clean s t)))"
  and      ist: "\<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (call i f clean (\<lambda>x y. Basic (g x y)))" apply (rule ccorresI') apply (erule exec_handlers.cases, simp_all)[1] apply clarsimp apply (erule exec_call_Normal_elim, simp_all)[1] apply (clarsimp elim!: exec_Normal_elim_cases) apply (rule ccorresE[OF cul ist], assumption+, simp+) apply (rule EHAbrupt) apply (erule(1) exec.Call) apply (rule EHEmpty) apply simp apply clarsimp apply (erule exec_call_Normal_elim, simp_all)[1] apply (clarsimp elim!: exec_Normal_elim_cases) apply (rule ccorresE[OF cul ist], assumption+, simp+) apply (rule EHOther, erule(1) exec.Call) apply simp apply (simp add: unif_rrel_simps) apply (erule rev_bexI) apply (simp add: gsr res) apply (rule ccorresE[OF cul ist], assumption+, simp+) apply (rule EHOther, erule(1) exec.Call) apply simp apply simp apply (rule ccorresE[OF cul ist], assumption+, simp+) apply (rule EHOther, erule(1) exec.Call) apply simp apply simp apply (rule ccorresE[OF cul ist], assumption+, simp+) apply (rule EHOther, erule exec.CallUndefined) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (call i f clean (\<lambda>x y. Basic (g x y))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>call i f clean (\<lambda>x y. Basic (g x y)) # 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 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = na; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>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 = 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>x y. Basic (g x y)),Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>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 = 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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 bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> Abrupt za\<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 = length hs) r xf arrel axf ra t')
 2. \<And>s sa za na t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa 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 = length hs) 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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 bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa 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 = 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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 bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f],i sa\<rangle> \<Rightarrow> (?n32 s sa (clean sa t') na t bdy t', ?x32 s sa (clean sa t') na t bdy t')
 2. \<And>s sa za na t bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'; ?x32 s sa za na t bdy t' = Normal t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel (?n32 s sa za na t bdy t' = length []) r xf' rrel xf' ra t'a; ?n32 s sa za na t bdy t' \<le> length []\<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 = length hs) 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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 (4 subgoals):
 1. \<And>s sa za na t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal (i sa)\<rangle> \<Rightarrow> Abrupt (?z40 s sa za na t bdy t')
 2. \<And>s sa za na t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[],?z40 s sa za na t bdy t'\<rangle> \<Rightarrow> (?n32 s sa (clean sa t') na t bdy t', ?x32 s sa (clean sa t') na t bdy t')
 3. \<And>s sa za na t bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'; ?x32 s sa za na t bdy t' = Normal t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel (?n32 s sa za na t bdy t' = length []) r xf' rrel xf' ra t'a; ?n32 s sa za na t bdy t' \<le> length []\<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 = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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 bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[],t'\<rangle> \<Rightarrow> (?n32 s sa (clean sa t') na t bdy t', ?x32 s sa (clean sa t') na t bdy t')
 2. \<And>s sa za na t bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'; ?x32 s sa za na t bdy t' = Normal t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel (?n32 s sa za na t bdy t' = length []) r xf' rrel xf' ra t'a; ?n32 s sa za na t bdy t' \<le> length []\<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 = length hs) 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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 bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'; Abrupt t' = Normal t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel (0 = length []) r xf' rrel xf' ra t'a; 0 \<le> length []\<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 = 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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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); s' = sa; call i f clean (\<lambda>x y. Basic (g x y)) = h; n = length hs; z = t; \<Gamma>\<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); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>x y. Basic (g x y)),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 (4 subgoals):
 1. \<And>s sa t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> 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')
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, g sa t' (clean sa t')) \<in> sr \<and> unif_rrel True r xf arrel axf ra (g sa t' (clean sa t'))
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s sa bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f],i sa\<rangle> \<Rightarrow> (?n64 s sa bdy t', ?x64 s sa bdy t')
 2. \<And>s sa bdy t' t'a ra t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; ?x64 s sa bdy t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n64 s sa bdy t' = length []) r xf' rrel xf' ra t'a; ?n64 s sa bdy t' \<le> length []\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, g sa t' (clean sa t')) \<in> sr \<and> unif_rrel True r xf arrel axf ra (g sa t' (clean sa t'))
 3. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 5. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s sa bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<not> isAbr (Normal t')
 2. \<And>s sa bdy t' t'a ra t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'a; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, g sa t' (clean sa t')) \<in> sr \<and> unif_rrel True r xf arrel axf ra (g sa t' (clean sa t'))
 3. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 5. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa bdy t' t'a ra t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'a; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, g sa t' (clean sa t')) \<in> sr \<and> unif_rrel True r xf arrel axf ra (g sa t' (clean sa t'))
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa bdy t' t'a ra t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'a; t' = t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; r ra (xf' t'a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, g sa t'a (clean sa t'a)) \<in> sr \<and> r ra (xf (g sa t'a (clean sa t'a)))
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa bdy t' t'a ra t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'a; t' = t'a; (t, t'a) \<in> sr; r ra (xf' t'a)\<rbrakk> \<Longrightarrow> case (ra, t) of (ra, t) \<Rightarrow> (t, g sa t'a (clean sa t'a)) \<in> sr \<and> r ra (xf (g sa t'a (clean sa t'a)))
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f],i sa\<rangle> \<Rightarrow> (?n79 s sa (Fault fa) bdy fa, ?x79 s sa (Fault fa) bdy fa)
 2. \<And>s sa t bdy fa t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa; ?x79 s sa t bdy fa = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n79 s sa t bdy fa = length []) r xf' rrel xf' ra t'; ?n79 s sa t bdy fa \<le> length []\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> \<not> isAbr (Fault fa)
 2. \<And>s sa t bdy fa t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'; length [] \<le> length []\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s sa t bdy fa t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'; length [] \<le> length []\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f],i sa\<rangle> \<Rightarrow> (?n94 s sa Stuck bdy, ?x94 s sa Stuck bdy)
 2. \<And>s sa t bdy t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck; ?x94 s sa t bdy = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n94 s sa t bdy = length []) r xf' rrel xf' ra t'; ?n94 s sa t bdy \<le> length []\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> \<not> isAbr Stuck
 2. \<And>s sa t bdy t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'; length [] \<le> length []\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s sa t bdy t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'; length [] \<le> length []\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f],i sa\<rangle> \<Rightarrow> (?n109 s sa Stuck, ?x109 s sa Stuck)
 2. \<And>s sa t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck; ?x109 s sa t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n109 s sa t = length []) r xf' rrel xf' ra t'; ?n109 s sa t \<le> length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> \<not> isAbr Stuck
 2. \<And>s sa t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'; length [] \<le> length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s sa t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = None; t = Stuck; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length [] = length []) r xf' rrel xf' ra t'; length [] \<le> length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!