theory ADT_IF_Refine

lemma haskell_to_abs:
  "uop_nonempty uop
   \<Longrightarrow> global_automata_refine check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if
                              kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if
                              full_invs_if (ADT_A_if uop) {s. step_restrict s} checkActiveIRQ_H_if
                              (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if
                              schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop)
                              (lift_snd_rel state_relation) True" apply (simp add: global_automata_refine_def) apply (intro conjI) apply (rule abstract_invs) apply (rule haskell_invs) apply (unfold_locales) apply (simp add: step_restrict_def) apply (simp add: ADT_H_if_def ADT_A_if_def) apply (clarsimp simp add: lift_snd_rel_def full_invs_if_def full_invs_if'_def) apply (frule valid_device_abs_state_eq[OF invs_machine_state]) apply (frule absKState_correct[rotated]) apply simp+ apply (simp add: ADT_H_if_def ADT_A_if_def lift_fst_rel_def) apply (clarsimp simp: lift_snd_rel_def) apply (subgoal_tac "((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation") apply (fastforce simp: step_restrict_def has_srel_state_def lift_fst_rel_def lift_snd_rel_def) apply (simp add: full_invs_if'_def) apply (clarsimp simp: ex_abs_def) apply (frule(1) absKState_correct[rotated],simp+) apply (simp add: full_invs_if_def) apply (frule valid_device_abs_state_eq[OF invs_machine_state]) apply (case_tac ba; clarsimp simp: domain_time_rel_eq domain_list_rel_eq) apply (fastforce simp: active_from_running ct_running_related ct_idle_related schedaction_related)+ apply (simp add: sched_act_cnt_related) apply (fastforce simp: active_from_running ct_running_related ct_idle_related schedaction_related)+ apply (simp add: check_active_irq_A_if_def checkActiveIRQ_H_if_def) apply (rule step_corres_lifts) apply (rule corres_guard_imp) apply (rule check_active_irq_if_corres,simp+) apply (rule checkActiveIRQ_if_empty_fail) apply (simp add: check_active_irq_A_if_def checkActiveIRQ_H_if_def) apply (rule step_corres_lifts) apply (rule corres_guard_imp) apply (rule check_active_irq_if_corres,simp+) apply (rule checkActiveIRQ_if_empty_fail) apply (simp add: do_user_op_A_if_def doUserOp_H_if_def) apply (rule step_corres_lifts) apply (rule corres_guard_imp) apply (rule do_user_op_if_corres) apply (fastforce simp: full_invs_if_def uop_nonempty_def) apply (simp add: full_invs_if'_def uop_nonempty_def) apply (rule doUserOp_if_empty_fail) apply (simp add: kernelCall_H_if_def kernel_call_A_if_def del: unit_Inl_or_Inr(2)) apply (rule step_corres_lifts) apply (rule corres_rel_imp) apply (rule corres_guard_imp) apply (rule kernel_entry_if_corres) apply clarsimp apply ((clarsimp simp: full_invs_if_def full_invs_if'_def)+)[2] apply (fastforce simp: prod_lift_def) apply (rule kernelEntry_if_empty_fail) apply (simp add: kernel_handle_preemption_if_def handlePreemption_H_if_def) apply (rule step_corres_lifts) apply (rule corres_guard_imp) apply (rule handle_preemption_if_corres) apply (simp add: full_invs_if_def) apply (simp add: full_invs_if'_def) apply (rule handlePreemption_if_empty_fail) apply (simp add: kernel_schedule_if_def schedule'_H_if_def) apply (rule step_corres_lifts) apply (rule corres_guard_imp) apply (rule schedule_if_corres) apply (simp add: full_invs_if_def) apply (simp add: full_invs_if'_def) apply (rule schedule'_if_empty_fail) apply (simp add: kernel_exit_A_if_def kernelExit_H_if_def split del: if_split) apply (rule_tac S="\<top>" and S'="invs'" in step_corres_lifts(5)) apply (rule corres_guard_imp) apply (rule kernel_exit_if_corres) apply ((simp add: full_invs_if_def full_invs_if'_def)+)[2] apply (rule kernelExit_if_empty_fail) apply clarsimp apply (clarsimp simp: ct_running'_related ct_running_related) apply wp apply (clarsimp simp: full_invs_if'_def) apply wp apply (clarsimp simp: kernel_call_A_if_def) apply (drule use_valid[OF _ kernel_entry_if_no_preempt]; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> global_automata_refine check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) {s. step_restrict s} checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) (Collect step_restrict) \<and> global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV \<and> global_automata_refine_axioms check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) (Collect step_restrict) checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True proof (prove)
goal (3 subgoals):
 1. uop_nonempty uop \<Longrightarrow> global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) (Collect step_restrict)
 2. uop_nonempty uop \<Longrightarrow> global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV
 3. uop_nonempty uop \<Longrightarrow> global_automata_refine_axioms check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) (Collect step_restrict) checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV
 2. uop_nonempty uop \<Longrightarrow> global_automata_refine_axioms check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) (Collect step_restrict) checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> global_automata_refine_axioms check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) (Collect step_restrict) checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True proof (prove)
goal (11 subgoals):
 1. uop_nonempty uop \<Longrightarrow> has_srel_state (lift_fst_rel (lift_snd_rel state_relation)) full_invs_if' \<subseteq> Collect step_restrict
 2. \<And>s s' mode. \<lbrakk>uop_nonempty uop; (s, s') \<in> lift_snd_rel state_relation; (s, mode) \<in> full_invs_if; (s', mode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> Fin (ADT_H_if uop) (s', mode) = Fin (ADT_A_if uop) (s, mode)
 3. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 7. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 9. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 10. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s s' mode. \<lbrakk>uop_nonempty uop; (s, s') \<in> lift_snd_rel state_relation; (s, mode) \<in> full_invs_if; (s', mode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> Fin (ADT_H_if uop) (s', mode) = Fin (ADT_A_if uop) (s, mode)
 2. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (10 subgoals):
 1. \<And>s s' mode. \<lbrakk>uop_nonempty uop; (s, s') \<in> lift_snd_rel state_relation; (s, mode) \<in> full_invs_if; (s', mode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> (case s' of (uc, s) \<Rightarrow> Pair (uc, absKState s)) mode = (s, mode)
 2. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (10 subgoals):
 1. \<And>b aa ba mode. \<lbrakk>uop_nonempty uop; (b, ba) \<in> state_relation; invs b; invs' ba; valid_list b; ex_abs einvs ba; valid_sched b; arch_extras ba; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time b; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime ba; domain_time b = 0 \<longrightarrow> scheduler_action b = choose_new_thread; ksDomainTime ba = 0 \<longrightarrow> ksSchedulerAction ba = ChooseNewThread; valid_domain_list b; case mode of InUserMode \<Rightarrow> ct_running (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((aa, b), mode))) \<and> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | _ \<Rightarrow> True; valid_domain_list' ba; case mode of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> absKState ba = b
 2. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (10 subgoals):
 1. \<And>b aa ba mode. \<lbrakk>uop_nonempty uop; (b, ba) \<in> state_relation; invs b; invs' ba; valid_list b; ex_abs einvs ba; valid_sched b; arch_extras ba; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time b; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime ba; domain_time b = 0 \<longrightarrow> scheduler_action b = choose_new_thread; ksDomainTime ba = 0 \<longrightarrow> ksSchedulerAction ba = ChooseNewThread; valid_domain_list b; case mode of InUserMode \<Rightarrow> ct_running (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((aa, b), mode))) \<and> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | _ \<Rightarrow> True; valid_domain_list' ba; case mode of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0 | _ \<Rightarrow> True; abs_state b = b\<rbrakk> \<Longrightarrow> absKState ba = b
 2. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (12 subgoals):
 1. \<And>b aa ba mode. \<lbrakk>uop_nonempty uop; (b, ba) \<in> state_relation; invs b; invs' ba; valid_list b; ex_abs einvs ba; valid_sched b; arch_extras ba; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time b; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime ba; domain_time b = 0 \<longrightarrow> scheduler_action b = choose_new_thread; ksDomainTime ba = 0 \<longrightarrow> ksSchedulerAction ba = ChooseNewThread; valid_domain_list b; case mode of InUserMode \<Rightarrow> ct_running (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((aa, b), mode))) \<and> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | _ \<Rightarrow> True; valid_domain_list' ba; case mode of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0 | _ \<Rightarrow> True; abs_state b = b\<rbrakk> \<Longrightarrow> (?s24 b aa ba mode, ba) \<in> state_relation
 2. \<And>b aa ba mode. \<lbrakk>uop_nonempty uop; (b, ba) \<in> state_relation; invs b; invs' ba; valid_list b; ex_abs einvs ba; valid_sched b; arch_extras ba; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time b; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime ba; domain_time b = 0 \<longrightarrow> scheduler_action b = choose_new_thread; ksDomainTime ba = 0 \<longrightarrow> ksSchedulerAction ba = ChooseNewThread; valid_domain_list b; case mode of InUserMode \<Rightarrow> ct_running (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((aa, b), mode))) \<and> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | _ \<Rightarrow> True; valid_domain_list' ba; case mode of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0 | _ \<Rightarrow> True; abs_state b = b\<rbrakk> \<Longrightarrow> einvs (?s24 b aa ba mode)
 3. \<And>b aa ba mode. \<lbrakk>uop_nonempty uop; (b, ba) \<in> state_relation; invs b; invs' ba; valid_list b; ex_abs einvs ba; valid_sched b; arch_extras ba; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time b; mode \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime ba; domain_time b = 0 \<longrightarrow> scheduler_action b = choose_new_thread; ksDomainTime ba = 0 \<longrightarrow> ksSchedulerAction ba = ChooseNewThread; valid_domain_list b; case mode of InUserMode \<Rightarrow> ct_running (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((aa, b), mode)) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((aa, b), mode))) \<and> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((aa, b), mode)) \<or> ct_idle (internal_state_if ((aa, b), mode))) \<and> scheduler_action (internal_state_if ((aa, b), mode)) = resume_cur_thread | _ \<Rightarrow> True; valid_domain_list' ba; case mode of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, ba), mode)) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, ba), mode)) \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, ba), mode)) \<or> ct_idle' (internal_state_if ((aa, ba), mode))) \<and> ksSchedulerAction (internal_state_if ((aa, ba), mode)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, ba), mode)) \<noteq> 0 | _ \<Rightarrow> True; abs_state b = b; absKState ba = abs_state (?s24 b aa ba mode)\<rbrakk> \<Longrightarrow> absKState ba = b
 4. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 8. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 10. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
A total of 12 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_H_if uop) a \<subseteq> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if uop) a
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a. uop_nonempty uop \<Longrightarrow> ({user_context_of a} \<times> {s'. absKState s' = internal_state_if a}) \<times> {sys_mode_of a} \<inter> full_invs_if' \<subseteq> {r'. \<exists>r\<in>{a} \<inter> full_invs_if \<inter> Collect step_restrict. snd r = snd r' \<and> (fst r, fst r') \<in> lift_snd_rel state_relation}
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb. \<lbrakk>uop_nonempty uop; ((a, bb), ba) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ((a, absKState bb), ba) \<in> full_invs_if \<and> step_restrict ((a, absKState bb), ba) \<and> (absKState bb, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (10 subgoals):
 1. \<And>a ba bb. \<lbrakk>uop_nonempty uop; ((a, bb), ba) \<in> full_invs_if'; ((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((a, absKState bb), ba) \<in> full_invs_if \<and> step_restrict ((a, absKState bb), ba) \<and> (absKState bb, bb) \<in> state_relation
 2. \<And>a ba bb. \<lbrakk>uop_nonempty uop; ((a, bb), ba) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb. \<lbrakk>uop_nonempty uop; ((a, bb), ba) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb. \<lbrakk>uop_nonempty uop; invs' bb \<and> ex_abs einvs bb \<and> arch_extras bb \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb) \<and> (ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread) \<and> valid_domain_list' bb \<and> (case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> ((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb s. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (s, bb) \<in> state_relation; ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; invs s; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_list s; valid_sched s; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> ((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb s. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (s, bb) \<in> state_relation; ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; invs s; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_list s; valid_sched s; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True; absKState bb = abs_state s\<rbrakk> \<Longrightarrow> ((a, abs_state s), ba) \<in> full_invs_if \<and> (abs_state s, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb s. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (s, bb) \<in> state_relation; ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; invs s; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_list s; valid_sched s; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True; absKState bb = abs_state s\<rbrakk> \<Longrightarrow> invs (abs_state s) \<and> valid_list (abs_state s) \<and> valid_sched (abs_state s) \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (abs_state s)) \<and> (domain_time (abs_state s) = 0 \<longrightarrow> scheduler_action (abs_state s) = choose_new_thread) \<and> valid_domain_list (abs_state s) \<and> (case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((a, abs_state s), ba)) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((a, abs_state s), ba)) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((a, abs_state s), ba))) \<and> (ct_running (internal_state_if ((a, abs_state s), ba)) \<or> ct_idle (internal_state_if ((a, abs_state s), ba))) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((a, abs_state s), ba)) \<or> ct_idle (internal_state_if ((a, abs_state s), ba))) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | _ \<Rightarrow> True) \<and> (abs_state s, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>a ba bb s. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (s, bb) \<in> state_relation; ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; invs s; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_list s; valid_sched s; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((a, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((a, bb), ba)) \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((a, bb), ba)) \<or> ct_idle' (internal_state_if ((a, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((a, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((a, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True; absKState bb = abs_state s; abs_state s = s\<rbrakk> \<Longrightarrow> invs (abs_state s) \<and> valid_list (abs_state s) \<and> valid_sched (abs_state s) \<and> (ba \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (abs_state s)) \<and> (domain_time (abs_state s) = 0 \<longrightarrow> scheduler_action (abs_state s) = choose_new_thread) \<and> valid_domain_list (abs_state s) \<and> (case ba of InUserMode \<Rightarrow> ct_running (internal_state_if ((a, abs_state s), ba)) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if ((a, abs_state s), ba)) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if ((a, abs_state s), ba))) \<and> (ct_running (internal_state_if ((a, abs_state s), ba)) \<or> ct_idle (internal_state_if ((a, abs_state s), ba))) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if ((a, abs_state s), ba)) \<or> ct_idle (internal_state_if ((a, abs_state s), ba))) \<and> scheduler_action (internal_state_if ((a, abs_state s), ba)) = resume_cur_thread | _ \<Rightarrow> True) \<and> (abs_state s, bb) \<in> state_relation
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (13 subgoals):
 1. \<And>bb. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; 0 < domain_time (absKState bb); invs (absKState bb); domain_time (absKState bb) \<noteq> 0; valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; ct_running' bb; ksSchedulerAction bb = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ct_running (absKState bb) \<and> scheduler_action (absKState bb) = resume_cur_thread
 2. \<And>bb. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; 0 < domain_time (absKState bb); invs (absKState bb); domain_time (absKState bb) \<noteq> 0; valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; ct_idle' bb; ksSchedulerAction bb = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ct_idle (absKState bb) \<and> scheduler_action (absKState bb) = resume_cur_thread
 3. \<And>bb x3. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; 0 < domain_time (absKState bb); invs (absKState bb); domain_time (absKState bb) \<noteq> 0; valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; x3 \<noteq> Interrupt \<longrightarrow> ct_running' bb; ct_running' bb \<or> ct_idle' bb; ksSchedulerAction bb = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (x3 \<noteq> Interrupt \<longrightarrow> ct_running (absKState bb)) \<and> (ct_running (absKState bb) \<or> ct_idle (absKState bb)) \<and> scheduler_action (absKState bb) = resume_cur_thread
 4. \<And>bb x5. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; x5; invs (absKState bb); valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; domain_time (absKState bb) = 0; ksSchedulerAction bb = ChooseNewThread\<rbrakk> \<Longrightarrow> scheduler_action (absKState bb) = choose_new_thread
 5. \<And>bb. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; 0 < domain_time (absKState bb); invs (absKState bb); valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; ct_running' bb \<or> ct_idle' bb; ksSchedulerAction bb = ResumeCurrentThread; domain_time (absKState bb) \<noteq> 0\<rbrakk> \<Longrightarrow> (ct_running (absKState bb) \<or> ct_idle (absKState bb)) \<and> scheduler_action (absKState bb) = resume_cur_thread
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 9. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 10. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
A total of 13 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>bb x5. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; x5; invs (absKState bb); valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; domain_time (absKState bb) = 0; ksSchedulerAction bb = ChooseNewThread\<rbrakk> \<Longrightarrow> scheduler_action (absKState bb) = choose_new_thread
 2. \<And>bb. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; 0 < domain_time (absKState bb); invs (absKState bb); valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; ct_running' bb \<or> ct_idle' bb; ksSchedulerAction bb = ResumeCurrentThread; domain_time (absKState bb) \<noteq> 0\<rbrakk> \<Longrightarrow> (ct_running (absKState bb) \<or> ct_idle (absKState bb)) \<and> scheduler_action (absKState bb) = resume_cur_thread
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>bb. \<lbrakk>uop_nonempty uop; invs' bb; arch_extras bb; (absKState bb, bb) \<in> state_relation; 0 < domain_time (absKState bb); invs (absKState bb); valid_list (absKState bb); valid_sched (absKState bb); valid_domain_list (absKState bb); abs_state (absKState bb) = absKState bb; ct_running' bb \<or> ct_idle' bb; ksSchedulerAction bb = ResumeCurrentThread; domain_time (absKState bb) \<noteq> 0\<rbrakk> \<Longrightarrow> (ct_running (absKState bb) \<or> ct_idle (absKState bb)) \<and> scheduler_action (absKState bb) = resume_cur_thread
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (check_active_irq_if tc s)} {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (\<lambda>s. ((tc, s), InUserMode) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), InUserMode) \<in> full_invs_if') (check_active_irq_if tc) (checkActiveIRQ_if tc)
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (checkActiveIRQ_if tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (11 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (?Q157 tc) (?Q'157 tc) (check_active_irq_if tc) (checkActiveIRQ_if tc)
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q157 tc s
 3. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'157 tc s
 4. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (checkActiveIRQ_if tc)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 7. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 9. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 10. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
A total of 11 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> empty_fail (checkActiveIRQ_if tc)
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' check_active_irq_A_if checkActiveIRQ_H_if
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 3. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InIdleMode full_invs_if full_invs_if' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (check_active_irq_if tc s)} {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 3. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (\<lambda>s. ((tc, s), InIdleMode) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), InIdleMode) \<in> full_invs_if') (check_active_irq_if tc) (checkActiveIRQ_if tc)
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (checkActiveIRQ_if tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (10 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (?Q166 tc) (?Q'166 tc) (check_active_irq_if tc) (checkActiveIRQ_if tc)
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InIdleMode) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q166 tc s
 3. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InIdleMode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'166 tc s
 4. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (checkActiveIRQ_if tc)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 9. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> empty_fail (checkActiveIRQ_if tc)
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 3. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' (do_user_op_A_if uop) (doUserOp_H_if uop)
 2. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) InUserMode full_invs_if full_invs_if' {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (do_user_op_if uop a b)} {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_if uop a b)}
 2. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (\<lambda>s. ((tc, s), InUserMode) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), InUserMode) \<in> full_invs_if') (do_user_op_if uop tc) (doUserOp_if uop tc)
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (doUserOp_if uop tc)
 3. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (?Q183 tc) (?Q'183 tc) (do_user_op_if uop tc) (doUserOp_if uop tc)
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q183 tc s
 3. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'183 tc s
 4. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (doUserOp_if uop tc)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if\<rbrakk> \<Longrightarrow> (einvs and ct_running and (\<lambda>_. \<forall>t pl pr pxn tcu. uop t pl pr pxn tcu \<noteq> {})) s
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s
 3. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (doUserOp_if uop tc)
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), InUserMode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (doUserOp_if uop tc)
 3. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (doUserOp_if uop tc)
 2. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' (kernel_call_A_if e) (kernelCall_H_if e)
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 3. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelEntry e) full_invs_if full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernel_entry_if e a b) \<and> ba = (r \<noteq> Inr ())} {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 3. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. \<And>e tc. uop_nonempty uop \<Longrightarrow> corres (\<lambda>r r'. (fst r = Inr ()) = (fst r' = Inr ()) \<and> snd r = snd r') (\<lambda>s. ((tc, s), KernelEntry e) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), KernelEntry e) \<in> full_invs_if') (kernel_entry_if e tc) (kernelEntry_if e tc)
 2. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. \<And>e tc. uop_nonempty uop \<Longrightarrow> corres (?r'214 e tc) (\<lambda>s. ((tc, s), KernelEntry e) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), KernelEntry e) \<in> full_invs_if') (kernel_entry_if e tc) (kernelEntry_if e tc)
 2. \<And>e tc x y. \<lbrakk>uop_nonempty uop; ?r'214 e tc x y\<rbrakk> \<Longrightarrow> (fst x = Inr ()) = (fst y = Inr ()) \<and> snd x = snd y
 3. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (9 subgoals):
 1. \<And>e tc. uop_nonempty uop \<Longrightarrow> corres (?r'214 e tc) (?Q217 e tc) (?Q'217 e tc) (kernel_entry_if e tc) (kernelEntry_if e tc)
 2. \<And>e tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelEntry e) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q217 e tc s
 3. \<And>e tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelEntry e) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'217 e tc s
 4. \<And>e tc x y. \<lbrakk>uop_nonempty uop; ?r'214 e tc x y\<rbrakk> \<Longrightarrow> (fst x = Inr ()) = (fst y = Inr ()) \<and> snd x = snd y
 5. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 8. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. \<And>e tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelEntry e) \<in> full_invs_if\<rbrakk> \<Longrightarrow> (einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s
 2. \<And>e tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelEntry e) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 3. \<And>e tc x y. \<lbrakk>uop_nonempty uop; prod_lift (dc \<oplus> dc) x y\<rbrakk> \<Longrightarrow> (fst x = Inr ()) = (fst y = Inr ()) \<and> snd x = snd y
 4. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. \<And>e tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelEntry e) \<in> full_invs_if\<rbrakk> \<Longrightarrow> invs s \<and> valid_list s \<and> valid_sched s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s
 2. \<And>e tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelEntry e) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 3. \<And>e tc x y. \<lbrakk>uop_nonempty uop; prod_lift (dc \<oplus> dc) x y\<rbrakk> \<Longrightarrow> (fst x = Inr ()) = (fst y = Inr ()) \<and> snd x = snd y
 4. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 7. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. \<And>e tc x y. \<lbrakk>uop_nonempty uop; prod_lift (dc \<oplus> dc) x y\<rbrakk> \<Longrightarrow> (fst x = Inr ()) = (fst y = Inr ()) \<and> snd x = snd y
 2. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>e tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_if e tc)
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 3. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' kernel_handle_preemption_if handlePreemption_H_if
 2. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelPreempted full_invs_if full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handle_preemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 2. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (\<lambda>s. ((tc, s), KernelPreempted) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), KernelPreempted) \<in> full_invs_if') (handle_preemption_if tc) (handlePreemption_if tc)
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (handlePreemption_if tc)
 3. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (?Q244 tc) (?Q'244 tc) (handle_preemption_if tc) (handlePreemption_if tc)
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelPreempted) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q244 tc s
 3. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelPreempted) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'244 tc s
 4. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (handlePreemption_if tc)
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 6. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelPreempted) \<in> full_invs_if\<rbrakk> \<Longrightarrow> (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelPreempted) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (handlePreemption_if tc)
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelPreempted) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (handlePreemption_if tc)
 3. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (handlePreemption_if tc)
 2. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (3 subgoals):
 1. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' kernel_schedule_if schedule'_H_if
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 3. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (3 subgoals):
 1. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) (KernelSchedule b) full_invs_if full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule_if x xa)} {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 3. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. \<And>b tc. uop_nonempty uop \<Longrightarrow> corres (=) (\<lambda>s. ((tc, s), KernelSchedule b) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), KernelSchedule b) \<in> full_invs_if') (schedule_if tc) (schedule'_if tc)
 2. \<And>b tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (schedule'_if tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. \<And>b tc. uop_nonempty uop \<Longrightarrow> corres (=) (?Q253 b tc) (?Q'253 b tc) (schedule_if tc) (schedule'_if tc)
 2. \<And>b tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelSchedule b) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q253 b tc s
 3. \<And>b tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelSchedule b) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'253 b tc s
 4. \<And>b tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (schedule'_if tc)
 5. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>b tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelSchedule b) \<in> full_invs_if\<rbrakk> \<Longrightarrow> (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s
 2. \<And>b tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelSchedule b) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>b tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (schedule'_if tc)
 4. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. \<And>b tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelSchedule b) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 2. \<And>b tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (schedule'_if tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (3 subgoals):
 1. \<And>b tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (schedule'_if tc)
 2. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 3. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' kernel_exit_A_if kernelExit_H_if
 2. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres True (lift_snd_rel state_relation) KernelExit full_invs_if full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 2. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (6 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (\<lambda>s. ((tc, s), KernelExit) \<in> full_invs_if) (\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if') (kernel_exit_if tc) (kernelExit_if tc)
 2. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_if tc)
 3. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> state_relation; invs' s'; True\<rbrakk> \<Longrightarrow> (if ct_running s then InUserMode else InIdleMode) = (if ct_running' s' then InUserMode else InIdleMode)
 4. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 5. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (8 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres (=) (?Q263 tc) (?Q'263 tc) (kernel_exit_if tc) (kernelExit_if tc)
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> full_invs_if\<rbrakk> \<Longrightarrow> ?Q263 tc s
 3. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?Q'263 tc s
 4. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_if tc)
 5. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> state_relation; invs' s'; True\<rbrakk> \<Longrightarrow> (if ct_running s then InUserMode else InIdleMode) = (if ct_running' s' then InUserMode else InIdleMode)
 6. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 7. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (7 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> full_invs_if\<rbrakk> \<Longrightarrow> invs s
 2. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_if tc)
 4. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> state_relation; invs' s'; True\<rbrakk> \<Longrightarrow> (if ct_running s then InUserMode else InIdleMode) = (if ct_running' s' then InUserMode else InIdleMode)
 5. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 6. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (5 subgoals):
 1. \<And>tc. \<lbrakk>uop_nonempty uop; True\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_if tc)
 2. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> state_relation; invs' s'; True\<rbrakk> \<Longrightarrow> (if ct_running s then InUserMode else InIdleMode) = (if ct_running' s' then InUserMode else InIdleMode)
 3. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 4. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> state_relation; invs' s'; True\<rbrakk> \<Longrightarrow> (if ct_running s then InUserMode else InIdleMode) = (if ct_running' s' then InUserMode else InIdleMode)
 2. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> state_relation; invs' s'\<rbrakk> \<Longrightarrow> (ct_running s \<longrightarrow> ct_running' s') \<and> (\<not> ct_running s \<longrightarrow> \<not> ct_running' s')
 2. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (3 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if'\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (3 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 2. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (2 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> full_invs_if\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (1 subgoal):
 1. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernel_call_A_if Interrupt\<rbrakk> \<Longrightarrow> b = False proof (prove)
goal (1 subgoal):
 1. \<And>ab bc tc s'. \<lbrakk>uop_nonempty uop; ((Inl (), tc), s') \<in> fst (kernel_entry_if Interrupt ab bc)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!