theory Refine_C

lemma ccorres_corres_u_xf:
  "\<lbrakk> ccorres rel xf P (Collect P') [] H C; no_fail P H \<rbrakk> \<Longrightarrow>
  corres_underlying rf_sr nf nf' rel P P' H ((exec_C \<Gamma> C) >>= (\<lambda>_. gets xf))" apply (clarsimp simp: ccorres_underlying_def corres_underlying_def) apply (drule (1) bspec) apply (clarsimp simp: exec_C_def no_fail_def) apply (drule_tac x = a in spec) apply (clarsimp simp:gets_def Nondet_Monad.bind_def get_def return_def) apply (rule conjI) apply clarsimp apply (erule_tac x=0 in allE) apply (erule_tac x="Normal y" in allE) apply simp apply (erule impE) apply (drule EHOther [where hs="[]"], simp) apply simp apply (simp add: unif_rrel_def) apply (clarsimp simp:image_def) apply (case_tac xs, simp_all) apply (fastforce intro: EHAbrupt EHEmpty) apply (fastforce intro: EHOther)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres rel xf P (Collect P') [] H C; no_fail P H\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' rel P P' H (do _ <- exec_C \<Gamma> C;
gets xf
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False)); no_fail P H; (a, b) \<in> rf_sr; P a; P' b; nf \<longrightarrow> \<not> snd (H a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((do _ <- exec_C \<Gamma> C;
gets xf
od) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> rel r r') \<and> (nf' \<longrightarrow> \<not> snd ((do _ <- exec_C \<Gamma> C;
gets xf
od) b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>no_fail P H; (a, b) \<in> rf_sr; P a; P' b; nf \<longrightarrow> \<not> snd (H a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((do _ <- exec_C \<Gamma> C;
gets xf
od) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> rel r r') \<and> (nf' \<longrightarrow> \<not> snd ((do _ <- exec_C \<Gamma> C;
gets xf
od) b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>s. P s \<longrightarrow> \<not> snd (H s); (a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((do _ <- \<lambda>s. ({()} \<times> {s'. \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Normal s'}, \<exists>xs. xs \<notin> range Normal \<and> \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> xs);
gets xf
od) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> rel r r') \<and> (nf' \<longrightarrow> \<not> snd ((do _ <- \<lambda>s. ({()} \<times> {s'. \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Normal s'}, \<exists>xs. xs \<notin> range Normal \<and> \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> xs);
gets xf
od) b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); P a \<longrightarrow> \<not> snd (H a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((do _ <- \<lambda>s. ({()} \<times> {s'. \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Normal s'}, \<exists>xs. xs \<notin> range Normal \<and> \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> xs);
gets xf
od) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> rel r r') \<and> (nf' \<longrightarrow> \<not> snd ((do _ <- \<lambda>s. ({()} \<times> {s'. \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Normal s'}, \<exists>xs. xs \<notin> range Normal \<and> \<Gamma>\<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> xs);
gets xf
od) b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> (\<forall>y. \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y \<longrightarrow> (\<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y))) \<and> (nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> \<forall>y. \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y \<longrightarrow> (\<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y))
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y; \<forall>t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (0, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (0 = length []) rel xf rel xf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y; \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (0, Normal y) \<longrightarrow> (case Normal y of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (0 = length []) rel xf rel xf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y; \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (0, Normal y) \<longrightarrow> (\<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> unif_rrel True rel xf rel xf r y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (3 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (0, Normal y)
 2. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y; \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> unif_rrel True rel xf rel xf r y\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 3. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (3 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (length [], Normal y)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (0, Normal y)
 2. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y; \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> unif_rrel True rel xf rel xf r y\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 3. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<not> snd (H a); \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Normal y; \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> unif_rrel True rel xf rel xf r y\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (H a). case x of (r, t) \<Rightarrow> (t, y) \<in> rf_sr \<and> rel r (xf y)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs) proof (prove)
goal (1 subgoal):
 1. \<And>a b xs. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); nf'; \<forall>x. xs \<noteq> Normal x; \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> xs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b xs x2. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); nf'; \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Abrupt x2; xs = Abrupt x2\<rbrakk> \<Longrightarrow> False
 2. \<And>a b xs x3. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); nf'; \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Fault x3; xs = Fault x3\<rbrakk> \<Longrightarrow> False
 3. \<And>a b xs. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); nf'; \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Stuck; xs = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b xs x3. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); nf'; \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Fault x3; xs = Fault x3\<rbrakk> \<Longrightarrow> False
 2. \<And>a b xs. \<lbrakk>(a, b) \<in> rf_sr; P a; P' b; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[C],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) rel xf rel xf r s'' | _ \<Rightarrow> False); \<not> snd (H a); nf'; \<Gamma>\<turnstile> \<langle>C,Normal b\<rangle> \<Rightarrow> Stuck; xs = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!