theory SyscallArgs_C

lemma ccorres_defer:
  assumes c: "ccorres r xf P P' hs H C"
  assumes f: "no_fail Q H"
  shows "ccorres (\<lambda>_. r rv) xf (\<lambda>s. P s \<and> Q s \<and> (P s \<and> Q s \<longrightarrow> fst (H s) = {(rv,s)})) P' hs (return ()) C" using c apply (clarsimp simp: ccorres_underlying_def split: xstate.splits) apply (drule (1) bspec) apply clarsimp apply (erule impE) apply (insert f)[1] apply (clarsimp simp: no_fail_def) apply (clarsimp simp: return_def) apply (rule conjI) apply clarsimp apply (rename_tac s) apply (erule_tac x=n in allE) apply (erule_tac x="Normal s" in allE) apply (clarsimp simp: unif_rrel_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>_. r rv) xf (\<lambda>s. P s \<and> Q s \<and> (P s \<and> Q s \<longrightarrow> fst (H s) = {(rv, s)})) P' hs (return ()) C proof (prove)
using this:
ccorres r xf P P' hs H C

goal (1 subgoal):
 1. ccorres (\<lambda>_. r rv) xf (\<lambda>s. P s \<and> Q s \<and> (P s \<and> Q s \<longrightarrow> fst (H s) = {(rv, s)})) P' hs (return ()) C proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (H s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (s', C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)); (a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (return () a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; case (a, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (H s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (s', C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>))\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (return () a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<not> snd (H a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>))\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (return () a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'\<rbrakk> \<Longrightarrow> \<not> snd (H a)
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (return () a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; no_fail Q H\<rbrakk> \<Longrightarrow> \<not> snd (H a)
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (return () a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (return () a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> \<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n x1. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1)\<rbrakk> \<Longrightarrow> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () x1
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n s. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal s)\<rbrakk> \<Longrightarrow> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () s
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n s. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal s); \<forall>t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () s
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b n s. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal s); (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal s) \<longrightarrow> (\<forall>x1. Normal s = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. Normal s \<noteq> Abrupt x2) \<or> (b, C # hs, n, Normal s) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. Normal s \<noteq> Fault x3) \<or> (b, C # hs, n, Normal s) \<notin> exec_handlers \<Gamma>) \<and> (Normal s = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> unif_rrel (n = length hs) (\<lambda>_. r rv) xf (\<lambda>_. r rv) xf () s
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; Q a; fst (H a) = {(rv, a)}; b \<in> P'; \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf rv x1)) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal:
No subgoals!