theory Refine

lemma akernel_invariant:
  "ADT_A uop \<Turnstile> full_invs" unfolding full_invs_def apply (rule invariantI) apply (clarsimp simp: ADT_A_def subset_iff) apply (frule bspec[OF akernel_init_invs]) apply (simp add: Let_def Init_A_def) apply (simp add: init_A_st_def ext_init_def) apply (clarsimp simp: ADT_A_def global_automaton_def) apply (rename_tac tc' s' mode' e' tc s mode e) apply (elim disjE) apply ((clarsimp simp: kernel_call_A_def
                   | drule use_valid[OF _ kernel_entry_invs])+)[2] apply ((clarsimp simp: do_user_op_A_def monad_to_transition_def
                                  check_active_irq_A_def
                 | drule use_valid[OF _ do_user_op_invs2]
                 | drule use_valid[OF _ check_active_irq_invs_just_running])+)[2] apply ((clarsimp simp add: check_active_irq_A_def
               | drule use_valid[OF _ check_active_irq_invs])+)[1] apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) apply ((clarsimp simp add: do_user_op_A_def check_active_irq_A_def
             | drule use_valid[OF _ do_user_op_invs2]
             | drule use_valid[OF _ check_active_irq_invs_just_running])+)[1] apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) apply ((clarsimp simp add: check_active_irq_A_def
         | drule use_valid[OF _ check_active_irq_invs])+)[1] apply ((clarsimp simp add: check_active_irq_A_def
        | drule use_valid[OF _ check_active_irq_invs_just_idle])+)[1] apply ((clarsimp simp add: check_active_irq_A_def
        | drule use_valid[OF _ check_active_irq_invs])+)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_A uop \<Turnstile> full_invs proof (prove)
goal (1 subgoal):
 1. ADT_A uop \<Turnstile> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} proof (prove)
goal (2 subgoals):
 1. \<forall>s. Init (ADT_A uop) s \<subseteq> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread}
 2. \<forall>j. Step (ADT_A uop) j `` {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} \<subseteq> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> Init_A \<Longrightarrow> invs b \<and> valid_list b \<and> valid_sched b \<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 < domain_time b \<and> valid_domain_list b \<and> scheduler_action b = resume_cur_thread
 2. \<forall>j. Step (ADT_A uop) j `` {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} \<subseteq> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Init_A; case ((a, b), aa, ba) of (x, xa) \<Rightarrow> (case x of (tc, s) \<Rightarrow> \<lambda>(m, e). invs s \<and> ct_running s) xa\<rbrakk> \<Longrightarrow> invs b \<and> valid_list b \<and> valid_sched b \<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 < domain_time b \<and> valid_domain_list b \<and> scheduler_action b = resume_cur_thread
 2. \<forall>j. Step (ADT_A uop) j `` {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} \<subseteq> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} proof (prove)
goal (2 subgoals):
 1. invs init_A_st \<and> ct_running init_A_st \<Longrightarrow> 0 < domain_time init_A_st \<and> scheduler_action init_A_st = resume_cur_thread
 2. \<forall>j. Step (ADT_A uop) j `` {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} \<subseteq> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step (ADT_A uop) j `` {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} \<subseteq> {((tc, s), m, e). einvs s \<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 < domain_time s \<and> valid_domain_list s \<and> scheduler_action s = resume_cur_thread} 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_A e) \<or> ac = UserMode \<and> bc = None \<and> aa = UserMode \<and> ba = None \<and> ((ab, bb), None, a, b) \<in> do_user_op_A 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_A uop) \<or> ac = UserMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_A \<or> ac = IdleMode \<and> bc = None \<and> aa = IdleMode \<and> ba = None \<and> ((ab, bb), False, a, b) \<in> check_active_irq_A \<or> ac = IdleMode \<and> bc = None \<and> aa = KernelMode \<and> ba = Some Interrupt \<and> ((ab, bb), True, a, b) \<in> check_active_irq_A; invs bb; valid_list bb; valid_sched_2 (ready_queues bb) (ekheap bb) resume_cur_thread (cur_domain bb) (kheap bb) (cur_thread bb) (idle_thread bb); 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 < domain_time bb; valid_domain_list bb; scheduler_action bb = resume_cur_thread\<rbrakk> \<Longrightarrow> invs b \<and> valid_list b \<and> valid_sched b \<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 < domain_time b \<and> valid_domain_list b \<and> scheduler_action b = resume_cur_thread proof (prove)
goal (1 subgoal):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>mode = KernelMode \<and> (\<exists>ea. e = Some ea \<and> e' = None \<and> ((tc, s), mode', tc', s') \<in> kernel_call_A ea) \<or> mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop \<or> mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop) \<or> mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A \<or> mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A \<or> mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A; 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; mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (12 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; mode = KernelMode \<and> (\<exists>ea. e = Some ea \<and> e' = None \<and> ((tc, s), mode', tc', s') \<in> kernel_call_A ea); ct_running s\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; mode = KernelMode \<and> (\<exists>ea. e = Some ea \<and> e' = None \<and> ((tc, s), mode', tc', s') \<in> kernel_call_A ea); ct_idle s\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 5. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 6. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 7. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 8. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 9. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 10. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 5. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 6. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 7. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 8. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 9. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 10. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (8 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 5. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 6. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 7. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 8. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (7 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 5. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 6. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 7. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (6 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_running s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 5. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 6. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (5 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = UserMode \<and> e' = None \<and> ((tc, s), None, tc', s') \<in> do_user_op_A uop\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 5. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (4 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> (\<exists>e. e' = Some e \<and> ((tc, s), Some e, tc', s') \<in> do_user_op_A uop)\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 4. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (3 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = UserMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 3. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (2 subgoals):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = IdleMode \<and> e' = None \<and> ((tc, s), False, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread
 2. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal (1 subgoal):
 1. \<And>tc' s' mode' e' tc s mode e. \<lbrakk>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); mode = KernelMode \<longrightarrow> (\<exists>y. e = Some y); mode = UserMode \<longrightarrow> ct_running s; mode = IdleMode \<longrightarrow> ct_idle s; (\<exists>y. e = Some y) \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running s; 0 < domain_time s; valid_domain_list s; scheduler_action s = resume_cur_thread; ct_idle s; mode = IdleMode \<and> e = None \<and> mode' = KernelMode \<and> e' = Some Interrupt \<and> ((tc, s), True, tc', s') \<in> check_active_irq_A\<rbrakk> \<Longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (ct_running s' \<or> ct_idle s') \<and> (mode' = KernelMode \<longrightarrow> (\<exists>y. e' = Some y)) \<and> (mode' = UserMode \<longrightarrow> ct_running s') \<and> (mode' = IdleMode \<longrightarrow> ct_idle s') \<and> ((\<exists>y. e' = Some y) \<and> e' \<noteq> Some Interrupt \<longrightarrow> ct_running s') \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread proof (prove)
goal:
No subgoals!