theory CCorresLemmas

lemma ccorres_cond2:
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P  = (s' \<in> P') "
  and     c1: "ccorres_underlying sr \<Gamma> r xf arrel axf Pt Rt hs a c"
  and     c2: "ccorres_underlying sr \<Gamma> r xf arrel axf Pf Rf hs b c'"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s))
                    {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)} hs (if P then a else b) (Cond P' c c')" apply (rule ccorresI') apply clarsimp apply (case_tac " s' \<in> P'", clarsimp) apply (drule exec_handlers_semantic_equivD1 [where b = c]) apply (rule semantic_equivI) apply (fastforce elim: exec_Normal_elim_cases intro: exec.CondTrue) 
(* the following works but takes a while:
   apply (insert abs)
   apply (fastforce elim: ccorres_underlyingE [OF c1] elim!: bexI [rotated])
*)
    apply (rule ccorresE [OF c1]) apply assumption apply (insert abs) apply fastforce apply fastforce apply fastforce apply simp apply (fastforce elim!: bexI [rotated]) apply clarsimp apply (drule exec_handlers_semantic_equivD2 [where b = c']) apply (rule semantic_equivI) apply (fastforce elim: exec_Normal_elim_cases intro: exec.CondFalse) 

(* the following works but takes a while:
  apply (fastforce elim: ccorres_underlyingE [OF c2] elim!: bexI [rotated]) *)
   apply (rule ccorresE [OF c2]) apply assumption apply (insert abs, fastforce) apply fastforce apply fastforce apply simp apply (fastforce elim!: bexI[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)} hs (if P then a else b) (Cond P' c c') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; s' \<in> {s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)}; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((if P then a else b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z s'a. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a (Cond P' c c') c
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z s'a. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond P' c c',Normal s'\<rangle> \<Rightarrow> s'a = \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> s'a
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (7 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (?s39 s s' n z, ?s'39 s s' n z) \<in> sr
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pt (?s39 s s' n z)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> ?s'39 s s' n z \<in> Rt
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a (?s39 s s' n z))
 5. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,?s'39 s s' n z\<rangle> \<Rightarrow> (?n39 s s' n z, ?x39 s s' n z)
 6. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x39 s s' n z = Normal t'; (ra, t) \<in> fst (a (?s39 s s' n z)); (t, t') \<in> sr; unif_rrel (?n39 s s' n z = length hs) r xf arrel axf ra t'; ?n39 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 7. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (6 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pt s
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> s' \<in> Rt
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n39 s s' n z, ?x39 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x39 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n39 s s' n z = length hs) r xf arrel axf ra t'; ?n39 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 6. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (6 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> Pt s
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> s' \<in> Rt
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n39 s s' n z, ?x39 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x39 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n39 s s' n z = length hs) r xf arrel axf ra t'; ?n39 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 6. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (5 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> s' \<in> Rt
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n39 s s' n z, ?x39 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x39 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n39 s s' n z = length hs) r xf arrel axf ra t'; ?n39 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 5. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n39 s s' n z, ?x39 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x39 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n39 s s' n z = length hs) r xf arrel axf ra t'; ?n39 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n39 s s' n z, ?x39 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x39 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n39 s s' n z = length hs) r xf arrel axf ra t'; ?n39 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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 t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> Rt; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')))
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); R s; s' \<in> P' \<longrightarrow> s' \<in> Rt; s' \<notin> P' \<longrightarrow> s' \<in> Rf; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> (P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) \<and> (\<not> P \<longrightarrow> (\<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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 s'a. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a c' (Cond P' c c')
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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 s'a. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> s'a = \<Gamma>\<turnstile> \<langle>Cond P' c c',Normal s'\<rangle> \<Rightarrow> s'a
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (6 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (?s115 s s' n z, ?s'115 s s' n z) \<in> sr
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pf (?s115 s s' n z)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> ?s'115 s s' n z \<in> Rf
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (b (?s115 s s' n z))
 5. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,?s'115 s s' n z\<rangle> \<Rightarrow> (?n115 s s' n z, ?x115 s s' n z)
 6. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x115 s s' n z = Normal t'; (ra, t) \<in> fst (b (?s115 s s' n z)); (t, t') \<in> sr; unif_rrel (?n115 s s' n z = length hs) r xf arrel axf ra t'; ?n115 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pf s
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> s' \<in> Rf
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (b s)
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n115 s s' n z, ?x115 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x115 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n115 s s' n z = length hs) r xf arrel axf ra t'; ?n115 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> s' \<in> Rf
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (b s)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n115 s s' n z, ?x115 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x115 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n115 s s' n z = length hs) r xf arrel axf ra t'; ?n115 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (b s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n115 s s' n z, ?x115 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x115 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n115 s s' n z = length hs) r xf arrel axf ra t'; ?n115 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (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. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n115 s s' n z, ?x115 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x115 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n115 s s' n z = length hs) r xf arrel axf ra t'; ?n115 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd (b s); R s; s' \<in> Rf; Pf s; s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!