theory Scheduler_IF

lemma schedule_reads_respects_scheduler_cur_domain:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_scheduler aag l (invs and pas_refined aag and valid_sched
                                        and guarded_pas_domain aag
                                        and (\<lambda>s. reads_scheduler_cur_domain aag l s)) schedule" supply ethread_get_wp[wp del] apply (simp add: schedule_def schedule_switch_thread_fastfail_def) apply (rule equiv_valid_guard_imp) apply (rule bind_ev)+ apply wpc 
           (* resume current thread *)
            apply wp[1] prefer 2 
          (* choose new thread *)
           apply (rule bind_ev) apply (rule schedule_choose_new_thread_read_respects_scheduler[OF domains_distinct]) apply ((wpsimp wp: when_ev gts_wp get_thread_state_reads_respects_scheduler)+)[2] 
         (* switch thread *)
          apply (rule bind_ev)+ apply (rule if_ev) apply (rule read_respects_scheduler_switch_thread_case[OF domains_distinct]) apply (rule if_ev) apply (rule read_respects_scheduler_switch_thread_case_app[OF domains_distinct]) apply simp apply (rule ev_weaken_pre_relation) apply (rule guarded_switch_to_thread_midstrength_reads_respects_scheduler[OF domains_distinct]) apply fastforce apply (rule gets_highest_prio_ev_from_weak_sae) apply fastforce apply (wpsimp wp: when_ev gts_wp get_thread_state_reads_respects_scheduler
                                        ethread_get_when_reads_respects_scheduler
                                        hoare_vcg_all_lift
                             | wp (once) hoare_vcg_conj_lift hoare_drop_imps)+ 
  (* TODO: cleanup *)
   apply (intro impI conjI allI
         ; (fastforce simp: guarded_pas_domain_def valid_sched_def
                      dest: st_tcb_at_idle_thread switch_to_cur_domain)?
         ; (fastforce simp: guarded_pas_domain_def scheduler_equiv_def st_tcb_at_def obj_at_def
                            switch_to_cur_domain reads_lrefl)?
         ; (fastforce simp: guarded_pas_domain_def scheduler_equiv_def st_tcb_at_def obj_at_def
                            switch_to_cur_domain valid_sched_def reads_scheduler_def
                     split: if_splits
                      dest: domains_distinct[THEN pas_domains_distinct_inj])?) 
   (* Last remaining goal is more fiddly (duplicated modulo "runnable st")
      We are switching to a new thread but still in the current domain.
      By the domains_distinct condition, we must remain in the current label as well
    *)
    apply (thin_tac "runnable st" for st) prefer 2 apply (thin_tac "\<not>runnable st" for st) apply distinct_subgoals apply (clarsimp simp: guarded_pas_domain_def pas_refined_def reads_scheduler_def
                      tcb_domain_map_wellformed_aux_def
                      valid_sched_def valid_sched_action_def weak_valid_sched_action_def
                      switch_in_cur_domain_def in_cur_domain_def
               split: if_splits) apply (frule st_tcb_at_tcb_at, drule (1) tcb_at_is_etcb_at, drule (1) etcb_in_domains_of_state) apply (drule (1) bspec) apply simp by (metis Int_emptyI assms pas_domains_distinct_inj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) schedule proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) schedule proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) (do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q (do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od)
 2. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q11 rv rva rvb) (case rvb of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 2. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 3. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>?Q11 rv rva\<rbrace>
 4. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 5. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 6. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 7. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 8. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb. rvb = resume_cur_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R23 rv rva rvb) (do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 3. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R20 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 4. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 5. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> ?R23 rv rva rvb s) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R20 rv rva rvb s)\<rbrace>
 6. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 7. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 8. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 9. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 10. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb. rvb = resume_cur_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R23 rv rva rvb) (do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 3. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R20 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 4. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 5. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> ?R23 rv rva rvb s) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R20 rv rva rvb s)\<rbrace>
 6. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 7. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 8. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 9. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 10. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R20 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 3. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 4. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R20 rv rva rvb s)\<rbrace>
 5. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 6. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 7. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 8. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 9. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R20 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 3. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 4. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R20 rv rva rvb s)\<rbrace>
 5. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 6. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 7. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 8. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 9. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R20 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 3. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 4. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R20 rv rva rvb s)\<rbrace>
 5. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 6. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 7. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 8. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 9. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (11 subgoals):
 1. \<And>rv rva rvb rvc. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q33 rv rva rvb rvc) schedule_choose_new_thread
 2. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'33 rv rva rvb) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv))
 3. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> \<lbrace>?P''33 rv rva rvb\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>?Q33 rv rva rvb\<rbrace>
 4. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 5. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 6. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?P'33 rv rva rvb s \<and> ?P''33 rv rva rvb s)\<rbrace>
 7. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 8. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 9. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 10. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'33 rv rva rvb) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv))
 2. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> \<lbrace>?P''33 rv rva rvb\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvc. invs and pas_refined aag and valid_queues\<rbrace>
 3. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 4. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 5. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?P'33 rv rva rvb s \<and> ?P''33 rv rva rvb s)\<rbrace>
 6. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 7. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 8. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 9. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 10. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 3. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> (runnable rva \<longrightarrow> pas_refined aag s) \<and> (if runnable rva then \<lambda>s. invs s \<and> pas_refined aag s \<and> (valid_queues and st_tcb_at runnable rv) s else (\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s)) s)\<rbrace>
 4. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 5. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 6. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 7. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 8. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?R22 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- if rv \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'11 rv rva) (gets scheduler_action)
 3. \<And>rv rva. \<lbrace>?P''11 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R22 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> (runnable rva \<longrightarrow> pas_refined aag s) \<and> (if runnable rva then \<lambda>s. invs s \<and> pas_refined aag s \<and> (valid_queues and st_tcb_at runnable rv) s else (\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s)) s)\<rbrace>
 4. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (get_thread_state rv)
 5. \<And>rv. \<lbrace>?P''7 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'11 rv rva s \<and> ?P''11 rv rva s\<rbrace>
 6. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (gets cur_thread)
 7. \<lbrace>?P''3\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 8. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (22 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q80 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (if rvg \<and> \<not> rvi then do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<and> rvf = rve then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>?Q80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
A total of 22 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; rvg \<and> \<not> rvi\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P84 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (do tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi)\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q84 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (if runnable rva \<and> rvf = rve then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> ?P84 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> ?Q84 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s)\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 8. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 10. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
A total of 23 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi)\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q84 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (if runnable rva \<and> rvf = rve then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> ?Q84 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s)\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
A total of 22 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi); runnable rva \<and> rvf = rve\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi); \<not> (runnable rva \<and> rvf = rve)\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> ?P88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> ?Q88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s))\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 8. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 10. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
A total of 23 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi); \<not> (runnable rva \<and> rvf = rve)\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> ?Q88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s))\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
A total of 22 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rva rvb x2 rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; rvg \<longrightarrow> rvi; runnable rva \<longrightarrow> rvf \<noteq> rve\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q88 rv rva (switch_thread x2) x2 () rvd rve rvf rvg rvh rvi) (do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> ?Q88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s))\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
A total of 22 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>rv rva rvb x2 rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; rvg \<longrightarrow> rvi; runnable rva \<longrightarrow> rvf \<noteq> rve\<rbrakk> \<Longrightarrow> equiv_valid (scheduler_equiv aag) (?A92 rv rva rvb x2 rvd rve rvf rvg rvh rvi) (scheduler_affects_equiv aag l) (?Q88 rv rva (switch_thread x2) x2 () rvd rve rvf rvg rvh rvi) (do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb x2 rvd rve rvf rvg rvh rvi s t. \<lbrakk>rvb = switch_thread x2; rvg \<longrightarrow> rvi; runnable rva \<longrightarrow> rvf \<noteq> rve; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> ?A92 rv rva rvb x2 rvd rve rvf rvg rvh rvi s t
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> ?Q88 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s))\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 8. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 10. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
A total of 23 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rva rvb x2 rvd rve rvf rvg rvh rvi s t. \<lbrakk>rvb = switch_thread x2; rvg \<longrightarrow> rvi; runnable rva \<longrightarrow> rvf \<noteq> rve; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s t
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag x2 \<in> pasDomainAbs aag (cur_domain s))) s))\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
A total of 22 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag x2 \<in> pasDomainAbs aag (cur_domain s))) s))\<rbrace>
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''64 rv rva rvb x2 rvc rvd\<rbrace> ethread_get tcb_priority x2 \<lbrace>\<lambda>rve s. ?P'68 rv rva rvb x2 rvc rvd rve s \<and> ?P''68 rv rva rvb x2 rvc rvd rve s\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<forall>s t. scheduler_affects_equiv aag l s t \<longrightarrow> weak_scheduler_affects_equiv (?aag107 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (?l107 rv rva rvb x2 rvc rvd rve rvf rvg rvh) s t
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag x2 \<in> pasDomainAbs aag (cur_domain s))) s))\<rbrace>
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. pasDomainAbs (?aag107 rv rva rvb x2 rvc rvd rve rvf rvg rvh) rvh \<inter> reads_scheduler (?aag107 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (?l107 rv rva rvb x2 rvc rvd rve rvf rvg rvh) \<noteq> {} \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 8. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
 10. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''64 rv rva rvb x2 rvc rvd\<rbrace> ethread_get tcb_priority x2 \<lbrace>\<lambda>rve s. ?P'68 rv rva rvb x2 rvc rvd rve s \<and> ?P''68 rv rva rvb x2 rvc rvd rve s\<rbrace>
A total of 21 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread x2) and valid_sched_action and pas_refined aag) s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag x2 \<in> pasDomainAbs aag (cur_domain s))) s))\<rbrace>
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'76 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''76 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. pasDomainAbs aag rvh \<inter> reads_scheduler aag l \<noteq> {} \<and> ?P''80 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'72 rv rva rvb x2 rvc rvd rve rvf) (if rv \<noteq> rvd then return (rve < rvf) else return True)
 5. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''72 rv rva rvb x2 rvc rvd rve rvf\<rbrace> if rv \<noteq> rvd then return (rve < rvf) else return True \<lbrace>\<lambda>rvg s. ?P'76 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''76 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 6. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'68 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 7. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''68 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'72 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''72 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 8. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'64 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
 9. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''64 rv rva rvb x2 rvc rvd\<rbrace> ethread_get tcb_priority x2 \<lbrace>\<lambda>rve s. ?P'68 rv rva rvb x2 rvc rvd rve s \<and> ?P''68 rv rva rvb x2 rvc rvd rve s\<rbrace>
 10. \<And>rv rva rvb x2 rvc. rvb = switch_thread x2 \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'60 rv rva rvb x2 rvc) (gets idle_thread)
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>_. True) (cur_thread s) s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l \<or> cur_thread s = idle_thread s) \<and> valid_idle s \<and> (\<forall>st. (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>x xa. scheduler_equiv aag x xa \<and> scheduler_affects_equiv aag l x xa \<longrightarrow> idle_thread x = idle_thread xa) \<and> pasObjectAbs aag x \<in> reads_scheduler aag l \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s)) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>x xa. scheduler_equiv aag x xa \<and> scheduler_affects_equiv aag l x xa \<longrightarrow> idle_thread x = idle_thread xa) \<and> pasObjectAbs aag x \<in> reads_scheduler aag l \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_queues s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>_. True) (cur_thread s) s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l \<or> cur_thread s = idle_thread s) \<and> valid_idle s \<and> (\<forall>st. (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>x xa. scheduler_equiv aag x xa \<and> scheduler_affects_equiv aag l x xa \<longrightarrow> idle_thread x = idle_thread xa) \<and> pasObjectAbs aag x \<in> reads_scheduler aag l \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s)) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>x xa. scheduler_equiv aag x xa \<and> scheduler_affects_equiv aag l x xa \<longrightarrow> idle_thread x = idle_thread xa) \<and> pasObjectAbs aag x \<in> reads_scheduler aag l \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_queues s \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_queues s))) proof (prove)
goal (2 subgoals):
 1. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l
 2. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l proof (prove)
goal (2 subgoals):
 1. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l
 2. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l proof (prove)
goal (2 subgoals):
 1. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l
 2. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l proof (prove)
goal (2 subgoals):
 1. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l
 2. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l proof (prove)
goal (2 subgoals):
 1. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l
 2. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s st x. \<lbrakk>invs s; pas_refined aag s; valid_sched s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s st x. \<lbrakk>st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x; invs s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); l \<noteq> SilcLabel; pas_wellformed aag; valid_etcbs s; irq_map_wellformed aag s; valid_queues s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); state_objs_in_policy aag s; st_tcb_at runnable x s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) l \<noteq> {}\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l proof (prove)
goal (1 subgoal):
 1. \<And>s st x. \<lbrakk>st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x; invs s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); l \<noteq> SilcLabel; pas_wellformed aag; valid_etcbs s; irq_map_wellformed aag s; valid_queues s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); state_objs_in_policy aag s; st_tcb_at runnable x s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) l \<noteq> {}; (x, cur_domain s) \<in> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l proof (prove)
goal (1 subgoal):
 1. \<And>s st x. \<lbrakk>st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x; invs s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); l \<noteq> SilcLabel; pas_wellformed aag; valid_etcbs s; irq_map_wellformed aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); state_objs_in_policy aag s; st_tcb_at runnable x s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) l \<noteq> {}; (x, cur_domain s) \<in> domains_of_state s; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l proof (prove)
goal (1 subgoal):
 1. \<And>s st x. \<lbrakk>st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x; invs s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); l \<noteq> SilcLabel; pas_wellformed aag; valid_etcbs s; irq_map_wellformed aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); state_objs_in_policy aag s; st_tcb_at runnable x s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) l \<noteq> {}; (x, cur_domain s) \<in> domains_of_state s; pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l