theory Ipc_C

lemma ccorres_break_return:
  assumes r: "\<And>s s'. \<lbrakk> (s,s') \<in> rf_sr; P s; s' \<in> P' \<rbrakk> \<Longrightarrow> r n (xf s')"
  assumes xf: "\<And>s. xf (global_exn_var_'_update (\<lambda>_. Break) s) = xf s"
  shows "ccorres r xf P P' (catchbrk_C#hs) (return n) break_C" apply (simp add: throwError_def cbreak_def) apply (clarsimp simp: ccorres_underlying_def return_def split: xstate.splits) apply (frule (2) r) apply (rule conjI) apply clarsimp apply (erule exec_handlers.cases, simp_all)[1] apply clarsimp apply (erule exec_elim_cases, simp_all)[1] apply (erule exec_elim_cases, simp_all)[1] apply clarsimp apply (erule exec_elim_cases, simp_all)[1] apply clarsimp apply (erule exec_handlers.cases, simp_all)[1] apply (clarsimp simp: catchbrk_C_def) apply (erule exec_elim_cases, simp_all)[1] apply (erule exec_elim_cases, simp_all)[1] apply clarsimp apply (clarsimp simp: catchbrk_C_def) apply (erule exec_elim_cases, simp_all)[1] apply clarsimp apply (erule exec_elim_cases, simp_all)[1] apply (clarsimp simp: unif_rrel_def xf) apply clarsimp apply clarsimp apply (erule exec_elim_cases, simp_all)[1] apply (erule exec_elim_cases, simp_all)[1] apply (erule exec_elim_cases, simp_all)[1] apply (rule conjI, clarsimp) apply (erule exec_handlers.cases, simp_all)[1] apply clarsimp apply ((erule exec_elim_cases, simp_all)[1])+ apply (clarsimp simp: catchbrk_C_def) apply (erule exec_handlers.cases, simp_all)[1] apply (auto elim: exec_elim_cases)[3] apply (rule conjI, clarsimp) apply (erule exec_handlers.cases, simp_all)[1] apply clarsimp apply ((erule exec_elim_cases, simp_all)[1])+ apply (clarsimp simp: catchbrk_C_def) apply (erule exec_handlers.cases, simp_all)[1] apply (auto elim: exec_elim_cases)[3] apply clarsimp apply (erule exec_handlers.cases, simp_all)[1] apply clarsimp apply ((erule exec_elim_cases, simp_all)[1])+ apply (clarsimp simp: catchbrk_C_def) apply (erule exec_handlers.cases, simp_all)[1] apply (auto elim!: exec_elim_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' (catchbrk_C # hs) (return n) break_C proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' (catchbrk_C # hs) (return n) (\<acute>global_exn_var :== Break;;
THROW) proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Normal x1) \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Normal x1) \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> \<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Normal x1) \<longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b na x1. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b); \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Normal x1)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a b na x1 h s z naa t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = naa; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (naa, t)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (naa = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 s z na. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break;;
THROW,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Normal x1)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 s z na sa s'. \<lbrakk>(a, sa) \<in> rf_sr; P a; sa \<in> P'; r n (xf sa); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Normal x1); s = sa; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break,Normal sa\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>THROW,s'\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 s z na sa s' sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Normal x1); s = sb; \<Gamma>\<turnstile> \<langle>THROW,Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rangle> \<Rightarrow> Abrupt z; sa = sb; s' = Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 z na sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Normal x1); \<Gamma>\<turnstile> \<langle>THROW,Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 z na sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,s\<rangle> \<Rightarrow> (na, Normal x1); sb\<lparr>global_exn_var_' := Break\<rparr> = s; z = s\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 na sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,sb\<lparr>global_exn_var_' := Break\<rparr>\<rangle> \<Rightarrow> (na, Normal x1)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x1 na sb h s z nb t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; catchbrk_C = h; na = nb; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (nb, t)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (nb = Suc (length hs)) r xf r xf n x1
 2. \<And>a x1 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; catchbrk_C = h; na = length hs; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 3. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x1 sb z na. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile> \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI,Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x1)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a x1 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; catchbrk_C = h; na = length hs; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 3. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (5 subgoals):
 1. \<And>a x1 sb z na s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x1); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s = Break; \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a x1 sb z na s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x1); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s \<noteq> Break; \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 3. \<And>a x1 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; catchbrk_C = h; na = length hs; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 4. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 5. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x1 sb z na s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x1); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s \<noteq> Break; \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel (na = Suc (length hs)) r xf r xf n x1
 2. \<And>a x1 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; catchbrk_C = h; na = length hs; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 3. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; catchbrk_C = h; na = length hs; Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile> \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI,Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x1 sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s = Break; \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 2. \<And>a x1 sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s \<noteq> Break; \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 3. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x1 sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile> \<langle>SKIP,Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 2. \<And>a x1 sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s \<noteq> Break; \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 3. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x1 sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; x1 = s\<rbrakk> \<Longrightarrow> (a, s) \<in> rf_sr \<and> unif_rrel False r xf r xf n s
 2. \<And>a x1 sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s \<noteq> Break; \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 3. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x1 sb s. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; global_exn_var_' s \<noteq> Break; \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel False r xf r xf n x1
 2. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b na x1 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Normal x1 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a x1 s. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break;;
THROW,Normal s\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a x1 s sa s'. \<lbrakk>(a, sa) \<in> rf_sr; P a; sa \<in> P'; r n (xf sa); s = sa; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break,Normal sa\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>THROW,s'\<rangle> \<Rightarrow> Normal x1\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a x1 s sa s' sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); s = sb; \<Gamma>\<turnstile> \<langle>THROW,Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rangle> \<Rightarrow> Normal x1; sa = sb; s' = Normal (sb\<lparr>global_exn_var_' := Break\<rparr>)\<rbrakk> \<Longrightarrow> (a, x1) \<in> rf_sr \<and> unif_rrel True r xf r xf n x1
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b na x2. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b); \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Abrupt x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a b na x2 h s z naa t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = naa; Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (naa, t)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x2 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x2 s z na. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break;;
THROW,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Abrupt x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x2 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x2 s z na sa s' sb sc. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,sc\<rangle> \<Rightarrow> (na, Abrupt x2); s = sb; sa = sb; s' = Normal sc; sb\<lparr>global_exn_var_' := Break\<rparr> = sc; z = sc\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x2 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (3 subgoals):
 1. \<And>a x2 na sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,sb\<lparr>global_exn_var_' := Break\<rparr>\<rangle> \<Rightarrow> (na, Abrupt x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x2 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (4 subgoals):
 1. \<And>a x2 na sb h s z nb t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; na = nb; Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (nb, t)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x2 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; na = length hs; Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na x2 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Abrupt x2 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (2 subgoals):
 1. \<And>a b na x3. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b); \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Fault x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (3 subgoals):
 1. \<And>a b na x3 h s z naa t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = naa; Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (naa, t)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x3 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (3 subgoals):
 1. \<And>a x3 s z na. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break;;
THROW,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Fault x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x3 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (3 subgoals):
 1. \<And>a x3 s z na sa s' sb sc. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,sc\<rangle> \<Rightarrow> (na, Fault x3); s = sb; sa = sb; s' = Normal sc; sb\<lparr>global_exn_var_' := Break\<rparr> = sc; z = sc\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x3 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (3 subgoals):
 1. \<And>a x3 na sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,sb\<lparr>global_exn_var_' := Break\<rparr>\<rangle> \<Rightarrow> (na, Fault x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na x3 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (4 subgoals):
 1. \<And>a x3 na sb h s z nb t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; na = nb; Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (nb, t)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x3 na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; na = length hs; Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na x3 h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Fault x3 = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 4. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b)\<rbrakk> \<Longrightarrow> t = Stuck \<longrightarrow> (b, (\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs, na, Stuck) \<notin> exec_handlers \<Gamma> proof (prove)
goal (1 subgoal):
 1. \<And>a b na. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; r n (xf b); \<Gamma>\<turnstile>\<^sub>h \<langle>(\<acute>global_exn_var :== Break;;
THROW) # catchbrk_C # hs,b\<rangle> \<Rightarrow> (na, Stuck)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b na h s z naa t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = naa; Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (naa, Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a s z na. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Break;;
THROW,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,z\<rangle> \<Rightarrow> (na, Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a s z na sa s' sb sc. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>catchbrk_C # hs,sc\<rangle> \<Rightarrow> (na, Stuck); s = sb; sa = sb; s' = Normal sc; sb\<lparr>global_exn_var_' := Break\<rparr> = sc; z = sc\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a na sb. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,sb\<lparr>global_exn_var_' := Break\<rparr>\<rangle> \<Rightarrow> (na, Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b na h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a na sb h s z nb t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; na = nb; Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (nb, Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a na sb h s t. \<lbrakk>(a, sb) \<in> rf_sr; P a; sb \<in> P'; r n (xf sb); sb\<lparr>global_exn_var_' := Break\<rparr> = s; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI = h; na = length hs; Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a b na h s t. \<lbrakk>(a, s) \<in> rf_sr; P a; s \<in> P'; r n (xf s); b = s; (\<acute>global_exn_var :== Break;;
THROW) = h; na = Suc (length hs); Stuck = t; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!