theory ADT_IF_Refine_C

lemma c_to_haskell:
  "uop_nonempty uop
   \<Longrightarrow> global_automata_refine 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
         check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if
         schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) (lift_snd_rel rf_sr) False" apply (simp add: global_automata_refine_def) apply (intro conjI) apply (rule haskell_invs) apply (unfold_locales) apply (simp add: ADT_C_if_def) apply (simp_all add: preserves_trivial preserves'_trivial) apply (clarsimp simp: lift_snd_rel_def ADT_C_if_def ADT_H_if_def absKState_crelation
                                rf_sr_def full_invs_if'_def) apply (clarsimp simp: rf_sr_def full_invs_if'_def ex_abs_def) apply (simp add: ADT_H_if_def ADT_C_if_def lift_fst_rel_def lift_snd_rel_def) apply safe apply (clarsimp simp: absKState_crelation  rf_sr_def full_invs_if'_def) apply (rule_tac x="((a,bb),ba)" in bexI) apply simp apply simp apply (frule cstate_to_H_correct[rotated],simp add: invs'_def) apply (case_tac ba,simp_all) apply (simp_all add: checkActiveIRQ_H_if_def check_active_irq_C_if_def
                             doUserOp_H_if_def do_user_op_C_if_def
                             kernelCall_H_if_def kernel_call_C_if_def
                             handlePreemption_H_if_def handle_preemption_C_if_def
                             schedule'_H_if_def schedule_C_if_def
                             kernelExit_H_if_def kernel_exit_C_if_def) apply (rule step_corres_lifts,rule corres_guard_imp[OF check_active_irq_corres_C]; fastforce simp: full_invs_if'_def) apply (rule step_corres_lifts,rule corres_guard_imp[OF check_active_irq_corres_C]; fastforce simp: full_invs_if'_def) apply (rule step_corres_lifts,rule corres_guard_imp[OF do_user_op_if_C_corres]; auto simp: full_invs_if'_def ex_abs_def) apply (rule step_corres_lifts) apply (rule corres_rel_imp) apply (rule corres_guard_imp[OF kernelEntry_corres_C],(clarsimp simp: prod_lift_def)+) apply (rule step_corres_lifts,rule corres_guard_imp[OF handle_preemption_corres_C]; auto simp add: full_invs_if'_def) apply (rule step_corres_lifts,rule corres_guard_imp[OF schedule_if_corres_C]; auto simp: full_invs_if'_def ex_abs_def) apply (rule_tac S="invs'" and S'="\<top>" in step_corres_lifts(5)) apply (rule corres_guard_imp[OF kernel_exit_corres_C]) apply (fastforce simp: full_invs_if'_def) apply simp+ apply (simp add: ct_running'_C) apply wp+ apply (clarsimp simp: full_invs_if'_def) apply (clarsimp) apply (drule use_valid[OF _ kernelEntry_if_no_preempt]; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> global_automata_refine 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 check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) (lift_snd_rel rf_sr) False proof (prove)
goal (1 subgoal):
 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 \<and> global_automaton_invs check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) UNIV \<and> global_automata_refine_axioms 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 check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) (lift_snd_rel rf_sr) False proof (prove)
goal (3 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_automaton_invs check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) UNIV
 3. uop_nonempty uop \<Longrightarrow> global_automata_refine_axioms 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 check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) (lift_snd_rel rf_sr) False proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> global_automaton_invs check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) UNIV
 2. uop_nonempty uop \<Longrightarrow> global_automata_refine_axioms 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 check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if UNIV (ADT_C_if fp uop) (lift_snd_rel rf_sr) False proof (prove)
goal (24 subgoals):
 1. uop_nonempty uop \<Longrightarrow> Step (ADT_C_if fp uop) = (\<lambda>u. global_automaton_if check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if kernel_exit_C_if \<inter> {(s, s'). s' \<in> UNIV})
 2. uop_nonempty uop \<Longrightarrow> preserves InUserMode InUserMode UNIV check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> preserves InIdleMode InIdleMode UNIV check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> preserves InUserMode (KernelEntry Interrupt) UNIV check_active_irq_C_if
 5. uop_nonempty uop \<Longrightarrow> preserves InIdleMode (KernelEntry Interrupt) UNIV check_active_irq_C_if
 6. uop_nonempty uop \<Longrightarrow> preserves InUserMode InUserMode UNIV (do_user_op_C_if uop)
 7. \<And>e. uop_nonempty uop \<Longrightarrow> preserves InUserMode (KernelEntry e) UNIV (do_user_op_C_if uop)
 8. \<And>e. \<lbrakk>uop_nonempty uop; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> preserves (KernelEntry e) KernelPreempted UNIV (kernel_call_C_if fp e)
 9. \<And>e. uop_nonempty uop \<Longrightarrow> preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) UNIV (kernel_call_C_if fp e)
 10. uop_nonempty uop \<Longrightarrow> preserves KernelPreempted (KernelSchedule True) UNIV handle_preemption_C_if
A total of 24 subgoals... proof (prove)
goal (23 subgoals):
 1. uop_nonempty uop \<Longrightarrow> preserves InUserMode InUserMode UNIV check_active_irq_C_if
 2. uop_nonempty uop \<Longrightarrow> preserves InIdleMode InIdleMode UNIV check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> preserves InUserMode (KernelEntry Interrupt) UNIV check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> preserves InIdleMode (KernelEntry Interrupt) UNIV check_active_irq_C_if
 5. uop_nonempty uop \<Longrightarrow> preserves InUserMode InUserMode UNIV (do_user_op_C_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> preserves InUserMode (KernelEntry e) UNIV (do_user_op_C_if uop)
 7. \<And>e. \<lbrakk>uop_nonempty uop; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> preserves (KernelEntry e) KernelPreempted UNIV (kernel_call_C_if fp e)
 8. \<And>e. uop_nonempty uop \<Longrightarrow> preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) UNIV (kernel_call_C_if fp e)
 9. uop_nonempty uop \<Longrightarrow> preserves KernelPreempted (KernelSchedule True) UNIV handle_preemption_C_if
 10. \<And>b. uop_nonempty uop \<Longrightarrow> preserves (KernelSchedule b) KernelExit UNIV schedule_C_if
A total of 23 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s s' mode. \<lbrakk>uop_nonempty uop; (s, s') \<in> lift_snd_rel rf_sr; (s, mode) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> Fin (ADT_C_if fp uop) (s', mode) = Fin (ADT_H_if uop) (s, mode)
 2. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_C_if fp uop) a \<subseteq> lift_fst_rel (lift_snd_rel rf_sr) `` Init (ADT_H_if uop) a
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 5. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 7. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 9. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 10. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernelCall_H_if Interrupt\<rbrakk> \<Longrightarrow> \<not> b proof (prove)
goal (9 subgoals):
 1. \<And>a. uop_nonempty uop \<Longrightarrow> Init (ADT_C_if fp uop) a \<subseteq> lift_fst_rel (lift_snd_rel rf_sr) `` Init (ADT_H_if uop) a
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernelCall_H_if Interrupt\<rbrakk> \<Longrightarrow> \<not> b proof (prove)
goal (9 subgoals):
 1. \<And>a b ba aa bb bc. \<lbrakk>uop_nonempty uop; ((aa, bb), bc) \<in> Init (ADT_C_if fp uop) ((a, b), ba)\<rbrakk> \<Longrightarrow> ((aa, bb), bc) \<in> lift_fst_rel (lift_snd_rel {(s, s'). cstate_relation s (globals s')}) `` Init (ADT_H_if uop) ((a, b), ba)
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernelCall_H_if Interrupt\<rbrakk> \<Longrightarrow> \<not> b proof (prove)
goal (9 subgoals):
 1. \<And>a ba b. \<lbrakk>uop_nonempty uop; \<exists>a bb. (bb, b) \<in> rf_sr \<and> ((a, bb), ba) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> \<exists>r\<in>({a} \<times> {s'. absKState s' = cstate_to_A b}) \<times> {ba} \<inter> full_invs_if'. snd r = ba \<and> fst (fst r) = a \<and> cstate_relation (internal_state_if r) (globals b)
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>s s' b. \<lbrakk>uop_nonempty uop; (s, b, s') \<in> kernelCall_H_if Interrupt\<rbrakk> \<Longrightarrow> \<not> b proof (prove)
goal (9 subgoals):
 1. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; (bb, b) \<in> rf_sr; ((aa, bb), ba) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> \<exists>r\<in>({a} \<times> {s'. absKState s' = cstate_to_A b}) \<times> {ba} \<inter> full_invs_if'. snd r = ba \<and> fst (fst r) = a \<and> cstate_relation (internal_state_if r) (globals b)
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), bb, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (9 subgoals):
 1. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; cstate_relation bb (globals b); invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<exists>r\<in>({a} \<times> {s'. absKState s' = absKState bb}) \<times> {ba} \<inter> {s. invs' (internal_state_if s) \<and> ex_abs einvs (internal_state_if s) \<and> vs_valid_duplicates' (ksPSpace (internal_state_if s)) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime (internal_state_if s)) \<and> (ksDomainTime (internal_state_if s) = 0 \<longrightarrow> ksSchedulerAction (internal_state_if s) = ChooseNewThread) \<and> valid_domain_list' (internal_state_if s) \<and> (case snd s of InUserMode \<Rightarrow> ct_running' (internal_state_if s) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if s) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if s) \<and> ksDomainTime (internal_state_if s) \<noteq> 0) \<and> (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if s) \<noteq> 0 | _ \<Rightarrow> True)}. snd r = ba \<and> fst (fst r) = a \<and> cstate_relation (internal_state_if r) (globals b)
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), bb, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (10 subgoals):
 1. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; cstate_relation bb (globals b); invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> snd ((a, bb), ba) = ba \<and> fst (fst ((a, bb), ba)) = a \<and> cstate_relation (internal_state_if ((a, bb), ba)) (globals b)
 2. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; cstate_relation bb (globals b); invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> ((a, bb), ba) \<in> ({a} \<times> {s'. absKState s' = absKState bb}) \<times> {ba} \<inter> {s. invs' (internal_state_if s) \<and> ex_abs einvs (internal_state_if s) \<and> vs_valid_duplicates' (ksPSpace (internal_state_if s)) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime (internal_state_if s)) \<and> (ksDomainTime (internal_state_if s) = 0 \<longrightarrow> ksSchedulerAction (internal_state_if s) = ChooseNewThread) \<and> valid_domain_list' (internal_state_if s) \<and> (case snd s of InUserMode \<Rightarrow> ct_running' (internal_state_if s) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if s) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if s) \<and> ksDomainTime (internal_state_if s) \<noteq> 0) \<and> (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if s) \<noteq> 0 | _ \<Rightarrow> True)}
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 5. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 6. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 7. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 8. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 9. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 10. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), bb, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (9 subgoals):
 1. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; cstate_relation bb (globals b); invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> ((a, bb), ba) \<in> ({a} \<times> {s'. absKState s' = absKState bb}) \<times> {ba} \<inter> {s. invs' (internal_state_if s) \<and> ex_abs einvs (internal_state_if s) \<and> vs_valid_duplicates' (ksPSpace (internal_state_if s)) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime (internal_state_if s)) \<and> (ksDomainTime (internal_state_if s) = 0 \<longrightarrow> ksSchedulerAction (internal_state_if s) = ChooseNewThread) \<and> valid_domain_list' (internal_state_if s) \<and> (case snd s of InUserMode \<Rightarrow> ct_running' (internal_state_if s) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if s) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if s) \<and> ksDomainTime (internal_state_if s) \<noteq> 0) \<and> (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> ksSchedulerAction (internal_state_if s) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if s) \<noteq> 0 | _ \<Rightarrow> True)}
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), bb, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (9 subgoals):
 1. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; cstate_relation bb (globals b); invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> 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
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), bb, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (9 subgoals):
 1. \<And>a ba b aa bb. \<lbrakk>uop_nonempty uop; cstate_relation bb (globals b); invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); ba \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case ba of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), ba)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), ba)) \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), ba)) \<or> ct_idle' (internal_state_if ((aa, bb), ba))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), ba)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), ba)) \<noteq> 0 | _ \<Rightarrow> True; cstate_to_H (globals b) = bb\<lparr>ksMachineState := observable_memory (ksMachineState bb) (user_mem' bb)\<rparr>\<rbrakk> \<Longrightarrow> 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
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 5. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 7. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 8. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 9. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), bb, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV checkActiveIRQ_H_if check_active_irq_C_if
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV (doUserOp_H_if uop) (do_user_op_C_if uop)
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV (kernelCall_H_if e) (kernel_call_C_if fp e)
 5. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV handlePreemption_H_if handle_preemption_C_if
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV schedule'_H_if schedule_C_if
 7. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV kernelExit_H_if kernel_exit_C_if
 8. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; ((a, b), True, aa, ba) \<in> kernelCall_H_if Interrupt; bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)} {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_C_if tc s)}
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)} {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_C_if tc s)}
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_if uop a b)} {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_C_if uop a b)}
 4. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV {((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 ())} {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_C_if fp e a b) \<and> ba = (r \<noteq> Inr ())}
 5. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 6. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 7. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 8. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (7 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InIdleMode full_invs_if' UNIV {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)} {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_C_if tc s)}
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_if uop a b)} {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_C_if uop a b)}
 3. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV {((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 ())} {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_C_if fp e a b) \<and> ba = (r \<noteq> Inr ())}
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 7. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) InUserMode full_invs_if' UNIV {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_if uop a b)} {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_C_if uop a b)}
 2. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV {((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 ())} {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_C_if fp e a b) \<and> ba = (r \<noteq> Inr ())}
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 5. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 6. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>e. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelEntry e) full_invs_if' UNIV {((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 ())} {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_C_if fp e a b) \<and> ba = (r \<noteq> Inr ())}
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 3. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 5. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>e tc. uop_nonempty uop \<Longrightarrow> corres_underlying rf_sr False False (\<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> UNIV) (kernelEntry_if e tc) (kernelEntry_C_if fp e tc)
 2. \<And>e tc. \<lbrakk>uop_nonempty uop; False\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_C_if fp e tc)
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 4. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 5. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 6. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (7 subgoals):
 1. \<And>e tc. uop_nonempty uop \<Longrightarrow> corres_underlying rf_sr False False (?r'95 e tc) (\<lambda>s. ((tc, s), KernelEntry e) \<in> full_invs_if') (\<lambda>s'. ((tc, s'), KernelEntry e) \<in> UNIV) (kernelEntry_if e tc) (kernelEntry_C_if fp e tc)
 2. \<And>e tc x y. \<lbrakk>uop_nonempty uop; ?r'95 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; False\<rbrakk> \<Longrightarrow> empty_fail (kernelEntry_C_if fp e tc)
 4. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 5. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 6. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 7. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelPreempted full_invs_if' UNIV {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_C_if x xa)}
 2. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 3. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 4. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) (KernelSchedule b) full_invs_if' UNIV {(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_C_if' x xa)}
 2. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 3. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> step_corres False (lift_snd_rel rf_sr) KernelExit full_invs_if' UNIV {(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)} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_C_if x xa) \<and> m = (if ct_running_C (snd s') then InUserMode else InIdleMode)}
 2. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> corres_underlying rf_sr False False (=) (\<lambda>s. ((tc, s), KernelExit) \<in> full_invs_if') (\<lambda>s'. ((tc, s'), KernelExit) \<in> UNIV) (kernelExit_if tc) (kernelExit_C_if tc)
 2. \<And>tc. \<lbrakk>uop_nonempty uop; False\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_C_if tc)
 3. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> rf_sr; True; invs' s\<rbrakk> \<Longrightarrow> (if ct_running' s then InUserMode else InIdleMode) = (if ct_running_C s' then InUserMode else InIdleMode)
 4. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> UNIV\<rbrace> kernelExit_C_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 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>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> 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> UNIV\<rbrakk> \<Longrightarrow> True
 3. \<And>tc. \<lbrakk>uop_nonempty uop; False\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_C_if tc)
 4. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> rf_sr; True; invs' s\<rbrakk> \<Longrightarrow> (if ct_running' s then InUserMode else InIdleMode) = (if ct_running_C s' then InUserMode else InIdleMode)
 5. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> UNIV\<rbrace> kernelExit_C_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 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>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> UNIV\<rbrakk> \<Longrightarrow> True
 2. \<And>tc. \<lbrakk>uop_nonempty uop; False\<rbrakk> \<Longrightarrow> empty_fail (kernelExit_C_if tc)
 3. \<And>tc s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> rf_sr; True; invs' s\<rbrakk> \<Longrightarrow> (if ct_running' s then InUserMode else InIdleMode) = (if ct_running_C s' then InUserMode else InIdleMode)
 4. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> UNIV\<rbrace> kernelExit_C_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 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>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>uop_nonempty uop; (s, s') \<in> rf_sr; invs' s\<rbrakk> \<Longrightarrow> (if ct_running' s then InUserMode else InIdleMode) = (if ct_running_C s' then InUserMode else InIdleMode)
 2. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> UNIV\<rbrace> kernelExit_C_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 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>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>tc. uop_nonempty uop \<Longrightarrow> \<lbrace>\<lambda>s'. ((tc, s'), KernelExit) \<in> UNIV\<rbrace> kernelExit_C_if tc \<lbrace>\<lambda>_ _. True\<rbrace>
 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>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>tc s. \<lbrakk>uop_nonempty uop; ((tc, s), KernelExit) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> invs' s
 2. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba bb. \<lbrakk>uop_nonempty uop; \<exists>bb. bb \<and> (\<exists>r. ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b) \<and> bb = (r \<noteq> Inr ())); bb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba bb r. \<lbrakk>uop_nonempty uop; bb; r \<noteq> Inr (); ((r, aa), ba) \<in> fst (kernelEntry_if Interrupt a b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!