theory Ipc_C

lemma ccorres_emptyOnFailure:
  assumes corr_ac: "ccorres (\<lambda>f c. case f of Inl _ \<Rightarrow> r [] c | Inr xs \<Rightarrow> r xs c)
                            xf
                            P P' hs a c"
  shows "ccorres r xf P P' hs (emptyOnFailure a) c" using corr_ac apply (simp add: emptyOnFailure_def catch_def const_def bind_def split_def) apply (clarsimp simp: ccorres_underlying_def return_def split: xstate.splits sum.splits) apply (drule (1) bspec) apply (rule conjI, clarsimp) apply (erule_tac x=n in allE) apply (rename_tac s) apply (erule_tac x="Normal s" in allE) apply clarsimp apply (rule bexI) prefer 2 apply assumption apply clarsimp apply (rule conjI, clarsimp simp: unif_rrel_def) apply (clarsimp simp: unif_rrel_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' hs (emptyOnFailure a) c proof (prove)
using this:
ccorres (\<lambda>f c. case f of Inl x \<Rightarrow> r [] c | Inr xs \<Rightarrow> r xs c) xf P P' hs a c

goal (1 subgoal):
 1. ccorres r xf P P' hs (emptyOnFailure a) c proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>f c. case f of Inl x \<Rightarrow> r [] c | Inr xs \<Rightarrow> r xs c) xf P P' hs a c \<Longrightarrow> ccorres r xf P P' hs (\<lambda>s. (\<Union>x\<in>fst (a s). fst ((case fst x of Inl e \<Rightarrow> return [] | Inr x \<Rightarrow> return x) (snd x)), (\<exists>x\<in>fst (a s). snd ((case fst x of Inl e \<Rightarrow> return [] | Inr x \<Rightarrow> return x) (snd x))) \<or> snd (a s))) c proof (prove)
goal (1 subgoal):
 1. \<And>aa b n t. \<lbrakk>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>)); (aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] x1) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 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>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] x1) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 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>aa b n x1. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<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 (a aa). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf ra 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>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] x1) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 x1)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n x1. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal x1); \<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 (a aa). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf ra 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>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] x1) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 x1)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n s. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<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 (a aa). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf ra 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>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 s)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n s. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<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 (a aa). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf ra 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>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 s)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a aa). ((\<exists>x1. fst y = Inl x1) \<longrightarrow> (snd y, s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. fst y = Inr x2 \<longrightarrow> (snd y, s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 s)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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 (3 subgoals):
 1. \<And>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> ((\<exists>x1. fst (?y203 aa b n s aaa ba) = Inl x1) \<longrightarrow> (snd (?y203 aa b n s aaa ba), s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. fst (?y203 aa b n s aaa ba) = Inr x2 \<longrightarrow> (snd (?y203 aa b n s aaa ba), s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 s)
 2. \<And>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> ?y203 aa b n s aaa ba \<in> fst (a aa)
 3. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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 (3 subgoals):
 1. \<And>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> ?y203 aa b n s aaa ba \<in> fst (a aa)
 2. \<And>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> ((\<exists>x1. fst (?y203 aa b n s aaa ba) = Inl x1) \<longrightarrow> (snd (?y203 aa b n s aaa ba), s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. fst (?y203 aa b n s aaa ba) = Inr x2 \<longrightarrow> (snd (?y203 aa b n s aaa ba), s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 s)
 3. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> ((\<exists>x1. fst (aaa, ba) = Inl x1) \<longrightarrow> (snd (aaa, ba), s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. fst (aaa, ba) = Inr x2 \<longrightarrow> (snd (aaa, ba), s) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf x2 s)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> ((\<exists>x1. aaa = Inl x1) \<longrightarrow> unif_rrel (n = length hs) r xf r xf [] s) \<and> (\<forall>x2. aaa = Inr x2 \<longrightarrow> unif_rrel (n = length hs) r xf r xf x2 s)
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n s aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal s); (aaa, ba) \<in> fst (a aa); (ba, s) \<in> rf_sr; unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf aaa s\<rbrakk> \<Longrightarrow> \<forall>x2. aaa = Inr x2 \<longrightarrow> unif_rrel (n = length hs) r xf r xf x2 s
 2. \<And>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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>aa b n t. \<lbrakk>(aa, b) \<in> rf_sr; P aa; b \<in> P'; \<not> snd (a aa); case (aa, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). case x of (ra, ta) \<Rightarrow> (ta, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) xf (\<lambda>f c. ((\<exists>x1. f = Inr x1) \<or> r [] c) \<and> (\<forall>x2. f = Inr x2 \<longrightarrow> r x2 c)) 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>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:
No subgoals!