theory CCorresLemmas

lemma ccorres_from_vcg_split_throws:
  "\<lbrakk> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV;
     \<And>\<sigma>. \<Gamma> \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr}
              c UNIV,
         {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<rbrakk>
    \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (P' \<inter> R') (SKIP # hs) a (c ;; d)" apply (rule ccorres_guard_imp2) apply (rule ccorres_split_throws[rotated], assumption) apply (rule ccorres_from_vcg_throws[where P=P and P'="P' \<inter> R'"]) apply (rule allI) apply (erule_tac x=\<sigma> in meta_allE) apply (rule conseqPost) apply (erule HoarePartialProps.Merge_PostConj [OF conseqPre]) apply clarsimp apply assumption apply simp apply clarsimp apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (P' \<inter> R') (SKIP # hs) a (c;;
d) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' (SKIP # hs) a (c;;
d)
 2. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?P'3 (SKIP # hs) a c
 2. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?P'3 \<inter> R' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} c {},{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 2. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} c {},{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 2. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} c {},{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 2. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} c (?Q'11 \<sigma>),(?A'11 \<sigma>)
 2. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> ?Q'11 \<sigma> \<subseteq> {}
 3. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> ?A'11 \<sigma> \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 4. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} \<subseteq> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr}
 2. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?G15 \<sigma>\<^esub> (?P'15 \<sigma>) c (?R15 \<sigma>),(?X15 \<sigma>)
 3. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {} \<subseteq> ?G15 \<sigma>
 4. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} \<subseteq> ?P'15 \<sigma>
 5. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> UNIV \<inter> ?R15 \<sigma> \<subseteq> {}
 6. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<inter> ?X15 \<sigma> \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 7. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?G15 \<sigma>\<^esub> (?P'15 \<sigma>) c (?R15 \<sigma>),(?X15 \<sigma>)
 2. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {} \<subseteq> ?G15 \<sigma>
 3. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} \<subseteq> ?P'15 \<sigma>
 4. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> UNIV \<inter> ?R15 \<sigma> \<subseteq> {}
 5. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<inter> ?X15 \<sigma> \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 6. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {} \<subseteq> UNIV
 2. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} \<subseteq> R'
 3. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> UNIV \<inter> {} \<subseteq> {}
 4. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<inter> UNIV \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 5. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV \<Longrightarrow> {s. P \<sigma> \<and> s \<in> P' \<inter> R' \<and> (\<sigma>, s) \<in> sr} \<subseteq> R'
 2. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> UNIV \<inter> {} \<subseteq> {}
 3. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<inter> UNIV \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 4. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> UNIV \<inter> {} \<subseteq> {}
 2. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<inter> UNIV \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 3. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}\<rbrakk> \<Longrightarrow> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)} \<inter> UNIV \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}
 2. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {},UNIV; \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}; (s, s') \<in> sr; P s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> P' \<inter> R' \<inter> R' proof (prove)
goal:
No subgoals!