theory Noninterference

lemma uwr_scheduler_affects_equiv:
  "\<lbrakk> (s,s') \<in> uwr PSched; (s,s') \<in> uwr u; invs_if s; invs_if s' \<rbrakk>
     \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and>
         scheduler_affects_equiv initial_aag (label_for_partition u)
                                 (internal_state_if s) (internal_state_if s')" apply (simp add: uwr_def) apply (case_tac u) apply simp apply (rule sameFor_scheduler_affects_equiv) apply (simp add: invs_if_def Invs_def)+ apply (rule context_conjI) apply (rule sameFor_scheduler_equiv,simp+) apply (rule SilcLabel_affects_scheduler_equiv) apply (rule sameFor_scheduler_equiv,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched s'; uwr2 s u s'; invs_if s; invs_if s'\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag u; invs_if s; invs_if s'\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag u; invs_if s; invs_if s'; u = Partition x1\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if s')
 2. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag u; invs_if s; invs_if s'; u = PSched\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag (Partition x1); invs_if s; invs_if s'; u = Partition x1\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (OrdinaryLabel x1) (internal_state_if s) (internal_state_if s')
 2. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag u; invs_if s; invs_if s'; u = PSched\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if s') proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag (Partition x1); invs_if s; invs_if s'; u = Partition x1\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for initial_aag PSched
 2. \<And>x1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag (Partition x1); invs_if s; invs_if s'; u = Partition x1\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for initial_aag (Partition x1)
 3. \<And>x1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag (Partition x1); invs_if s; invs_if s'; u = Partition x1\<rbrakk> \<Longrightarrow> invs (internal_state_if s)
 4. \<And>x1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag (Partition x1); invs_if s; invs_if s'; u = Partition x1\<rbrakk> \<Longrightarrow> invs (internal_state_if s')
 5. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; (s, s') \<in> same_for initial_aag u; invs_if s; invs_if s'; u = PSched\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s) \<and> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) \<and> domain_sep_inv False s0_internal (internal_state_if s) \<and> pas_refined_if s \<and> guarded_pas_domain_if s \<and> idle_equiv s0_internal (internal_state_if s) \<and> valid_domain_list (internal_state_if s) \<and> valid_vspace_objs_if (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s)) \<and> (domain_time (internal_state_if s) = 0 \<longrightarrow> scheduler_action (internal_state_if s) = choose_new_thread) \<and> (snd s \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s) \<longrightarrow> user_context_of s = idle_context (internal_state_if s)) \<and> (case snd s of InUserMode \<Rightarrow> ct_running (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s)) \<and> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | _ \<Rightarrow> True); invs (internal_state_if s') \<and> valid_list (internal_state_if s') \<and> valid_sched (internal_state_if s') \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s') \<and> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') \<and> domain_sep_inv False s0_internal (internal_state_if s') \<and> pas_refined_if s' \<and> guarded_pas_domain_if s' \<and> idle_equiv s0_internal (internal_state_if s') \<and> valid_domain_list (internal_state_if s') \<and> valid_vspace_objs_if (internal_state_if s') \<and> det_inv (sys_mode_of s') (cur_thread_context_of s') (internal_state_if s') \<and> (snd s' \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s')) \<and> (domain_time (internal_state_if s') = 0 \<longrightarrow> scheduler_action (internal_state_if s') = choose_new_thread) \<and> (snd s' \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s') \<longrightarrow> user_context_of s' = idle_context (internal_state_if s')) \<and> (case snd s' of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True); u = PSched\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv initial_aag SilcLabel (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s) \<and> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) \<and> domain_sep_inv False s0_internal (internal_state_if s) \<and> pas_refined_if s \<and> guarded_pas_domain_if s \<and> idle_equiv s0_internal (internal_state_if s) \<and> valid_domain_list (internal_state_if s) \<and> valid_vspace_objs_if (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s)) \<and> (domain_time (internal_state_if s) = 0 \<longrightarrow> scheduler_action (internal_state_if s) = choose_new_thread) \<and> (snd s \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s) \<longrightarrow> user_context_of s = idle_context (internal_state_if s)) \<and> (case snd s of InUserMode \<Rightarrow> ct_running (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s)) \<and> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | _ \<Rightarrow> True); invs (internal_state_if s') \<and> valid_list (internal_state_if s') \<and> valid_sched (internal_state_if s') \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s') \<and> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') \<and> domain_sep_inv False s0_internal (internal_state_if s') \<and> pas_refined_if s' \<and> guarded_pas_domain_if s' \<and> idle_equiv s0_internal (internal_state_if s') \<and> valid_domain_list (internal_state_if s') \<and> valid_vspace_objs_if (internal_state_if s') \<and> det_inv (sys_mode_of s') (cur_thread_context_of s') (internal_state_if s') \<and> (snd s' \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s')) \<and> (domain_time (internal_state_if s') = 0 \<longrightarrow> scheduler_action (internal_state_if s') = choose_new_thread) \<and> (snd s' \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s') \<longrightarrow> user_context_of s' = idle_context (internal_state_if s')) \<and> (case snd s' of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True); u = PSched\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s')
 2. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s) \<and> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) \<and> domain_sep_inv False s0_internal (internal_state_if s) \<and> pas_refined_if s \<and> guarded_pas_domain_if s \<and> idle_equiv s0_internal (internal_state_if s) \<and> valid_domain_list (internal_state_if s) \<and> valid_vspace_objs_if (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s)) \<and> (domain_time (internal_state_if s) = 0 \<longrightarrow> scheduler_action (internal_state_if s) = choose_new_thread) \<and> (snd s \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s) \<longrightarrow> user_context_of s = idle_context (internal_state_if s)) \<and> (case snd s of InUserMode \<Rightarrow> ct_running (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s)) \<and> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | _ \<Rightarrow> True); invs (internal_state_if s') \<and> valid_list (internal_state_if s') \<and> valid_sched (internal_state_if s') \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s') \<and> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') \<and> domain_sep_inv False s0_internal (internal_state_if s') \<and> pas_refined_if s' \<and> guarded_pas_domain_if s' \<and> idle_equiv s0_internal (internal_state_if s') \<and> valid_domain_list (internal_state_if s') \<and> valid_vspace_objs_if (internal_state_if s') \<and> det_inv (sys_mode_of s') (cur_thread_context_of s') (internal_state_if s') \<and> (snd s' \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s')) \<and> (domain_time (internal_state_if s') = 0 \<longrightarrow> scheduler_action (internal_state_if s') = choose_new_thread) \<and> (snd s' \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s') \<longrightarrow> user_context_of s' = idle_context (internal_state_if s')) \<and> (case snd s' of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True); u = PSched; scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_affects_equiv initial_aag SilcLabel (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s) \<and> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) \<and> domain_sep_inv False s0_internal (internal_state_if s) \<and> pas_refined_if s \<and> guarded_pas_domain_if s \<and> idle_equiv s0_internal (internal_state_if s) \<and> valid_domain_list (internal_state_if s) \<and> valid_vspace_objs_if (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s)) \<and> (domain_time (internal_state_if s) = 0 \<longrightarrow> scheduler_action (internal_state_if s) = choose_new_thread) \<and> (snd s \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s) \<longrightarrow> user_context_of s = idle_context (internal_state_if s)) \<and> (case snd s of InUserMode \<Rightarrow> ct_running (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s)) \<and> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | _ \<Rightarrow> True); invs (internal_state_if s') \<and> valid_list (internal_state_if s') \<and> valid_sched (internal_state_if s') \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s') \<and> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') \<and> domain_sep_inv False s0_internal (internal_state_if s') \<and> pas_refined_if s' \<and> guarded_pas_domain_if s' \<and> idle_equiv s0_internal (internal_state_if s') \<and> valid_domain_list (internal_state_if s') \<and> valid_vspace_objs_if (internal_state_if s') \<and> det_inv (sys_mode_of s') (cur_thread_context_of s') (internal_state_if s') \<and> (snd s' \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s')) \<and> (domain_time (internal_state_if s') = 0 \<longrightarrow> scheduler_action (internal_state_if s') = choose_new_thread) \<and> (snd s' \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s') \<longrightarrow> user_context_of s' = idle_context (internal_state_if s')) \<and> (case snd s' of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True); u = PSched; scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_affects_equiv initial_aag SilcLabel (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> same_for initial_aag PSched; invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s) \<and> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) \<and> domain_sep_inv False s0_internal (internal_state_if s) \<and> pas_refined_if s \<and> guarded_pas_domain_if s \<and> idle_equiv s0_internal (internal_state_if s) \<and> valid_domain_list (internal_state_if s) \<and> valid_vspace_objs_if (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s)) \<and> (domain_time (internal_state_if s) = 0 \<longrightarrow> scheduler_action (internal_state_if s) = choose_new_thread) \<and> (snd s \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s) \<longrightarrow> user_context_of s = idle_context (internal_state_if s)) \<and> (case snd s of InUserMode \<Rightarrow> ct_running (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s)) \<and> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | _ \<Rightarrow> True); invs (internal_state_if s') \<and> valid_list (internal_state_if s') \<and> valid_sched (internal_state_if s') \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s') \<and> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') \<and> domain_sep_inv False s0_internal (internal_state_if s') \<and> pas_refined_if s' \<and> guarded_pas_domain_if s' \<and> idle_equiv s0_internal (internal_state_if s') \<and> valid_domain_list (internal_state_if s') \<and> valid_vspace_objs_if (internal_state_if s') \<and> det_inv (sys_mode_of s') (cur_thread_context_of s') (internal_state_if s') \<and> (snd s' \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s')) \<and> (domain_time (internal_state_if s') = 0 \<longrightarrow> scheduler_action (internal_state_if s') = choose_new_thread) \<and> (snd s' \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s') \<longrightarrow> user_context_of s' = idle_context (internal_state_if s')) \<and> (case snd s' of InUserMode \<Rightarrow> ct_running (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s') \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s')) \<and> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s') \<or> ct_idle (internal_state_if s')) \<and> scheduler_action (internal_state_if s') = resume_cur_thread | _ \<Rightarrow> True); u = PSched; scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if s') proof (prove)
goal:
No subgoals!