theory Refine_C

lemma refinement2_both:
  "\<lparr> Init = Init_C, Fin = Fin_C,
     Step = (\<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)) \<rparr>
   \<sqsubseteq> ADT_H uop" supply word_neq_0_conv[simp] apply (rule sim_imp_refines) apply (rule L_invariantI [where I\<^sub>c=UNIV and r="lift_state_relation rf_sr"]) apply (rule full_invs_both) apply simp apply (unfold LI_def) apply (rule conjI) apply (simp add: ADT_H_def) apply (blast intro!: init_refinement_C) apply (rule conjI) prefer 2 apply (simp add: ADT_H_def) apply (clarsimp simp: Fin_C_def) apply (drule lift_state_relationD) apply (clarsimp simp: cstate_to_A_def) apply (subst cstate_to_H_correct) apply (fastforce simp: full_invs'_def invs'_def) apply (clarsimp simp: rf_sr_def) apply (simp add:absKState_def observable_memory_def absExst_def) apply (rule MachineTypes.machine_state.equality,simp_all)[1] apply (rule ext) apply (clarsimp simp: user_mem'_def option_to_0_def split:if_splits) apply (simp add: ADT_H_def) supply subst_all [simp del] apply (clarsimp simp: rel_semi_def global_automaton_def relcomp_unfold
                        in_lift_state_relation_eq) apply (erule_tac P="a \<and> (\<exists>x. b x)" for a b in disjE) apply (clarsimp simp add: kernel_call_C_def kernel_call_H_def) apply (subgoal_tac "all_invs' x b") apply (drule_tac fp=fp and tc=af in entry_refinement_C, simp+) apply clarsimp apply (drule spec, drule spec, drule(1) mp) apply (clarsimp simp: full_invs'_def) apply (frule use_valid, rule kernelEntry_invs',
          simp add: sch_act_simple_def) apply (fastforce simp: ct_running'_C) apply (clarsimp simp: full_invs_def full_invs'_def all_invs'_def) apply fastforce apply (erule_tac P="a \<and> b \<and> c \<and> d \<and> e" for a b c d e in disjE) apply (clarsimp simp add: do_user_op_C_def do_user_op_H_def monad_to_transition_def) apply (rule rev_mp, rule_tac f="uop" and tc=af in do_user_op_corres_C) apply (clarsimp simp: corres_underlying_def invs_def ex_abs_def) apply (fastforce simp: full_invs'_def ex_abs_def) apply (erule_tac P="a \<and> b \<and> c \<and> (\<exists>x. e x)" for a b c d e in disjE) apply (clarsimp simp add: do_user_op_C_def do_user_op_H_def monad_to_transition_def) apply (rule rev_mp, rule_tac f="uop" and tc=af in do_user_op_corres_C) apply (clarsimp simp: corres_underlying_def invs_def ex_abs_def) apply (fastforce simp: full_invs'_def ex_abs_def) apply (clarsimp simp: check_active_irq_C_def check_active_irq_H_def) apply (rule rev_mp, rule check_active_irq_corres_C) apply (fastforce simp: corres_underlying_def full_invs'_def ex_abs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> \<sqsubseteq> ADT_H uop proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> \<sqsubseteq> ADT_H uop proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> \<sqsubseteq>\<^sub>F ADT_H uop proof (prove)
goal (3 subgoals):
 1. ADT_H uop \<Turnstile> ?I\<^sub>a2
 2. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> \<Turnstile> UNIV
 3. LI (ADT_H uop) \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> (lift_state_relation rf_sr) (?I\<^sub>a2 \<times> UNIV) proof (prove)
goal (2 subgoals):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> \<Turnstile> UNIV
 2. LI (ADT_H uop) \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> (lift_state_relation rf_sr) ({s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. LI (ADT_H uop) \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> (lift_state_relation rf_sr) ({s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. Init \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s \<subseteq> lift_state_relation rf_sr `` Init (ADT_H uop) s) \<and> (\<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr) \<and> (\<forall>s s'. (s, s') \<in> lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV \<longrightarrow> Fin \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s' = Fin (ADT_H uop) s) proof (prove)
goal (2 subgoals):
 1. \<forall>s. Init \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s \<subseteq> lift_state_relation rf_sr `` Init (ADT_H uop) s
 2. (\<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr) \<and> (\<forall>s s'. (s, s') \<in> lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV \<longrightarrow> Fin \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s' = Fin (ADT_H uop) s) proof (prove)
goal (2 subgoals):
 1. \<forall>a b aa ba. Init_C ((a, b), aa, ba) \<subseteq> lift_state_relation rf_sr `` Init_H
 2. (\<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr) \<and> (\<forall>s s'. (s, s') \<in> lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV \<longrightarrow> Fin \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s' = Fin (ADT_H uop) s) proof (prove)
goal (1 subgoal):
 1. (\<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr) \<and> (\<forall>s s'. (s, s') \<in> lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV \<longrightarrow> Fin \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s' = Fin (ADT_H uop) s) proof (prove)
goal (2 subgoals):
 1. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr
 2. \<forall>s s'. (s, s') \<in> lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV \<longrightarrow> Fin \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s' = Fin (ADT_H uop) s proof (prove)
goal (2 subgoals):
 1. \<forall>s s'. (s, s') \<in> lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV \<longrightarrow> Fin \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> s' = Fin (ADT_H uop) s
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<forall>a b aa ba ab bb ac bc. (((a, b), aa, ba), (ab, bb), ac, bc) \<in> lift_state_relation rf_sr \<and> (\<exists>ab bb ac bc. (((ab, bb), ac, bc), (a, b), aa, ba) \<in> lift_state_relation state_relation \<and> ((ab, bb), ac, bc) \<in> full_invs \<and> ((a, b), aa, ba) \<in> full_invs') \<longrightarrow> Fin_C ((ab, bb), ac, bc) = ((a, absKState b), aa, ba)
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>(((a, b), aa, ba), (ab, bb), ac, bc) \<in> lift_state_relation rf_sr; (((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'\<rbrakk> \<Longrightarrow> ab = a \<and> cstate_to_A bb = absKState b \<and> ac = aa \<and> bc = ba
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr \<and> ab = a \<and> ac = aa \<and> bc = ba\<rbrakk> \<Longrightarrow> ab = a \<and> cstate_to_A bb = absKState b \<and> ac = aa \<and> bc = ba
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> absKState (cstate_to_H (globals bb)) = absKState b
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> valid_state' (?as45 a b aa ba bb ad bd ae be)
 2. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> cstate_relation (?as45 a b aa ba bb ad bd ae be) (globals bb)
 3. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> absKState (?as45 a b aa ba bb ad bd ae be\<lparr>ksMachineState := observable_memory (ksMachineState (?as45 a b aa ba bb ad bd ae be)) (user_mem' (?as45 a b aa ba bb ad bd ae be))\<rparr>) = absKState b
 4. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> cstate_relation b (globals bb)
 2. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> absKState (b\<lparr>ksMachineState := observable_memory (ksMachineState b) (user_mem' b)\<rparr>) = absKState b
 3. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> absKState (b\<lparr>ksMachineState := observable_memory (ksMachineState b) (user_mem' b)\<rparr>) = absKState b
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> ksMachineState b\<lparr>underlying_memory := option_to_0 \<circ> user_mem' (b\<lparr>ksMachineState := ksMachineState b\<lparr>underlying_memory := option_to_0 \<circ> user_mem' b\<rparr>\<rparr>)\<rparr> = ksMachineState b\<lparr>underlying_memory := option_to_0 \<circ> user_mem' b\<rparr>
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba bb ad bd ae be. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> option_to_0 \<circ> user_mem' (b\<lparr>ksMachineState := ksMachineState b\<lparr>underlying_memory := option_to_0 \<circ> user_mem' b\<rparr>\<rparr>) = option_to_0 \<circ> user_mem' b
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba bb ad bd ae be x. \<lbrakk>(((ad, bd), ae, be), (a, b), aa, ba) \<in> lift_state_relation state_relation; ((ad, bd), ae, be) \<in> full_invs; ((a, b), aa, ba) \<in> full_invs'; (b, bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> (option_to_0 \<circ> user_mem' (b\<lparr>ksMachineState := ksMachineState b\<lparr>underlying_memory := option_to_0 \<circ> user_mem' b\<rparr>\<rparr>)) x = (option_to_0 \<circ> user_mem' b) x
 2. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (1 subgoal):
 1. \<forall>j. lift_state_relation rf_sr \<inter> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; Step \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)\<rparr> j \<subseteq> Step (ADT_H uop) j ;;; lift_state_relation rf_sr proof (prove)
goal (1 subgoal):
 1. lift_state_relation rf_sr \<inter> {s'. \<exists>a b aa ba. (((a, b), aa, ba), s') \<in> lift_state_relation state_relation \<and> ((a, b), aa, ba) \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp) \<subseteq> global_automaton check_active_irq_H (do_user_op_H uop) kernel_call_H ;;; lift_state_relation rf_sr proof (prove)
goal (1 subgoal):
 1. lift_state_relation rf_sr \<inter> {s'. \<exists>a b aa ba. (((a, b), aa, ba), s') \<in> lift_state_relation state_relation \<and> ((a, b), aa, ba) \<in> full_invs \<and> s' \<in> full_invs'} \<times> UNIV ;;; global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp) \<subseteq> global_automaton check_active_irq_H (do_user_op_H uop) kernel_call_H ;;; lift_state_relation rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, bd), ac, ab, bb) \<in> kernel_call_C fp e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = KernelMode \<and> (\<exists>x. bg = Some x \<and> bc = None \<and> ((af, bd), ac, ab, bb) \<in> kernel_call_C fp x)\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> ac = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd); all_invs' x b\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> ac = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 3. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>b ab bb bd bf af x ac. \<lbrakk>ac = (if ct_running_C bb then UserMode else IdleMode); (b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd); \<not> snd (kernelEntry_C fp x af bd) \<and> (\<forall>tc' t'. (tc', t') \<in> fst (kernelEntry_C fp x af bd) \<longrightarrow> (\<exists>s'. (tc', s') \<in> fst (kernelEntry x af b) \<and> (s', t') \<in> rf_sr))\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> (if ct_running_C bb then UserMode else IdleMode) = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 3. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>b ab bb bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd); \<not> snd (kernelEntry_C fp x af bd); \<forall>tc' t'. (tc', t') \<in> fst (kernelEntry_C fp x af bd) \<longrightarrow> (\<exists>s'. (tc', s') \<in> fst (kernelEntry x af b) \<and> (s', t') \<in> rf_sr)\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> (if ct_running_C bb then UserMode else IdleMode) = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 3. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>b ab bb bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd); \<not> snd (kernelEntry_C fp x af bd); \<exists>s'. (ab, s') \<in> fst (kernelEntry x af b) \<and> (s', bb) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> (if ct_running_C bb then UserMode else IdleMode) = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 3. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>b ab bb bd bf af x s'. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; (ab, bb) \<in> fst (kernelEntry_C fp x af bd); \<not> snd (kernelEntry_C fp x af bd); invs' b; (ab, s') \<in> fst (kernelEntry x af b); (s', bb) \<in> rf_sr; vs_valid_duplicates' (ksPSpace b); ex_abs einvs b; ksSchedulerAction b = ResumeCurrentThread; ct_running' b \<or> ct_idle' b; x \<noteq> Interrupt \<longrightarrow> ct_running' b; 0 < ksDomainTime b; valid_domain_list' b\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> (if ct_running_C bb then UserMode else IdleMode) = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 3. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>b ab bb bd bf af x s'. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; (ab, bb) \<in> fst (kernelEntry_C fp x af bd); \<not> snd (kernelEntry_C fp x af bd); invs' b; (ab, s') \<in> fst (kernelEntry x af b); (s', bb) \<in> rf_sr; vs_valid_duplicates' (ksPSpace b); ex_abs einvs b; ksSchedulerAction b = ResumeCurrentThread; ct_running' b \<or> ct_idle' b; x \<noteq> Interrupt \<longrightarrow> ct_running' b; 0 < ksDomainTime b; valid_domain_list' b; ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle')) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') s'\<rbrakk> \<Longrightarrow> \<exists>ba. (ab, ba) \<in> fst (kernelEntry x af b) \<and> (if ct_running_C bb then UserMode else IdleMode) = (if ct_running' ba then UserMode else IdleMode) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 3. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), KernelMode, Some x) \<in> full_invs; ((af, b), KernelMode, Some x) \<in> full_invs'; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd)\<rbrakk> \<Longrightarrow> all_invs' x b
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb ac bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; (ab, bb) \<in> fst (kernelEntry_C fp x af bd) \<and> ac = (if ct_running_C bb then UserMode else IdleMode) \<or> snd (kernelEntry_C fp x af bd); invs bf; invs' b; valid_list bf; vs_valid_duplicates' (ksPSpace b); valid_sched_2 (ready_queues bf) (ekheap bf) resume_cur_thread (cur_domain bf) (kheap bf) (cur_thread bf) (idle_thread bf); ex_abs einvs b; ct_running bf \<or> ct_idle bf; ksSchedulerAction b = ResumeCurrentThread; x \<noteq> Interrupt \<longrightarrow> ct_running bf; ct_running' b \<or> ct_idle' b; 0 < domain_time bf; x \<noteq> Interrupt \<longrightarrow> ct_running' b; valid_domain_list bf; scheduler_action bf = resume_cur_thread; 0 < ksDomainTime b; valid_domain_list' b\<rbrakk> \<Longrightarrow> \<exists>s. (s, b) \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, bd), None, ab, bb) \<in> do_user_op_C uop\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb bd bf af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), UserMode, None) \<in> full_invs; ((af, b), UserMode, None) \<in> full_invs'; ((None, ab), bb) \<in> fst (doUserOp_C uop af bd)\<rbrakk> \<Longrightarrow> \<exists>ba. ((None, ab), ba) \<in> fst (doUserOp uop af b) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb bd bf af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), UserMode, None) \<in> full_invs; ((af, b), UserMode, None) \<in> full_invs'; ((None, ab), bb) \<in> fst (doUserOp_C uop af bd)\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) (\<lambda>_. True) (doUserOp uop af) (doUserOp_C uop af) \<longrightarrow> (\<exists>ba. ((None, ab), ba) \<in> fst (doUserOp uop af b) \<and> (ba, bb) \<in> rf_sr)
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb bd bf af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), UserMode, None) \<in> full_invs; ((af, b), UserMode, None) \<in> full_invs'; ((None, ab), bb) \<in> fst (doUserOp_C uop af bd); \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> valid_state sa \<and> cur_tcb sa \<and> valid_list sa \<and> valid_sched sa) \<longrightarrow> (\<forall>x\<in>fst (doUserOp_C uop af s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doUserOp uop af s). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> r = r')\<rbrakk> \<Longrightarrow> \<exists>ba. ((None, ab), ba) \<in> fst (doUserOp uop af b) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, bd), Some e, ab, bb) \<in> do_user_op_C uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>x. bc = Some x \<and> ((af, bd), Some x, ab, bb) \<in> do_user_op_C uop)\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), UserMode, None) \<in> full_invs; ((af, b), UserMode, None) \<in> full_invs'; ((Some x, ab), bb) \<in> fst (doUserOp_C uop af bd)\<rbrakk> \<Longrightarrow> \<exists>ba. (((Some x, ab), ba) \<in> fst (doUserOp uop af b) \<or> x = Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), UserMode, None) \<in> full_invs; ((af, b), UserMode, None) \<in> full_invs'; ((Some x, ab), bb) \<in> fst (doUserOp_C uop af bd)\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) (\<lambda>_. True) (doUserOp uop af) (doUserOp_C uop af) \<longrightarrow> (\<exists>ba. (((Some x, ab), ba) \<in> fst (doUserOp uop af b) \<or> x = Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr)
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>b ab bb bd bf af x. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), UserMode, None) \<in> full_invs; ((af, b), UserMode, None) \<in> full_invs'; ((Some x, ab), bb) \<in> fst (doUserOp_C uop af bd); \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> valid_state sa \<and> cur_tcb sa \<and> valid_list sa \<and> valid_sched sa) \<longrightarrow> (\<forall>x\<in>fst (doUserOp_C uop af s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doUserOp uop af s). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> r = r')\<rbrakk> \<Longrightarrow> \<exists>ba. (((Some x, ab), ba) \<in> fst (doUserOp uop af b) \<or> x = Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr
 2. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, bd), False, ab, bb) \<in> check_active_irq_C \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, bd), True, ab, bb) \<in> check_active_irq_C\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> ((af, b), False, ab, ba) \<in> check_active_irq_H \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> ((af, b), True, ab, ba) \<in> check_active_irq_H) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, bb) \<in> fst (checkActiveIRQ_C bd) \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> (False, bb) \<in> fst (checkActiveIRQ_C bd) \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, bb) \<in> fst (checkActiveIRQ_C bd)\<rbrakk> \<Longrightarrow> \<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, ba) \<in> fst (checkActiveIRQ b) \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> (False, ba) \<in> fst (checkActiveIRQ b) \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, ba) \<in> fst (checkActiveIRQ b)) \<and> (ba, bb) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>b ab bb ac bc bd bf bg ag af. \<lbrakk>(b, bd) \<in> rf_sr; (bf, b) \<in> state_relation; ((af, bf), ag, bg) \<in> full_invs; ((af, b), ag, bg) \<in> full_invs'; ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, bb) \<in> fst (checkActiveIRQ_C bd) \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> (False, bb) \<in> fst (checkActiveIRQ_C bd) \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, bb) \<in> fst (checkActiveIRQ_C bd)\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True (=) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) (\<lambda>_. True) checkActiveIRQ checkActiveIRQ_C \<longrightarrow> (\<exists>ba. (ag = KernelMode \<and> (\<exists>e. bg = Some e \<and> bc = None \<and> ((af, b), ac, ab, ba) \<in> kernel_call_H e) \<or> ag = UserMode \<and> bg = None \<and> ac = UserMode \<and> bc = None \<and> ((af, b), None, ab, ba) \<in> do_user_op_H uop \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ((af, b), Some e, ab, ba) \<in> do_user_op_H uop) \<or> ag = UserMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, ba) \<in> fst (checkActiveIRQ b) \<or> ag = IdleMode \<and> bg = None \<and> ac = IdleMode \<and> bc = None \<and> (False, ba) \<in> fst (checkActiveIRQ b) \<or> ag = IdleMode \<and> bg = None \<and> ac = KernelMode \<and> bc = Some Interrupt \<and> (True, ba) \<in> fst (checkActiveIRQ b)) \<and> (ba, bb) \<in> rf_sr) proof (prove)
goal:
No subgoals!