theory CCorresLemmas

lemma ccorres_cond:
  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)) ((Rt \<inter> P') \<union> (Rf \<inter> - P')) hs (if P then a else b) (Cond P' c c')" apply (rule ccorresI') apply (erule UnE) 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: ccorresE [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 (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: ccorresE [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)) (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> 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 (2 subgoals):
 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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'\<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')
 2. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (3 subgoals):
 1. \<And>s s' n z s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 3. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (3 subgoals):
 1. \<And>s s' n z s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 3. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (2 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 2. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (2 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 2. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (7 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (?s33 s s' n z, ?s'33 s s' n z) \<in> sr
 2. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> Pt (?s33 s s' n z)
 3. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> ?s'33 s s' n z \<in> Rt
 4. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<not> snd (a (?s33 s s' n z))
 5. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,?s'33 s s' n z\<rangle> \<Rightarrow> (?n33 s s' n z, ?x33 s s' n z)
 6. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x33 s s' n z = Normal t'; (ra, t) \<in> fst (a (?s33 s s' n z)); (t, t') \<in> sr; unif_rrel (?n33 s s' n z = length hs) r xf arrel axf ra t'; ?n33 s s' n z \<le> length hs\<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')
 7. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (6 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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> (?n33 s s' n z, ?x33 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x33 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n33 s s' n z = length hs) r xf arrel axf ra t'; ?n33 s s' n z \<le> length hs\<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')
 6. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - P'\<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 (6 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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> (?n33 s s' n z, ?x33 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x33 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n33 s s' n z = length hs) r xf arrel axf ra t'; ?n33 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>(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')
 6. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (5 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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> (?n33 s s' n z, ?x33 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x33 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n33 s s' n z = length hs) r xf arrel axf ra t'; ?n33 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>(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')
 5. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (4 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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> (?n33 s s' n z, ?x33 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x33 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n33 s s' n z = length hs) r xf arrel axf ra t'; ?n33 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>(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')
 4. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (3 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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> (?n33 s s' n z, ?x33 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); ?x33 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n33 s s' n z = length hs) r xf arrel axf ra t'; ?n33 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>(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')
 3. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (2 subgoals):
 1. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rt \<inter> 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> \<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')
 2. \<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; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (2 subgoals):
 1. \<And>s s' n z s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (2 subgoals):
 1. \<And>s s' n z s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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 (6 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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> (?s139 s s' n z, ?s'139 s s' n z) \<in> sr
 2. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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 (?s139 s s' n z)
 3. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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'139 s s' n z \<in> Rf
 4. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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 (?s139 s s' n z))
 5. \<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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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'139 s s' n z\<rangle> \<Rightarrow> (?n139 s s' n z, ?x139 s s' n z)
 6. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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); ?x139 s s' n z = Normal t'; (ra, t) \<in> fst (b (?s139 s s' n z)); (t, t') \<in> sr; unif_rrel (?n139 s s' n z = length hs) r xf arrel axf ra t'; ?n139 s s' n z \<le> length hs\<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 (5 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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> (?n139 s s' n z, ?x139 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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); ?x139 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n139 s s' n z = length hs) r xf arrel axf ra t'; ?n139 s s' n z \<le> length hs\<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 (4 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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> (?n139 s s' n z, ?x139 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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); ?x139 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n139 s s' n z = length hs) r xf arrel axf ra t'; ?n139 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>(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 (3 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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> (?n139 s s' n z, ?x139 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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); ?x139 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n139 s s' n z = length hs) r xf arrel axf ra t'; ?n139 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>(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 (2 subgoals):
 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; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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> (?n139 s s' n z, ?x139 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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); ?x139 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> sr; unif_rrel (?n139 s s' n z = length hs) r xf arrel axf ra t'; ?n139 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>(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 t' ra t. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P \<longrightarrow> Pt s) and (\<lambda>s. \<not> P \<longrightarrow> Pf s)) s; \<not> snd ((if P then a else b) s); s' \<in> Rf \<inter> - 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>(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:
No subgoals!