theory Schedule_DR

lemma schedule_switch_thread_dcorres:
      "dcorres dc \<top>
        (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s
             \<and> invs s \<and> scheduler_action s = switch_thread target)
        Schedule_D.schedule
        (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
            it <- gets idle_thread;
            target_prio <- ethread_get tcb_priority target;
            ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
            fastfail <- schedule_switch_thread_fastfail cur 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 y <- tcb_sched_action tcb_sched_enqueue target;
                                            y <- set_scheduler_action choose_new_thread;
                                            schedule_choose_new_thread
                                         od
            else if runnable cur_ts \<and> ct_prio = target_prio
                 then do y <- tcb_sched_action tcb_sched_append target;
                         y <- set_scheduler_action choose_new_thread;
                         schedule_choose_new_thread
                      od
                 else do y <- guarded_switch_to target;
                         set_scheduler_action resume_cur_thread
                      od
         od)" (is "dcorres _ _ (\<lambda>s. ?PRE s) _ _") supply ethread_get_wp[wp del] apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_If_both) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply simp apply (rule schedule_choose_new_thread_dcorres) apply (wp set_scheduler_action_transform tcb_sched_action_transform)+ apply (rule dcorres_If_both) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply simp apply (rule schedule_choose_new_thread_dcorres) apply (wp set_scheduler_action_transform tcb_sched_action_transform)+ apply (simp add: Schedule_D.schedule_def guarded_switch_to_def bind_assoc) apply (rule corres_alternate1) apply (rule_tac P=\<top> and P'="?PRE" in stronger_corres_guard_imp) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_rhs_noop_below_True[OF set_scheduler_action_dcorres]) apply (rule corres_symb_exec_l_Ex) apply (rule corres_symb_exec_l_Ex) apply (rule corres_symb_exec_l_Ex) apply (rule corres_symb_exec_l_Ex) apply (rule switch_to_thread_same_corres) apply (wpsimp wp: gts_wp hoare_drop_imp)+ apply (frule schedule_switch_thread_helper, simp,simp,simp) apply (fastforce simp: select_def gets_def get_def bind_def return_def
                                        active_tcbs_in_domain_def invs_def valid_state_def
                                        valid_objs_def change_current_domain_def
                                        Schedule_D.switch_to_thread_def modify_def put_def
                                        option_map_def restrict_map_def map_add_def get_tcb_def
                                        transform_def transform_current_thread_def cur_tcb_def
                                        tcb_at_def) apply (clarsimp) apply (frule invs_valid_idle) apply (fastforce simp: pred_tcb_at_def obj_at_def valid_idle_def valid_sched_def
                                       valid_sched_action_def weak_valid_sched_action_def) apply (wp tcb_sched_action_transform
                         hoare_drop_imp[where f="ethread_get tcb_priority x" for x]
                         hoare_drop_imp[where f="ethread_get_when b tcb_priority t" for b t]
                         hoare_drop_imp[where f="gets cur_domain"]
                      | clarsimp simp add: schedule_switch_thread_fastfail_def
                                 split del: if_split
                      | split if_split)+ apply (fastforce elim: st_tcb_weakenE
                    simp: valid_sched_def valid_blocked_def valid_blocked_except_def
                          not_cur_thread_def valid_sched_action_def weak_valid_sched_action_def) apply (wp tcb_sched_action_transform, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target) Schedule_D.schedule (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority target;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur 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 y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target) Schedule_D.schedule (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority target;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur 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 y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q' rv) Schedule_D.schedule (do it <- gets idle_thread;
target_prio <- ethread_get tcb_priority target;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur 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 y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od)
 2. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rva. dcorres dc (\<lambda>_. True) (?Q'4 rv rva) Schedule_D.schedule (do target_prio <- ethread_get tcb_priority target;
ct_prio <- ethread_get_when (cur \<noteq> rva) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur rva 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 y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv. \<lbrace>?Q' rv\<rbrace> gets idle_thread \<lbrace>?Q'4 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rva rvb. dcorres dc (\<lambda>_. True) (?Q'8 rv rva rvb) Schedule_D.schedule (do ct_prio <- ethread_get_when (cur \<noteq> rva) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur rva ct_prio rvb;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom rvb);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
 3. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv. \<lbrace>?Q' rv\<rbrace> gets idle_thread \<lbrace>?Q'4 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q'\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb rvc. dcorres dc (\<lambda>_. True) (?Q'12 rv rva rvb rvc) Schedule_D.schedule (do fastfail <- schedule_switch_thread_fastfail cur rva rvc rvb;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom rvb);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 3. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
 5. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv. \<lbrace>?Q' rv\<rbrace> gets idle_thread \<lbrace>?Q'4 rv\<rbrace>
 7. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q'\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>rv rva rvb rvc rvd. dcorres dc (\<lambda>_. True) (?Q'16 rv rva rvb rvc rvd) Schedule_D.schedule (do cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom rvb);
if rvd \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 3. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 5. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
 7. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv. \<lbrace>?Q' rv\<rbrace> gets idle_thread \<lbrace>?Q'4 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q'\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rva rvb rvc rvd rve. dcorres dc (\<lambda>_. True) (?Q'20 rv rva rvb rvc rvd rve) Schedule_D.schedule (do highest <- gets (is_highest_prio rve rvb);
if rvd \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 3. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 5. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 7. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
 9. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv. \<lbrace>?Q' rv\<rbrace> gets idle_thread \<lbrace>?Q'4 rv\<rbrace>
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'24 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if rvd \<and> \<not> rvf then do y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>?Q'24 rv rva rvb rvc rvd rve\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?P'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- tcb_sched_action tcb_sched_enqueue target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then ?P'28 rv rva rvb rvc rvd rve r s else ?Q'28 rv rva rvb rvc rvd rve r s\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 6. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 8. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 10. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 16 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf rvg. dcorres dc (\<lambda>_. True) (?Q'31 rv rva rvb rvc rvd rve rvf rvg) Schedule_D.schedule (do y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'28 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 5. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then ?P'28 rv rva rvb rvc rvd rve r s else ?Q'28 rv rva rvb rvc rvd rve r s\<rbrace>
 6. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 8. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 10. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 18 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf rvg rvh. dcorres dc (\<lambda>_. True) (?Q'35 rv rva rvb rvc rvd rve rvf rvg rvh) Schedule_D.schedule schedule_choose_new_thread
 2. \<And>rv rva rvb rvc rvd rve rvf rvg. \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf rvg\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?Q'35 rv rva rvb rvc rvd rve rvf rvg\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf rvg cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'28 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 7. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then ?P'28 rv rva rvb rvc rvd rve r s else ?Q'28 rv rva rvb rvc rvd rve r s\<rbrace>
 8. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 10. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'35 () rva rvb rvc rvd rve rvf () ()) Schedule_D.schedule schedule_choose_new_thread
 2. \<And>rv rva rvb rvc rvd rve rvf rvg. \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf rvg\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?Q'35 rv rva rvb rvc rvd rve rvf rvg\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf rvg cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'28 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 7. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then ?P'28 rv rva rvb rvc rvd rve r s else ?Q'28 rv rva rvb rvc rvd rve r s\<rbrace>
 8. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 10. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf rvg. \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf rvg\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r a. valid_etcbs a \<and> valid_sched_except_blocked a \<and> invs a \<and> scheduler_action a = choose_new_thread\<rbrace>
 2. \<And>rv rva rvb rvc rvd rve rvf rvg cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'28 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>?Q'31 rv rva rvb rvc rvd rve rvf\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 6. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then ?P'28 rv rva rvb rvc rvd rve r s else ?Q'28 rv rva rvb rvc rvd rve r s\<rbrace>
 7. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 9. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
A total of 19 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'28 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (if runnable cur_ts \<and> rvc = rvb then do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else ?Q'28 rv rva rvb rvc rvd rve r s\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?P'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- tcb_sched_action tcb_sched_append target;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then ?P'87 rv rva rvb rvc rvd rve r s else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 6. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 8. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 10. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 16 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf rvg. dcorres dc (\<lambda>_. True) (?Q'90 rv rva rvb rvc rvd rve rvf rvg) Schedule_D.schedule (do y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'87 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 5. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then ?P'87 rv rva rvb rvc rvd rve r s else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 6. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 8. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 10. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 18 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf rvg rvh. dcorres dc (\<lambda>_. True) (?Q'94 rv rva rvb rvc rvd rve rvf rvg rvh) Schedule_D.schedule schedule_choose_new_thread
 2. \<And>rv rva rvb rvc rvd rve rvf rvg. \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf rvg\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?Q'94 rv rva rvb rvc rvd rve rvf rvg\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf rvg cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'87 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 7. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then ?P'87 rv rva rvb rvc rvd rve r s else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 8. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 10. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'94 () rva rvb rvc rvd rve rvf () ()) Schedule_D.schedule schedule_choose_new_thread
 2. \<And>rv rva rvb rvc rvd rve rvf rvg. \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf rvg\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?Q'94 rv rva rvb rvc rvd rve rvf rvg\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf rvg cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'87 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 7. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then ?P'87 rv rva rvb rvc rvd rve r s else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 8. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 10. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf rvg. \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf rvg\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r a. valid_etcbs a \<and> valid_sched_except_blocked a \<and> invs a \<and> scheduler_action a = choose_new_thread\<rbrace>
 2. \<And>rv rva rvb rvc rvd rve rvf rvg cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve rvf. \<lbrace>?P'87 rv rva rvb rvc rvd rve rvf\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>?Q'90 rv rva rvb rvc rvd rve rvf\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action tcb_sched_append target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 6. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then ?P'87 rv rva rvb rvc rvd rve r s else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 7. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 9. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
A total of 19 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 rv rva rvb rvc rvd rve rvf) Schedule_D.schedule (do y <- guarded_switch_to target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 () rva rvb rvc rvd rve rvf) (do y <- change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od \<sqinter> do y <- change_current_domain;
Schedule_D.switch_to_thread None
od) (do x <- get_thread_state target;
x <- assert (runnable x);
y <- Schedule_A.switch_to_thread target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf. dcorres dc (\<lambda>_. True) (?Q'87 () rva rvb rvc rvd rve rvf) (do y <- change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (do x <- get_thread_state target;
x <- assert (runnable x);
y <- Schedule_A.switch_to_thread target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else ?Q'87 rv rva rvb rvc rvd rve r s\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf. dcorres dc (?Q148 rva rvb rvc rvd rve rvf) (?Q'148 rva rvb rvc rvd rve rvf) (do y <- change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (do x <- get_thread_state target;
x <- assert (runnable x);
y <- Schedule_A.switch_to_thread target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q148 rva rvb rvc rvd rve rvf s
 3. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 4. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 5. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 7. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 9. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
A total of 17 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv. dcorres dc (?Q148 rva rvb rvc rvd rve rvf) (?Q'150 rva rvb rvc rvd rve rvf rv) (do y <- change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (do x <- assert (runnable rv);
y <- Schedule_A.switch_to_thread target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q148 rva rvb rvc rvd rve rvf s
 5. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 6. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 7. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 9. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
A total of 19 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv rvg. dcorres dc (?Q148 rva rvb rvc rvd rve rvf) (?Q'154 rva rvb rvc rvd rve rvf rv rvg) (do y <- change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (do y <- Schedule_A.switch_to_thread target;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>?Q'154 rva rvb rvc rvd rve rvf rv\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q148 rva rvb rvc rvd rve rvf s
 7. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 8. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 9. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv rvg. dcorres dc (?Q148 rva rvb rvc rvd rve rvf) (?Q'154 rva rvb rvc rvd rve rvf rv rvg) (do y <- change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (Schedule_A.switch_to_thread target)
 2. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>?Q'154 rva rvb rvc rvd rve rvf rv\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q148 rva rvb rvc rvd rve rvf s
 7. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 8. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 9. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv rvg rvh. dcorres dc (?Q162 rva rvb rvc rvd rve rvf rvh) (?Q'154 rva rvb rvc rvd rve rvf rv rvg) (do next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (Schedule_A.switch_to_thread target)
 2. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>?Q'154 rva rvb rvc rvd rve rvf rv\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. ?Q162 rva rvb rvc rvd rve rvf rv s \<and> (rv, s) \<in> fst (change_current_domain s)
 7. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 8. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 9. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv rvg rvh rvi. dcorres dc (?Q166 rva rvb rvc rvd rve rvf rvh rvi) (?Q'154 rva rvb rvc rvd rve rvf rv rvg) (do threads <- gets (active_tcbs_in_domain rvi);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (Schedule_A.switch_to_thread target)
 2. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>?Q'154 rva rvb rvc rvd rve rvf rv\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rvg. ?Q166 rva rvb rvc rvd rve rvf rv rvg s \<and> (rvg, s) \<in> fst (gets cdl_current_domain s)) \<and> (rv, s) \<in> fst (change_current_domain s)
 7. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 8. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 9. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv rvg rvh rvi rvj. dcorres dc (?Q170 rva rvb rvc rvd rve rvf rvh rvi rvj) (?Q'154 rva rvb rvc rvd rve rvf rv rvg) (do next_thread <- select rvj;
Schedule_D.switch_to_thread (Some next_thread)
od) (Schedule_A.switch_to_thread target)
 2. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>?Q'154 rva rvb rvc rvd rve rvf rv\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rvg. (\<exists>rvh. ?Q170 rva rvb rvc rvd rve rvf rv rvg rvh s \<and> (rvh, s) \<in> fst (gets (active_tcbs_in_domain rvg) s)) \<and> (rvg, s) \<in> fst (gets cdl_current_domain s)) \<and> (rv, s) \<in> fst (change_current_domain s)
 7. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 8. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 9. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv rvg rvh rvi rvj rvk. dcorres dc (?Q174 rva rvb rvc rvd rve rvf rvh rvi rvj rvk) (?Q'154 rva rvb rvc rvd rve rvf rv rvg) (Schedule_D.switch_to_thread (Some rvk)) (Schedule_A.switch_to_thread target)
 2. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>?Q'154 rva rvb rvc rvd rve rvf rv\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rvg. (\<exists>rvh. (\<exists>rvi. ?Q174 rva rvb rvc rvd rve rvf rv rvg rvh rvi s \<and> (rvi, s) \<in> fst (select rvh s)) \<and> (rvh, s) \<in> fst (gets (active_tcbs_in_domain rvg) s)) \<and> (rvg, s) \<in> fst (gets cdl_current_domain s)) \<and> (rv, s) \<in> fst (change_current_domain s)
 7. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 8. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 9. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
A total of 21 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf rv. \<lbrace>?Q'150 rva rvb rvc rvd rve rvf rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r. invs and (\<lambda>s. idle_thread s \<noteq> target) and valid_etcbs\<rbrace>
 2. \<And>rva rvb rvc rvd rve rvf rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rva rvb rvc rvd rve rvf. \<lbrace>?Q'148 rva rvb rvc rvd rve rvf\<rbrace> get_thread_state target \<lbrace>?Q'150 rva rvb rvc rvd rve rvf\<rbrace>
 4. \<And>rva rvb rvc rvd rve rvf cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rv. (\<exists>rva. (\<exists>rv. target = rv \<and> (rv, s) \<in> fst (select rva s)) \<and> (rva, s) \<in> fst (gets (active_tcbs_in_domain rv) s)) \<and> (rv, s) \<in> fst (gets cdl_current_domain s)) \<and> (rv, s) \<in> fst (change_current_domain s)
 6. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'148 rva rvb rvc rvd rve rvf s'
 7. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 8. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 10. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 20 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>s'. \<lbrakk>cur = cur_thread s'; st_tcb_at ((=) cur_ts) (cur_thread s') s'; valid_etcbs s'; valid_sched_2 (ready_queues s') (ekheap s') (switch_thread target) (cur_domain s') (kheap s') (cur_thread s') (idle_thread s'); invs s'; scheduler_action s' = switch_thread target\<rbrakk> \<Longrightarrow> (\<exists>rv. (\<exists>rva. (target, transform s') \<in> fst (select rva (transform s')) \<and> (rva, transform s') \<in> fst (gets (active_tcbs_in_domain rv) (transform s'))) \<and> (rv, transform s') \<in> fst (gets cdl_current_domain (transform s'))) \<and> ((), transform s') \<in> fst (change_current_domain (transform s'))
 2. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) target s' \<longrightarrow> runnable st \<longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> target) and valid_etcbs) s'
 3. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 6. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 8. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 10. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>s'. \<lbrakk>cur = cur_thread s'; st_tcb_at ((=) cur_ts) (cur_thread s') s'; valid_etcbs s'; valid_sched_2 (ready_queues s') (ekheap s') (switch_thread target) (cur_domain s') (kheap s') (cur_thread s') (idle_thread s'); invs s'; scheduler_action s' = switch_thread target; target \<in> active_tcbs_in_domain (cur_domain s') (transform s')\<rbrakk> \<Longrightarrow> (\<exists>rv. (\<exists>rva. (target, transform s') \<in> fst (select rva (transform s')) \<and> (rva, transform s') \<in> fst (gets (active_tcbs_in_domain rv) (transform s'))) \<and> (rv, transform s') \<in> fst (gets cdl_current_domain (transform s'))) \<and> ((), transform s') \<in> fst (change_current_domain (transform s'))
 2. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) target s' \<longrightarrow> runnable st \<longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> target) and valid_etcbs) s'
 3. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 4. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 6. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 8. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 10. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rva rvb rvc rvd rve rvf s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = switch_thread target; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) target s' \<longrightarrow> runnable st \<longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> target) and valid_etcbs) s'
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>s' st. \<lbrakk>cur = cur_thread s'; st_tcb_at ((=) cur_ts) (cur_thread s') s'; valid_etcbs s'; valid_sched_2 (ready_queues s') (ekheap s') (switch_thread (idle_thread s')) (cur_domain s') (kheap s') (cur_thread s') (idle_thread s'); invs s'; scheduler_action s' = switch_thread (idle_thread s'); st_tcb_at ((=) st) (idle_thread s') s'; runnable st; target = idle_thread s'\<rbrakk> \<Longrightarrow> False
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>s' st. \<lbrakk>cur = cur_thread s'; st_tcb_at ((=) cur_ts) (cur_thread s') s'; valid_etcbs s'; valid_sched_2 (ready_queues s') (ekheap s') (switch_thread (idle_thread s')) (cur_domain s') (kheap s') (cur_thread s') (idle_thread s'); invs s'; scheduler_action s' = switch_thread (idle_thread s'); st_tcb_at ((=) st) (idle_thread s') s'; runnable st; target = idle_thread s'; valid_idle s'\<rbrakk> \<Longrightarrow> False
 2. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 3. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 5. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 7. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 9. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rva rvb rvc rvd rve. \<lbrace>?Q'20 rv rva rvb rvc rvd rve\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. if rvd \<and> \<not> r then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else if runnable cur_ts \<and> rvc = rvb then valid_etcbs s \<and> valid_etcbs s \<and> (valid_queues and st_tcb_at runnable target) s \<and> True \<and> True \<and> True \<and> valid_idle_etcb s \<and> invs s \<and> True else cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = switch_thread target\<rbrace>
 2. \<And>rv rva rvb rvc rvd rve cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (is_highest_prio rve rvb) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv rva rvb rvc rvd. \<lbrace>?Q'16 rv rva rvb rvc rvd\<rbrace> gets cur_domain \<lbrace>?Q'20 rv rva rvb rvc rvd\<rbrace>
 4. \<And>rv rva rvb rvc rvd cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rva rvb rvc. \<lbrace>?Q'12 rv rva rvb rvc\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>?Q'16 rv rva rvb rvc\<rbrace>
 6. \<And>rv rva rvb rvc cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> schedule_switch_thread_fastfail cur rva rvc rvb \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rva rvb. \<lbrace>?Q'8 rv rva rvb\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>?Q'12 rv rva rvb\<rbrace>
 8. \<And>rv rva rvb cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get_when (cur \<noteq> rva) tcb_priority cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> ethread_get tcb_priority target \<lbrace>?Q'8 rv rva\<rbrace>
 10. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority target \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 14 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cur = cur_thread s; st_tcb_at ((=) cur_ts) (cur_thread s) s; valid_etcbs s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread target) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); invs s; scheduler_action s = switch_thread target\<rbrakk> \<Longrightarrow> (runnable cur_ts \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable target s \<and> valid_idle_etcb s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable target s \<and> valid_idle_etcb s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread target) (cur_thread s) \<and> valid_sched_action_2 (switch_thread target) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable (cur_thread s) s \<and> not_cur_thread_2 (cur_thread s) (switch_thread target) (cur_thread s) \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) (switch_thread target) (cur_thread s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable target s \<and> valid_idle_etcb s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable target s \<and> valid_idle_etcb s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread target) (cur_thread s) \<and> valid_sched_action_2 (switch_thread target) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable (cur_thread s) s \<and> not_cur_thread_2 (cur_thread s) (switch_thread target) (cur_thread s) \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) (switch_thread target) (cur_thread s)) \<and> (\<not> runnable cur_ts \<longrightarrow> valid_queues s \<and> st_tcb_at runnable target s \<and> valid_idle_etcb s)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!