theory Detype_C

lemma ccorres_stateAssert_after:
  assumes "ccorres r xf (P and (\<lambda>s. (\<forall>(rv,s') \<in> fst (f s). R s'))) P' hs f c"
  shows "ccorres r xf P P' hs (do _ \<leftarrow> f; stateAssert R vs od) c" using assms apply (clarsimp simp: ccorres_underlying_def split: xstate.splits) apply (drule snd_stateAssert_after) apply clarsimp apply (drule (1) bspec) apply (clarsimp simp: split_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 apply (simp add: bind_def stateAssert_def get_def assert_def) apply (rule bexI) prefer 2 apply assumption apply (clarsimp simp: return_def fail_def) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' hs (do _ <- f;
stateAssert R vs
od) c proof (prove)
using this:
ccorres r xf (P and (\<lambda>s. \<forall>(rv, s')\<in>fst (f s). R s')) P' hs f c

goal (1 subgoal):
 1. ccorres r xf P P' hs (do _ <- f;
stateAssert R vs
od) 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> (\<forall>x\<in>fst (f s). case x of (rv, x) \<Rightarrow> R x) \<and> s' \<in> P' \<and> \<not> snd (f 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 (f s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd ((do _ <- f;
stateAssert R vs
od) a)\<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 ((do _ <- f;
stateAssert R vs
od) a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r 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>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> (\<forall>x\<in>fst (f s). case x of (rv, x) \<Rightarrow> R x) \<and> s' \<in> P' \<and> \<not> snd (f 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 (f s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a) \<and> (\<forall>(rv, s')\<in>fst (f a). R s')\<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 ((do _ <- f;
stateAssert R vs
od) a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r 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>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> (\<forall>x\<in>fst (f s). case x of (rv, x) \<Rightarrow> R x) \<and> s' \<in> P' \<and> \<not> snd (f 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 (f s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). case x of (rv, s') \<Rightarrow> R s'\<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 ((do _ <- f;
stateAssert R vs
od) a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). case x of (rv, s') \<Rightarrow> R s'; case (a, b) of (s, s') \<Rightarrow> P s \<and> (\<forall>x\<in>fst (f s). case x of (rv, x) \<Rightarrow> R x) \<and> s' \<in> P' \<and> \<not> snd (f 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 (f s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf () 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 ((do _ <- f;
stateAssert R vs
od) a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 ((do _ <- f;
stateAssert R vs
od) a). (snd x, x1) \<in> rf_sr)) \<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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 ((do _ <- f;
stateAssert R vs
od) a). (snd x, x1) \<in> rf_sr)
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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> \<exists>x\<in>fst ((do _ <- f;
stateAssert R vs
od) a). (snd x, x1) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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> \<exists>x\<in>fst ((do _ <- f;
stateAssert R vs
od) a). (snd x, s) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<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> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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> \<exists>x\<in>fst ((do _ <- f;
stateAssert R vs
od) a). (snd x, s) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<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> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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> \<exists>x\<in>fst ((do _ <- f;
stateAssert R vs
od) a). (snd x, s) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do _ <- f;
stateAssert R vs
od) a). (snd x, s) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (f a). \<exists>x\<in>fst (case y of (uu_, s) \<Rightarrow> (if R s then return () else fail) s). (snd x, s) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 (3 subgoals):
 1. \<And>a b n s ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ?y89 a b n s ba of (uu_, s) \<Rightarrow> (if R s then return () else fail) s). (snd x, s) \<in> rf_sr
 2. \<And>a b n s ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> ?y89 a b n s ba \<in> fst (f a)
 3. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 (3 subgoals):
 1. \<And>a b n s ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> ?y89 a b n s ba \<in> fst (f a)
 2. \<And>a b n s ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ?y89 a b n s ba of (uu_, s) \<Rightarrow> (if R s then return () else fail) s). (snd x, s) \<in> rf_sr
 3. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ((), ba) of (uu_, s) \<Rightarrow> (if R s then return () else fail) s). (snd x, s) \<in> rf_sr
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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 ba. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); unif_rrel (n = length hs) r xf r xf () s; ((), ba) \<in> fst (f a); (ba, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> R ba
 2. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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; b \<in> P'; \<not> snd (f a); \<forall>x\<in>fst (f a). R (snd x); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, x1) \<in> rf_sr) \<and> unif_rrel (n = length hs) r xf r xf () 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!