theory Refine

lemma ckernel_invariant:
  "ADT_H uop \<Turnstile> full_invs'" unfolding full_invs'_def supply word_neq_0_conv[simp] supply domain_time_rel_eq[simp] domain_list_rel_eq[simp] apply (rule invariantI) apply (clarsimp simp add: ADT_H_def) apply (subst conj_commute, simp) apply (rule conjI) apply (drule ckernel_init_valid_duplicates'[rule_format], simp) apply (rule conjI) apply (frule init_refinement[simplified subset_eq, THEN bspec]) apply (clarsimp simp: ex_abs_def lift_state_relation_def) apply (frule akernel_init_invs[THEN bspec]) apply (rule_tac x = s in exI) apply (clarsimp simp: Init_A_def) apply (insert ckernel_init_invs)[1] apply clarsimp apply (frule ckernel_init_sch_norm) apply (frule ckernel_init_ctr) apply (frule ckernel_init_domain_time) apply (frule ckernel_init_domain_list) apply (fastforce simp: Init_H_def valid_domain_list'_def) apply (clarsimp simp: ADT_A_def ADT_H_def global_automaton_def) apply (erule_tac P="a \<and> (\<exists>x. b x)" for a b in disjE) apply (clarsimp simp: kernel_call_H_def) apply (drule use_valid[OF _ valid_corres_combined
                            [OF kernel_entry_invs entry_corres],
                            OF _ kernelEntry_invs'[THEN hoare_weaken_pre]]) subgoal by fastforce apply (fastforce simp: ex_abs_def sch_act_simple_def ct_running_related ct_idle_related
                           sched_act_rct_related) apply (clarsimp simp: kernel_call_H_def) subgoal by (fastforce simp: ex_abs_def sch_act_simple_def ct_running_related ct_idle_related
                              sched_act_rct_related) apply (erule_tac P="a \<and> b" for a b in disjE) apply (clarsimp simp add: do_user_op_H_def monad_to_transition_def) apply (drule use_valid) apply (rule hoare_vcg_conj_lift) apply (rule doUserOp_valid_duplicates') apply (rule valid_corres_combined[OF do_user_op_invs2 corres_guard_imp2[OF do_user_op_corres]]) apply clarsimp apply (rule doUserOp_invs'[THEN hoare_weaken_pre]) apply (fastforce simp: ex_abs_def) apply (clarsimp simp: ex_abs_def, rule_tac x=s in exI,
            clarsimp simp: ct_running_related sched_act_rct_related) apply (clarsimp simp: ex_abs_def) apply (fastforce simp: ex_abs_def ct_running_related sched_act_rct_related) apply (erule_tac P="a \<and> b \<and> c \<and> (\<exists>x. d x)" for a b c d in disjE) apply (clarsimp simp add: do_user_op_H_def monad_to_transition_def) apply (drule use_valid) apply (rule hoare_vcg_conj_lift) apply (rule doUserOp_valid_duplicates') apply (rule valid_corres_combined[OF do_user_op_invs2 corres_guard_imp2[OF do_user_op_corres]]) apply clarsimp apply (rule doUserOp_invs'[THEN hoare_weaken_pre]) apply (fastforce simp: ex_abs_def) apply (fastforce simp: ex_abs_def ct_running_related sched_act_rct_related) apply (fastforce simp: ex_abs_def) apply (erule_tac P="a \<and> b" for a b in disjE) apply (clarsimp simp: check_active_irq_H_def) apply (drule use_valid) apply (rule hoare_vcg_conj_lift) apply (rule checkActiveIRQ_valid_duplicates') apply (rule valid_corres_combined[OF check_active_irq_invs_just_running checkActiveIRQ_just_running_corres]) apply (rule checkActiveIRQ_invs'_just_running[THEN hoare_weaken_pre]) apply (fastforce simp: ex_abs_def) apply (fastforce simp: ex_abs_def ct_running_related sched_act_rct_related) apply (fastforce simp: ex_abs_def) apply (erule_tac P="a \<and> b" for a b in disjE) apply (clarsimp simp: check_active_irq_H_def) apply (drule use_valid) apply (rule hoare_vcg_conj_lift) apply (rule checkActiveIRQ_valid_duplicates') apply (rule valid_corres_combined[OF check_active_irq_invs_just_idle checkActiveIRQ_just_idle_corres]) apply (rule checkActiveIRQ_invs'_just_idle[THEN hoare_weaken_pre]) apply clarsimp apply (fastforce simp: ex_abs_def) apply (fastforce simp: ex_abs_def ct_idle_related sched_act_rct_related) apply (fastforce simp: ex_abs_def) apply (clarsimp simp: check_active_irq_H_def) apply (drule use_valid) apply (rule hoare_vcg_conj_lift) apply (rule checkActiveIRQ_valid_duplicates') apply (rule valid_corres_combined[OF check_active_irq_invs check_active_irq_corres]) apply (rule checkActiveIRQ_invs'[THEN hoare_weaken_pre]) apply clarsimp apply (fastforce simp: ex_abs_def) apply (fastforce simp: ex_abs_def ct_running_related ct_idle_related sched_act_rct_related) apply (fastforce simp: ex_abs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<Turnstile> full_invs' proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<Turnstile> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<Turnstile> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<Turnstile> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<forall>s. Init (ADT_H uop) s \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s}
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> vs_valid_duplicates' (ksPSpace b)
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 3. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ex_abs einvs b
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 3. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; ((a, b), aa, ba) \<in> lift_state_relation state_relation `` Init_A\<rbrakk> \<Longrightarrow> ex_abs einvs b
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 3. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' m e tc. \<lbrakk>((tc, s'), m, e) \<in> Init_H; ((tc, s), m, e) \<in> Init_A; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 3. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' m e tc. \<lbrakk>((tc, s'), m, e) \<in> Init_H; ((tc, s), m, e) \<in> Init_A; (s, s') \<in> state_relation; case ((tc, s), m, e) of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>(m, e). invs s \<and> ct_running s) xa\<rbrakk> \<Longrightarrow> \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 3. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' m e tc. \<lbrakk>((tc, s'), m, e) \<in> Init_H; ((tc, s), m, e) \<in> Init_A; (s, s') \<in> state_relation; case ((tc, s), m, e) of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>(m, e). invs s \<and> ct_running s) xa\<rbrakk> \<Longrightarrow> (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 3. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_H \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; \<forall>((tc, s), x)\<in>Init_H. invs' s\<rbrakk> \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; \<forall>x\<in>Init_H. case x of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>x. invs' s) xa\<rbrakk> \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; \<forall>x\<in>Init_H. case x of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>x. invs' s) xa; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; \<forall>x\<in>Init_H. case x of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>x. invs' s) xa; ksSchedulerAction b = ResumeCurrentThread; ct_running' b\<rbrakk> \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; \<forall>x\<in>Init_H. case x of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>x. invs' s) xa; ksSchedulerAction b = ResumeCurrentThread; ct_running' b; ksDomainTime b \<noteq> 0\<rbrakk> \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_H; \<forall>x\<in>Init_H. case x of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>x. invs' s) xa; ksSchedulerAction b = ResumeCurrentThread; ct_running' b; ksDomainTime b \<noteq> 0; 0 < length (ksDomSchedule b) \<and> (\<forall>(d, time)\<in>set (ksDomSchedule b). 0 < time)\<rbrakk> \<Longrightarrow> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b \<and> invs' b
 2. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step (ADT_H uop) j `` {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} \<subseteq> {((tc, s), m, e). invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ex_abs einvs s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> (ct_running' s \<or> ct_idle' s) \<and> (m = KernelMode \<longrightarrow> e \<noteq> None) \<and> (m = UserMode \<longrightarrow> ct_running' s) \<and> (m = IdleMode \<longrightarrow> ct_idle' s) \<and> (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> 0 < ksDomainTime s \<and> valid_domain_list' s} proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>ac = KernelMode \<and> (\<exists>e. bc = Some e \<and> ba = None \<and> ((ab, bb), aa, a, b) \<in> kernel_call_H e) \<or> ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H; invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = KernelMode \<and> (\<exists>x. bc = Some x \<and> ba = None \<and> ((ab, bb), aa, a, b) \<in> kernel_call_H x)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (a, b) \<in> fst (kernelEntry x ab bb)\<rbrakk> \<Longrightarrow> (ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> 0 < ksDomainTime b \<and> valid_domain_list' b) \<and> (\<not> ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb x s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>sa. (sa, s) \<in> state_relation \<and> (einvs and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) sa \<and> (invs' and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') s
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<exists>s. (s, bb) \<in> state_relation \<and> (einvs and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> (invs' and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) bb
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>r s. (s, b) \<in> state_relation \<and> (einvs and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle')) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = a\<rbrakk> \<Longrightarrow> (ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> 0 < ksDomainTime b \<and> valid_domain_list' b) \<and> (\<not> ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b)
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' bb_; vs_valid_duplicates' (ksPSpace bb_); ex_abs einvs bb_; ksSchedulerAction bb_ = ResumeCurrentThread; ct_running' bb_ \<or> ct_idle' bb_; x_ \<noteq> Interrupt \<longrightarrow> ct_running' bb_; 0 < ksDomainTime bb_; valid_domain_list' bb_; \<exists>sa. (sa, s_) \<in> state_relation \<and> (einvs and (\<lambda>s. x_ \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) sa \<and> (invs' and (\<lambda>s. x_ \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s_\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>s. x_ \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') s_ proof (prove)
goal (3 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<exists>s. (s, bb) \<in> state_relation \<and> (einvs and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> (invs' and (\<lambda>s. x \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) bb
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>r s. (s, b) \<in> state_relation \<and> (einvs and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle')) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = a\<rbrakk> \<Longrightarrow> (ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> 0 < ksDomainTime b \<and> valid_domain_list' b) \<and> (\<not> ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b)
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>r s. (s, b) \<in> state_relation \<and> (einvs and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle')) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = a\<rbrakk> \<Longrightarrow> (ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> 0 < ksDomainTime b \<and> valid_domain_list' b) \<and> (\<not> ct_running' b \<longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb x s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; x \<noteq> Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (s, b) \<in> state_relation; invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); ct_running s \<or> ct_idle s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ksSchedulerAction b = ResumeCurrentThread; invs' b; ct_running' b \<or> ct_idle' b; vs_valid_duplicates' (ksPSpace b)\<rbrakk> \<Longrightarrow> (ct_running' b \<longrightarrow> ex_abs einvs b) \<and> (\<not> ct_running' b \<longrightarrow> ex_abs einvs b \<and> ct_idle' b)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' bb_; vs_valid_duplicates' (ksPSpace bb_); ex_abs einvs bb_; ksSchedulerAction bb_ = ResumeCurrentThread; ct_running' bb_ \<or> ct_idle' bb_; x_ \<noteq> Interrupt \<longrightarrow> ct_running' bb_; 0 < ksDomainTime bb_; valid_domain_list' bb_; (s_, b_) \<in> state_relation; invs s_; valid_list s_; valid_sched_2 (ready_queues s_) (ekheap s_) resume_cur_thread (cur_domain s_) (kheap s_) (cur_thread s_) (idle_thread s_); ct_running s_ \<or> ct_idle s_; 0 < domain_time s_; valid_domain_list s_; scheduler_action s_ = resume_cur_thread; ksSchedulerAction b_ = ResumeCurrentThread; invs' b_; ct_running' b_ \<or> ct_idle' b_; vs_valid_duplicates' (ksPSpace b_)\<rbrakk> \<Longrightarrow> (ct_running' b_ \<longrightarrow> ex_abs einvs b_) \<and> (\<not> ct_running' b_ \<longrightarrow> ex_abs einvs b_ \<and> ct_idle' b_) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_H uop\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ((None, a), b) \<in> fst (doUserOp uop ab bb)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P202 a b ab bb\<rbrace> doUserOp uop ab \<lbrace>?Q202 a b ab bb\<rbrace>
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P202 a b ab bb bb
 3. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q202 a b ab bb (None, a) b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (5 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P209 a b ab bb\<rbrace> doUserOp uop ab \<lbrace>?Q209 a b ab bb\<rbrace>
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'209 a b ab bb\<rbrace> doUserOp uop ab \<lbrace>?Q'209 a b ab bb\<rbrace>
 3. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P209 a b ab bb bb \<and> ?P'209 a b ab bb bb
 4. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q209 a b ab bb (None, a) b \<and> ?Q'209 a b ab bb (None, a) b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'209 a b ab bb\<rbrace> doUserOp uop ab \<lbrace>?Q'209 a b ab bb\<rbrace>
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> ?P'209 a b ab bb bb
 3. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> ?Q'209 a b ab bb (None, a) b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (5 subgoals):
 1. \<And>a b ab bb s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s\<rbrakk> \<Longrightarrow> (einvs and ct_running) s
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'\<rbrace> doUserOp uop ab \<lbrace>?Q'213 a b ab bb\<rbrace>
 3. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 4. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'213 a b ab bb (None, a) b \<and> r = (None, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'\<rbrace> doUserOp uop ab \<lbrace>?Q'213 a b ab bb\<rbrace>
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 3. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'213 a b ab bb (None, a) b \<and> r = (None, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>sa. (sa, s) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) sa \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> (invs' and ex_abs einvs and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') s
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 3. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = (None, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 2. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = (None, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = (None, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_running' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb s sa. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < domain_time s; valid_domain_list s; vs_valid_duplicates' (ksPSpace b); (s, bb) \<in> state_relation; (sa, b) \<in> state_relation; invs s; invs sa; valid_list s; valid_sched s; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); ct_running sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' b; ksSchedulerAction b = ResumeCurrentThread; ct_running' b\<rbrakk> \<Longrightarrow> \<exists>s. (s, b) \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>e. ba = Some e \<and> ((ab, bb), Some e, a, b) \<in> do_user_op_H uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> (\<exists>x. ba = Some x \<and> ((ab, bb), Some x, a, b) \<in> do_user_op_H uop)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ((Some x, a), b) \<in> fst (doUserOp uop ab bb)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P296 a b ab bb x\<rbrace> doUserOp uop ab \<lbrace>?Q296 a b ab bb x\<rbrace>
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P296 a b ab bb x bb
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q296 a b ab bb x (Some x, a) b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (5 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P303 a b ab bb x\<rbrace> doUserOp uop ab \<lbrace>?Q303 a b ab bb x\<rbrace>
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'303 a b ab bb x\<rbrace> doUserOp uop ab \<lbrace>?Q'303 a b ab bb x\<rbrace>
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P303 a b ab bb x bb \<and> ?P'303 a b ab bb x bb
 4. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q303 a b ab bb x (Some x, a) b \<and> ?Q'303 a b ab bb x (Some x, a) b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'303 a b ab bb x\<rbrace> doUserOp uop ab \<lbrace>?Q'303 a b ab bb x\<rbrace>
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> ?P'303 a b ab bb x bb
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> ?Q'303 a b ab bb x (Some x, a) b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (5 subgoals):
 1. \<And>a b ab bb x s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s\<rbrakk> \<Longrightarrow> (einvs and ct_running) s
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'\<rbrace> doUserOp uop ab \<lbrace>?Q'307 a b ab bb x\<rbrace>
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 4. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'307 a b ab bb x (Some x, a) b \<and> r = (Some x, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s'\<rbrace> doUserOp uop ab \<lbrace>?Q'307 a b ab bb x\<rbrace>
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'307 a b ab bb x (Some x, a) b \<and> r = (Some x, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>a b ab bb x s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>sa. (sa, s) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) sa \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') s\<rbrakk> \<Longrightarrow> (invs' and ex_abs einvs and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') s
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 3. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = (Some x, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running') bb)
 2. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = (Some x, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb x. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') b \<and> r = (Some x, a))\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (x \<noteq> Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (True, b) \<in> fst (checkActiveIRQ bb)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P400 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q400 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P400 b bb bb
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q400 b bb True b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (5 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P404 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q404 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'404 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q'404 b bb\<rbrace>
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P404 b bb bb \<and> ?P'404 b bb bb
 4. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q404 b bb True b \<and> ?Q'404 b bb True b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'404 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q'404 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> ?P'404 b bb bb
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> ?Q'404 b bb True b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s'\<rbrace> checkActiveIRQ \<lbrace>?Q'407 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_running and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'407 b bb True b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>sa. (sa, s) \<in> state_relation \<and> (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) sa \<and> (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (invs' and ex_abs invs and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_running and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_running and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_running and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (False, b) \<in> fst (checkActiveIRQ bb)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P483 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q483 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P483 b bb bb
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q483 b bb False b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (5 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P487 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q487 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'487 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q'487 b bb\<rbrace>
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P487 b bb bb \<and> ?P'487 b bb bb
 4. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q487 b bb False b \<and> ?Q'487 b bb False b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'487 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q'487 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> ?P'487 b bb bb
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> ?Q'487 b bb False b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s'\<rbrace> checkActiveIRQ \<lbrace>?Q'490 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_idle and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'490 b bb False b \<and> r = False)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>sa. (sa, s) \<in> state_relation \<and> (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) sa \<and> (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (invs' and ex_abs invs and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_idle and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = False)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>bb s sa. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (sa, s) \<in> state_relation; ct_idle sa; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; ct_idle' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ex_abs invs s
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_idle and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = False)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) bb)
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_idle and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = False)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and ct_idle and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = False)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> ct_idle' b \<and> 0 < ksDomainTime b \<and> valid_domain_list' b
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_running' bb \<or> ct_idle' bb; ac = KernelMode \<longrightarrow> (\<exists>y. bc = Some y); ac = UserMode \<longrightarrow> ct_running' bb; ac = IdleMode \<longrightarrow> ct_idle' bb; (\<exists>y. bc = Some y) \<and> bc \<noteq> Some Interrupt \<longrightarrow> ct_running' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_H\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> (aa = KernelMode \<longrightarrow> (\<exists>y. ba = Some y)) \<and> (aa = UserMode \<longrightarrow> ct_running' b) \<and> (aa = IdleMode \<longrightarrow> ct_idle' b) \<and> ((\<exists>y. ba = Some y) \<and> ba \<noteq> Some Interrupt \<longrightarrow> ct_running' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (True, b) \<in> fst (checkActiveIRQ bb)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P560 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q560 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P560 b bb bb
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q560 b bb True b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (4 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P564 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q564 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'564 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q'564 b bb\<rbrace>
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> ?P564 b bb bb \<and> ?P'564 b bb bb
 4. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; ?Q564 b bb True b \<and> ?Q'564 b bb True b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>?P'564 b bb\<rbrace> checkActiveIRQ \<lbrace>?Q'564 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> ?P'564 b bb bb
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> ?Q'564 b bb True b\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'\<rbrace> checkActiveIRQ \<lbrace>?Q'567 b bb\<rbrace>
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> ?Q'567 b bb True b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>b bb s. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; \<exists>sa. (sa, s) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) sa \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (invs' and ex_abs invs and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (3 subgoals):
 1. \<And>bb s sa. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; (sa, s) \<in> state_relation; ct_running sa \<or> ct_idle sa; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; ksSchedulerAction s = ResumeCurrentThread; ct_running' s \<or> ct_idle' s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> ex_abs invs s
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) bb)
 3. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (2 subgoals):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace bb) \<and> (\<exists>s. (s, bb) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) bb)
 2. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal (1 subgoal):
 1. \<And>b bb. \<lbrakk>invs' bb; vs_valid_duplicates' (ksPSpace bb); ex_abs einvs bb; ksSchedulerAction bb = ResumeCurrentThread; ct_idle' bb; 0 < ksDomainTime bb; valid_domain_list' bb; vs_valid_duplicates' (ksPSpace b) \<and> (\<exists>r s. (s, b) \<in> state_relation \<and> (invs and (ct_running or ct_idle) and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<and> (invs' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) b \<and> r = True)\<rbrakk> \<Longrightarrow> invs' b \<and> vs_valid_duplicates' (ksPSpace b) \<and> ex_abs einvs b \<and> ksSchedulerAction b = ResumeCurrentThread \<and> (ct_running' b \<or> ct_idle' b) \<and> 0 < ksDomainTime b \<and> valid_domain_list' b proof (prove)
goal:
No subgoals!