theory CCorresLemmas

lemma ccorres_cond_strong:
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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))
                              (R' \<inter> (Rt \<inter> P' \<union> Rf \<inter> - P'))
                              hs
                              (if P then a else b) (Cond P' c c')" apply (rule ccorresI') apply clarsimp apply (erule disjE) apply (drule exec_handlers_semantic_equivD1 [where b = c]) apply (rule semantic_equivI) apply (fastforce elim: exec_Normal_elim_cases intro: exec.CondTrue) apply (rule ccorresE [OF c1]) apply assumption apply (insert abs) apply fastforce apply fastforce apply fastforce apply simp apply (fastforce elim!: bexI [rotated]) apply (drule exec_handlers_semantic_equivD2 [where b = c']) apply (rule semantic_equivI) apply (fastforce elim: exec_Normal_elim_cases intro: exec.CondFalse) 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)) (R' \<inter> (Rt \<inter> P' \<union> Rf \<inter> - P')) 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> R' \<inter> (Rt \<inter> P' \<union> Rf \<inter> - P'); \<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> R'; s' \<in> Rt \<and> s' \<in> P' \<or> s' \<in> Rf \<and> s' \<notin> P'; 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (?s40 s s' n z, ?s'40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pt (?s40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> ?s'40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a (?s40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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'40 s s' n z\<rangle> \<Rightarrow> (?n40 s s' n z, ?x40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x40 s s' n z = Normal t'; (ra, t) \<in> fst (a (?s40 s s' n z)); (t, t') \<in> sr; unif_rrel (?n40 s s' n z = length hs) r xf arrel axf ra t'; ?n40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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> (?n40 s s' n z, ?x40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x40 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n40 s s' n z = length hs) r xf arrel axf ra t'; ?n40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n40 s s' n z, ?x40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x40 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n40 s s' n z = length hs) r xf arrel axf ra t'; ?n40 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n40 s s' n z, ?x40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x40 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n40 s s' n z = length hs) r xf arrel axf ra t'; ?n40 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n40 s s' n z, ?x40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x40 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n40 s s' n z = length hs) r xf arrel axf ra t'; ?n40 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n40 s s' n z, ?x40 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x40 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n40 s s' n z = length hs) r xf arrel axf ra t'; ?n40 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rt \<and> 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 \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 s'a. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (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'))) proof (prove)
goal (2 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (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'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (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'))) 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (?s146 s s' n z, ?s'146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pf (?s146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> ?s'146 s s' n z \<in> Rf
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (b (?s146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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'146 s s' n z\<rangle> \<Rightarrow> (?n146 s s' n z, ?x146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x146 s s' n z = Normal t'; (ra, t) \<in> fst (b (?s146 s s' n z)); (t, t') \<in> sr; unif_rrel (?n146 s s' n z = length hs) r xf arrel axf ra t'; ?n146 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'))) 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> (?n146 s s' n z, ?x146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x146 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n146 s s' n z = length hs) r xf arrel axf ra t'; ?n146 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'))) 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> s' \<in> Rf
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (b 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n146 s s' n z, ?x146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x146 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n146 s s' n z = length hs) r xf arrel axf ra t'; ?n146 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<not> snd (b 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n146 s s' n z, ?x146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x146 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n146 s s' n z = length hs) r xf arrel axf ra t'; ?n146 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n146 s s' n z, ?x146 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> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<longrightarrow> P = (s' \<in> P'); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); ?x146 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n146 s s' n z = length hs) r xf arrel axf ra t'; ?n146 s s' n z \<le> length hs; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 t' ra t. \<lbrakk>(s, s') \<in> sr; \<not> snd ((if P then a else b) s); R s; s' \<in> R'; P \<longrightarrow> Pt s; \<not> P \<longrightarrow> Pf s; s' \<in> Rf \<and> s' \<notin> P'; \<forall>s s'. (s, s') \<in> sr \<and> R s \<and> s' \<in> R' \<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 \<and> s' \<in> R' \<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:
No subgoals!