theory Fastpath_C

lemma ccorres_call_hSkip':
  assumes  cul: "ccorres_underlying sr \<Gamma> r xf' r xf' P (i ` P') [SKIP] 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      csr: "\<And>x s t. (x, t) \<in> sr \<Longrightarrow> (x, 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     ares: "\<And>s t rv. r rv (xf' t) \<Longrightarrow> r rv (xf (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 r xf P P' [SKIP] 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 EHOther, rule exec.Skip, simp) apply clarsimp apply (erule exec_handlers.cases, simp_all)[1] apply (clarsimp elim!: exec_Normal_elim_cases) apply (clarsimp elim!: exec_Normal_elim_cases) apply (erule rev_bexI) apply (simp add: unif_rrel_simps csr ares) 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. ccorresG sr \<Gamma> r xf P P' [SKIP] 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)), SKIP],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]) r xf r xf 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>[SKIP],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 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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 = Suc 0) r xf r xf 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>[SKIP],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 = Suc 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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 = Suc 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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, SKIP],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>[SKIP],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 [SKIP]) r xf' r xf' ra t'a; ?n32 s sa za na t bdy t' \<le> length [SKIP]\<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 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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 (?z42 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>[SKIP],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>[SKIP],?z42 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>[SKIP],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 [SKIP]) r xf' r xf' ra t'a; ?n32 s sa za na t bdy t' \<le> length [SKIP]\<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 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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>[SKIP],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>[SKIP],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 [SKIP]) r xf' r xf' ra t'a; ?n32 s sa za na t bdy t' \<le> length [SKIP]\<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 0) r xf r xf 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 = Suc 0; 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 r xf 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>[SKIP],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'; Normal t' = Normal t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel (length [] = length [SKIP]) r xf' r xf' ra t'a; length [] \<le> length [SKIP]\<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 0) r xf r xf 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 = Suc 0; 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 r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa na t bdy t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>[SKIP],clean sa t'a\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel False r xf' r xf' ra t'a\<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 0) r xf r xf 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 = Suc 0; 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 r xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t bdy t'a ra ta h sb z n tb. \<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> Abrupt t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel False r xf' r xf' ra t'a; clean sa t'a = sb; SKIP = h; na = n; t = tb; \<Gamma>\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (n, tb)\<rbrakk> \<Longrightarrow> \<exists>t'. tb = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = Suc 0) r xf r xf ra t')
 2. \<And>s sa na t bdy t'a ra ta h sb tb. \<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> Abrupt t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel False r xf' r xf' ra t'a; clean sa t'a = sb; SKIP = h; na = 0; t = tb; \<Gamma>\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> tb; \<not> isAbr tb\<rbrakk> \<Longrightarrow> \<exists>t'. tb = 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 r xf 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 = Suc 0; 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 r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa na t bdy t'a ra ta h sb tb. \<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> Abrupt t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel False r xf' r xf' ra t'a; clean sa t'a = sb; SKIP = h; na = 0; t = tb; \<Gamma>\<turnstile> \<langle>SKIP,Normal sb\<rangle> \<Rightarrow> tb; \<not> isAbr tb\<rbrakk> \<Longrightarrow> \<exists>t'. tb = 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 r xf 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 = Suc 0; 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 r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa bdy t'a 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> Abrupt t'a; (ra, ta) \<in> fst (a s); (ta, t'a) \<in> sr; unif_rrel False r xf' r xf' ra t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, clean sa t'a) \<in> sr \<and> unif_rrel False r xf r xf ra (clean sa t'a)
 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 = Suc 0; 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 r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa bdy t'a 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> Abrupt t'a; (ta, t'a) \<in> sr; unif_rrel False r xf' r xf' ra t'a\<rbrakk> \<Longrightarrow> case (ra, ta) of (ra, t) \<Rightarrow> (t, clean sa t'a) \<in> sr \<and> unif_rrel False r xf r xf ra (clean sa t'a)
 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 = Suc 0; 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 r xf 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 = Suc 0; 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 r xf 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 r xf 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 r xf 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 r xf 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, SKIP],i sa\<rangle> \<Rightarrow> (?n98 s sa bdy t', ?x98 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'; ?x98 s sa bdy t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (?n98 s sa bdy t' = length [SKIP]) r xf' r xf' ra t'a; ?n98 s sa bdy t' \<le> length [SKIP]\<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 r xf 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 [SKIP] = length [SKIP]) r xf' r xf' ra t'a; length [SKIP] \<le> length [SKIP]\<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 r xf 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 [SKIP] = length [SKIP]) r xf' r xf' ra t'a; length [SKIP] \<le> length [SKIP]\<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 r xf 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, SKIP],i sa\<rangle> \<Rightarrow> (?n115 s sa (Fault fa) bdy fa, ?x115 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; ?x115 s sa t bdy fa = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n115 s sa t bdy fa = length [SKIP]) r xf' r xf' ra t'; ?n115 s sa t bdy fa \<le> length [SKIP]\<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 [SKIP] = length [SKIP]) r xf' r xf' ra t'; length [SKIP] \<le> length [SKIP]\<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 [SKIP] = length [SKIP]) r xf' r xf' ra t'; length [SKIP] \<le> length [SKIP]\<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, SKIP],i sa\<rangle> \<Rightarrow> (?n132 s sa Stuck bdy, ?x132 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; ?x132 s sa t bdy = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n132 s sa t bdy = length [SKIP]) r xf' r xf' ra t'; ?n132 s sa t bdy \<le> length [SKIP]\<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 [SKIP] = length [SKIP]) r xf' r xf' ra t'; length [SKIP] \<le> length [SKIP]\<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 [SKIP] = length [SKIP]) r xf' r xf' ra t'; length [SKIP] \<le> length [SKIP]\<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, SKIP],i sa\<rangle> \<Rightarrow> (?n149 s sa Stuck, ?x149 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; ?x149 s sa t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n149 s sa t = length [SKIP]) r xf' r xf' ra t'; ?n149 s sa t \<le> length [SKIP]\<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 [SKIP] = length [SKIP]) r xf' r xf' ra t'; length [SKIP] \<le> length [SKIP]\<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 [SKIP] = length [SKIP]) r xf' r xf' ra t'; length [SKIP] \<le> length [SKIP]\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!