theory L4VerifiedLinks

lemma ac_corres_ccorres_underlying:
  "ac_corres st check_termination \<Gamma> rx G A B \<Longrightarrow>
   ccorres_underlying {(a, b). a = st b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr (\<lambda>_. True) (Collect G) [] A B" apply (clarsimp simp: ac_corres_def ccorres_underlying_def) apply (erule allE, erule impE, force) apply clarsimp apply (erule exec_handlers.cases) apply clarsimp apply (erule allE, erule (1) impE) apply clarsimp apply (case_tac hs) apply clarsimp apply (erule allE, erule (1) impE) apply (clarsimp split: xstate.splits) apply (erule bexI [rotated]) apply (clarsimp simp: unif_rrel_def) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ac_corres st check_termination \<Gamma> rx G A B \<Longrightarrow> ccorres_underlying {(a, b). a = st b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr (\<lambda>_. True) (Collect G) [] A B proof (prove)
goal (1 subgoal):
 1. \<And>b n t. \<lbrakk>\<forall>s. G s \<and> \<not> snd (A (st s)) \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st s)))) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s); G b; \<not> snd (A (st b)); \<Gamma>\<turnstile>\<^sub>h \<langle>[B],b\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b n t. \<lbrakk>G b; \<not> snd (A (st b)); \<Gamma>\<turnstile>\<^sub>h \<langle>[B],b\<rangle> \<Rightarrow> (n, t); (\<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b)))) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b n t. \<lbrakk>G b; \<not> snd (A (st b)); \<Gamma>\<turnstile>\<^sub>h \<langle>[B],b\<rangle> \<Rightarrow> (n, t); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b n t h s z hs na ta. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = na; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta hs. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s z na ta. \<lbrakk>G s; \<not> snd (A (st s)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st s))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (na = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta hs. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s z na ta. \<lbrakk>G s; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); \<exists>s'. Abrupt z = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st s))\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (na = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta hs. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b n t h s ta hs. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b n t h s ta hs. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = []\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta hs a list. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = a # list\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s ta. \<lbrakk>G s; \<not> snd (A (st s)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st s))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (0 = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta hs a list. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = a # list\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s ta. \<lbrakk>G s; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; \<exists>s'. ta = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st s))\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (0 = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta hs a list. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = a # list\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>G s; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Normal s'; (Inr (rx s'), st s') \<in> fst (A (st s))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (A (st s)). case x of (r, t) \<Rightarrow> t = st s' \<and> unif_rrel True ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'
 2. \<And>b n t h s ta hs a list. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = a # list\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>G s; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Normal s'\<rbrakk> \<Longrightarrow> case (Inr (rx s'), st s') of (r, t) \<Rightarrow> t = st s' \<and> unif_rrel True ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'
 2. \<And>b n t h s ta hs a list. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = a # list\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 3. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b n t h s ta hs a list. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = h # hs; n = length hs; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; hs = a # list\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False
 2. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b n t s. \<lbrakk>G b; \<not> snd (A (st b)); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (\<exists>s'. t = Normal s' \<and> (Inr (rx s'), st s') \<in> fst (A (st b))); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b; b = s; [B] = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(a, b). a = st b} \<and> unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr r s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!