theory Scheduler_IF

lemma reads_respects_scheduler_invisible_domain_switch:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_scheduler aag l (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_queues s
                                       \<and> guarded_pas_domain aag s \<and> domain_time s = 0
                                       \<and> scheduler_action s = choose_new_thread
                                       \<and> \<not> reads_scheduler_cur_domain aag l s)
                              schedule" apply (rule equiv_valid_guard_imp) apply (simp add: schedule_def) apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_bind[where W=dc]) apply (rule equiv_valid_dc) apply wp apply wp apply (rule equiv_valid_2_bind_pre[where R'=dc]) apply (rule equiv_valid_2_bind_pre[where R'="(=)"]) apply simp apply (rule_tac P="rvb = choose_new_thread" in  EquivValid.gen_asm_ev2_l) apply simp apply (rule equiv_valid_2_bind_pre) apply (rule equiv_valid_2) apply (rule schedule_choose_new_thread_read_respects_scheduler[OF domains_distinct]) apply (rule_tac P="\<top>" and S="\<top>" and
                                  P'="pas_refined aag and
                                     (\<lambda>s. runnable rva
                                          \<longrightarrow> (pasObjectAbs aag rv \<notin> reads_scheduler aag l))" and
                                  S'="pas_refined aag and
                                     (\<lambda>s. runnable rv'a
                                           \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l)"
                               in equiv_valid_2_unobservable) apply wp apply (rule scheduler_equiv_lift) apply wp+ apply simp apply clarsimp apply wp apply (wp tcb_sched_action_unobservable) apply clarsimp apply (wp scheduler_equiv_lift)+ apply (wp | simp)+ apply (wp tcb_sched_action_unobservable)+ apply simp apply (fastforce+)[2] apply wp+ apply (force+)[2] apply (rule equiv_valid_2) apply (rule ev_gets_const) apply wp+ apply (force+)[2] apply (rule equiv_valid_dc) apply wp apply wp apply (wp gts_wp)+ apply (force+)[2] apply wp apply clarsimp apply (intro impI conjI allI; (rule TrueI refl)?) apply (simp add: guarded_pas_domain_def) apply (subgoal_tac "cur_thread s \<noteq> idle_thread s") apply (force simp: disjoint_iff_not_equal) apply (clarsimp simp: pred_tcb_at_def obj_at_def valid_state_def valid_idle_def invs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s) schedule proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q schedule
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s 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 <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
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. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. equiv_valid_rv_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 <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
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. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. equiv_valid_rv_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) dc ?Q (gets cur_thread)
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q3 rv) (?Q3 rv') (do ct_st <- get_thread_state rv;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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 rv);
schedule_choose_new_thread
od)
od) (do ct_st <- get_thread_state rv';
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv' = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv');
schedule_choose_new_thread
od)
od)
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 4. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> gets cur_thread \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>P. \<lbrace>P\<rbrace> gets cur_thread \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q3 rv) (?Q3 rv') (do ct_st <- get_thread_state rv;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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 rv);
schedule_choose_new_thread
od)
od) (do ct_st <- get_thread_state rv';
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv' = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv');
schedule_choose_new_thread
od)
od)
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 5. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> gets cur_thread \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q3 rv) (?Q3 rv') (do ct_st <- get_thread_state rv;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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 rv);
schedule_choose_new_thread
od)
od) (do ct_st <- get_thread_state rv';
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv' = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv');
schedule_choose_new_thread
od)
od)
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 4. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q3 rv) (?Q3 rv') (do ct_st <- get_thread_state rv;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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 rv);
schedule_choose_new_thread
od)
od) (do ct_st <- get_thread_state rv';
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv' = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv');
schedule_choose_new_thread
od)
od)
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 3. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q18 rv rv' rva) (?Q'18 rv rv' rv'a) (gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od) (\<lambda>candidate. 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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)) (gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable rv'a \<or> rv' = id)
od) (\<lambda>candidate. do y <- when (runnable rv'a) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv'a \<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 rv'a) (tcb_sched_action tcb_sched_enqueue rv');
schedule_choose_new_thread
od))
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 7. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 8. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (13 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>dc rv rv'; dc rva rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q25 rv rv' rva rv'a rvb) (?Q'25 rv rv' rva rv'a rv'b) (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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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) (case rv'b of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable rv'a \<or> rv' = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable rv'a) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv'a \<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 rv'a) (tcb_sched_action tcb_sched_enqueue rv');
schedule_choose_new_thread
od)
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q25 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 9. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 10. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rv' rva rv'a rvb. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q25 rv rv' rva rv'a rvb) (?Q'25 rv rv' rva rv'a 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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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) (case rvb of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable rv'a \<or> rv' = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable rv'a) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv'a \<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 rv'a) (tcb_sched_action tcb_sched_enqueue rv');
schedule_choose_new_thread
od)
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q25 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 9. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 10. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rv' rva rv'a rvb. rvb = choose_new_thread \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q32 rv rv' rva rv'a rvb) (?Q'25 rv rv' rva rv'a 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 <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
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) (case rvb of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable rv'a \<or> rv' = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable rv'a) (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 <- schedule_switch_thread_fastfail rv' it ct_prio target_prio;
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 rv'a \<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 rv'a) (tcb_sched_action tcb_sched_enqueue rv');
schedule_choose_new_thread
od)
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 9. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 10. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rv' rva rv'a. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q32 rv rv' rva rv'a choose_new_thread) (?Q'25 rv rv' rva rv'a choose_new_thread) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od) (do y <- when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv');
schedule_choose_new_thread
od)
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 9. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 10. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
A total of 13 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. ?R'35 rv rv' rva rv'a rvb rv'b \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q35 rv rv' rva rv'a rvb) (?Q'35 rv rv' rva rv'a rv'b) schedule_choose_new_thread schedule_choose_new_thread
 2. \<And>rv rv' rva rv'a. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (?R'35 rv rv' rva rv'a) (?P35 rv rv' rva rv'a) (?P'35 rv rv' rva rv'a) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv)) (when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv'))
 3. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>?Q35 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>?Q'35 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ?P35 rv rv' rva rv'a s \<and> ?S35 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ?P'35 rv rv' rva rv'a s \<and> ?S'35 rv rv' rva rv'a s
 7. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 8. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 9. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 10. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. ?R'35 rv rv' rva rv'a rvb rv'b \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q43 rv rv' rva rv'a) schedule_choose_new_thread
 2. \<And>rv rv' rva rv'a. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (?R'35 rv rv' rva rv'a) (?P35 rv rv' rva rv'a) (?P'35 rv rv' rva rv'a) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv)) (when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv'))
 3. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. ?Q43 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. ?Q43 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ?P35 rv rv' rva rv'a s \<and> ?S35 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ?P'35 rv rv' rva rv'a s \<and> ?S'35 rv rv' rva rv'a s
 7. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 8. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 9. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 10. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>rv rv' rva rv'a. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (?R'35 rv rv' rva rv'a) (?P35 rv rv' rva rv'a) (?P'35 rv rv' rva rv'a) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv)) (when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv'))
 2. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 4. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ?P35 rv rv' rva rv'a s \<and> ?S35 rv rv' rva rv'a s
 5. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ?P'35 rv rv' rva rv'a s \<and> ?S'35 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 7. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 8. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 9. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
A total of 17 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 4. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 6. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 7. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 8. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 9. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
A total of 22 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>rv rv' rva rv'a st. runnable rva \<Longrightarrow> \<lbrace>?Q49 rv rv' rva rv'a st\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>rv rv' rva rv'a st s. ((\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rva then ?Q49 rv rv' rva rv'a st else scheduler_equiv aag st) s
 3. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 5. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 6. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 7. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 8. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 9. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 10. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
A total of 23 subgoals... proof (prove)
goal (28 subgoals):
 1. \<And>rv rv' rva rv'a st sta. runnable rva \<Longrightarrow> \<lbrace>globals_equiv_scheduler sta\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>rv rv' rva rv'a st Q. runnable rva \<Longrightarrow> \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>rv rv' rva rv'a st P. runnable rva \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>rv rv' rva rv'a st Q. runnable rva \<Longrightarrow> \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>rv rv' rva rv'a st P. runnable rva \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>rv rv' rva rv'a st sta. runnable rva \<Longrightarrow> \<lbrace>silc_dom_equiv aag sta\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>rv rv' rva rv'a st s. ((\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rva then scheduler_equiv aag st else scheduler_equiv aag st) s
 8. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 10. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
A total of 28 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rv' rva rv'a st s. ((\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rva then scheduler_equiv aag st else scheduler_equiv aag st) s
 2. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 4. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 6. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 7. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 8. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 9. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
A total of 22 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 3. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 5. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 6. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 7. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 8. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 9. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rva st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 3. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 5. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 6. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 7. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 8. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 9. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
A total of 21 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rva st. runnable rva \<Longrightarrow> \<lbrace>?Q90 rv rva st\<rbrace> tcb_sched_action tcb_sched_enqueue rv \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>rv rva st s. (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rva then ?Q90 rv rva st else scheduler_affects_equiv aag l st) s
 3. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 4. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 6. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 7. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 8. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 9. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
A total of 22 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rva st s. (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rva then pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>s. pasObjectAbs aag rv \<notin> reads_scheduler aag l) else scheduler_affects_equiv aag l st) s
 2. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 3. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 5. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 6. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 7. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 8. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 9. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 10. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
A total of 21 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rv' rva rv'a st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 4. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 5. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 6. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 7. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 8. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 9. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 10. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
A total of 20 subgoals... proof (prove)
goal (26 subgoals):
 1. \<And>rv rv' rva rv'a st sta s. globals_equiv_scheduler sta s \<Longrightarrow> (if runnable rv'a then globals_equiv_scheduler sta else globals_equiv_scheduler sta) s
 2. \<And>rv rv' rva rv'a st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>rv rv' rva rv'a st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>rv rv' rva rv'a st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>rv rv' rva rv'a st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>rv rv' rva rv'a st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>rv rv' rva rv'a st s. ((\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> scheduler_equiv aag st s
 8. \<And>rv rv' rva rv'a st. \<lbrace>pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 10. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
A total of 26 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rv' rva rv'a st. runnable rv'a \<Longrightarrow> \<lbrace>?Q139 rv rv' rva rv'a st\<rbrace> tcb_sched_action tcb_sched_enqueue rv' \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>rv rv' rva rv'a st s. (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rv'a then ?Q139 rv rv' rva rv'a st else scheduler_affects_equiv aag l st) s
 3. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 4. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 5. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 6. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 7. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 8. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 9. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 10. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rv' rva rv'a st s. (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (if runnable rv'a then pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>s. pasObjectAbs aag rv' \<notin> reads_scheduler aag l) else scheduler_affects_equiv aag l st) s
 2. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 3. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 4. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 5. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 6. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 7. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 8. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 9. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 10. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
A total of 19 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rv' rva rv'a. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 2. \<And>rv rv' rva rv'a. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 3. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 5. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 6. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 7. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 8. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 9. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 10. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
A total of 18 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrace>?S35 rv rv' rva rv'a\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvb. invs and pas_refined aag and valid_queues\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrace>?S'35 rv rv' rva rv'a\<rbrace> when (runnable rv'a) (tcb_sched_action tcb_sched_enqueue rv') \<lbrace>\<lambda>rv'b. invs and pas_refined aag and valid_queues\<rbrace>
 3. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) s \<and> ?S35 rv rv' rva rv'a s
 4. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> ?S'35 rv rv' rva rv'a s
 5. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 6. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 7. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 8. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 9. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 10. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
A total of 16 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rv' rva rv'a s. ?Q32 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l))) 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
 2. \<And>rv rv' rva rv'a s. ?Q'25 rv rv' rva rv'a choose_new_thread s \<Longrightarrow> ((\<lambda>_. True) and (pas_refined aag and (\<lambda>s. runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))) s \<and> (if runnable rv'a 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
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 4. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. ?Q32 rv rv' rva rv'a rvb and K (rvb = choose_new_thread)\<rbrace>
 5. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>?Q'25 rv rv' rva rv'a\<rbrace>
 6. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 7. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 9. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 10. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P25 rv rv' rva rv'a) (?P'25 rv rv' rva rv'a) (gets scheduler_action) (gets scheduler_action)
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. (\<lambda>a. pas_refined aag a \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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)) a) and K (rvb = choose_new_thread)\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>a b. pas_refined aag b \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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)) b\<rbrace>
 4. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 5. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P'25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 6. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 9. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 10. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P25 rv rv' rva rv'a) (gets scheduler_action)
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. (\<lambda>a. pas_refined aag a \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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)) a) and K (rvb = choose_new_thread)\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>a b. pas_refined aag b \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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)) b\<rbrace>
 4. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S25 rv rv' rva rv'a s
 5. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> ?P25 rv rv' rva rv'a s \<and> ?S'25 rv rv' rva rv'a s
 6. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 8. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 9. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 10. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb. (\<lambda>a. pas_refined aag a \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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)) a) and K (rvb = choose_new_thread)\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'25 rv rv' rva rv'a\<rbrace> gets scheduler_action \<lbrace>\<lambda>a b. pas_refined aag b \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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)) b\<rbrace>
 3. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> scheduler_action s = ?x199 rv rv' rva rv'a \<and> ?S25 rv rv' rva rv'a s
 4. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> scheduler_action s = ?x199 rv rv' rva rv'a \<and> ?S'25 rv rv' rva rv'a s
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 6. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 7. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 8. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 9. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 10. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q18 rv rv' rva s\<rbrakk> \<Longrightarrow> scheduler_action s = ?x199 rv rv' rva rv'a \<and> ((\<lambda>a. pas_refined aag a \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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)) a) and K (scheduler_action s = choose_new_thread)) s
 2. \<And>rv rv' rva rv'a s. \<lbrakk>dc rv rv'; dc rva rv'a; ?Q'18 rv rv' rv'a s\<rbrakk> \<Longrightarrow> scheduler_action s = ?x199 rv rv' rva rv'a \<and> pas_refined aag s \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>?Q18 rv rv'\<rbrace>
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>?Q'18 rv rv'\<rbrace>
 6. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 7. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 8. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 9. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc (?P18 rv rv') (?P'18 rv rv') (get_thread_state rv) (get_thread_state rv')
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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 \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>\<lambda>rv'a s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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 rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 6. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 7. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' P. dc rv rv' \<Longrightarrow> \<lbrace>P\<rbrace> get_thread_state rv \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>rv rv' P. dc rv rv' \<Longrightarrow> \<lbrace>P\<rbrace> get_thread_state rv' \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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 \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>\<lambda>rv'a s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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>
 5. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 7. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 8. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' P. dc rv rv' \<Longrightarrow> \<lbrace>P\<rbrace> get_thread_state rv' \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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 \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>\<lambda>rv'a s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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 rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 6. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 7. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S18 rv rv'\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rva \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<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 \<and> scheduler_action s = choose_new_thread\<rbrace>
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> \<lbrace>?S'18 rv rv'\<rbrace> get_thread_state rv' \<lbrace>\<lambda>rv'a s. scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable rv'a 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>
 3. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> ?S18 rv rv' s
 4. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> ?S'18 rv rv' s
 5. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 6. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv s\<rbrakk> \<Longrightarrow> ?P18 rv rv' s \<and> (\<forall>st. st_tcb_at ((=) st) rv s \<longrightarrow> scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable st \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<and> (if runnable st 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 \<and> scheduler_action s = choose_new_thread)
 2. \<And>rv rv' s. \<lbrakk>dc rv rv'; ?Q3 rv' s\<rbrakk> \<Longrightarrow> ?P'18 rv rv' s \<and> (\<forall>st. st_tcb_at ((=) st) rv' s \<longrightarrow> scheduler_action s = ?x210 rv rv' \<and> pas_refined aag s \<and> (runnable st \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l) \<and> (if runnable st 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)
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 4. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. (?P'235 rv s \<and> (\<forall>st. st_tcb_at ((=) st) rv s \<longrightarrow> scheduler_action s = ?x236 \<and> pas_refined aag s \<and> (runnable st \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<and> (if runnable st 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)) \<and> (\<forall>st. st_tcb_at ((=) st) rv s \<longrightarrow> scheduler_action s = ?x236 \<and> pas_refined aag s \<and> (runnable st \<longrightarrow> pasObjectAbs aag rv \<notin> reads_scheduler aag l) \<and> (if runnable st 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 \<and> scheduler_action s = choose_new_thread)\<rbrace>
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (True \<and> (\<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> scheduler_action s = ?x236 \<and> pas_refined aag s \<and> (runnable st \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (if runnable st then \<lambda>sa. invs sa \<and> pas_refined aag sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa else (\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s)) s)) \<and> (\<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> scheduler_action s = ?x236 \<and> pas_refined aag s \<and> (runnable st \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (if runnable st then \<lambda>sa. invs sa \<and> pas_refined aag sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa else (\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s)) s \<and> scheduler_action s = choose_new_thread) proof (prove)
goal (1 subgoal):
 1. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; guarded_pas_domain aag s; domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}\<rbrakk> \<Longrightarrow> (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> choose_new_thread = ?x236 \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> st_tcb_at runnable (cur_thread s) s) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> choose_new_thread = ?x236) proof (prove)
goal (2 subgoals):
 1. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; guarded_pas_domain aag s; domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 2. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; guarded_pas_domain aag s; domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 2. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; guarded_pas_domain aag s; domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (3 subgoals):
 1. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 2. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
 3. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; guarded_pas_domain aag s; domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
 2. \<And>s st. \<lbrakk>pas_refined aag s; invs s; valid_queues s; guarded_pas_domain aag s; domain_time s = 0; scheduler_action s = choose_new_thread; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; runnable st; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal:
No subgoals!