theory Schedule_DR

lemma schedule_choose_new_thread_dcorres:
  "dcorres dc \<top>
        (\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread)
        Schedule_D.schedule
        schedule_choose_new_thread" unfolding schedule_choose_new_thread_def guarded_switch_to_def bind_assoc
            choose_thread_def max_non_empty_queue_def supply if_cong[cong] apply (rule dcorres_symb_exec_r, rename_tac dom_t) apply (case_tac "dom_t \<noteq> 0") apply (clarsimp) apply (rule dcorres_symb_exec_r, rename_tac cur_dom) apply (rule dcorres_symb_exec_r, rename_tac rq) apply (rule dcorres_rhs_noop_below_True[OF set_scheduler_action_dcorres]) 
         (* No threads in ready_queues *)
          apply (rule corres_guard_imp) apply (rule corres_if_rhs) apply (clarsimp simp: Schedule_D.schedule_def) apply (rule corres_alternate2) apply (rule change_current_domain_and_switch_to_idle_thread_dcorres) 
           (* Threads in ready_queues *)
            apply (simp only: Schedule_D.schedule_def) apply (rule corres_alternate1) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule_tac P'="\<lambda>s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread"
                               in stronger_corres_guard_imp) apply (rule corres_symb_exec_l_Ex) apply (clarsimp) 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 clarsimp apply (frule_tac prio="(Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})" in schedule_choose_new_thread_helper,simp,simp,simp,simp,simp) apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) apply (auto 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)[1] apply (clarsimp simp: invs_def valid_state_def valid_sched_def max_non_empty_queue_def) apply (frule_tac p="Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}" in idle_thread_not_in_queue,simp,simp) apply (clarsimp) apply (wp hoare_drop_imp| simp | clarsimp simp: valid_sched_def)+ apply (frule max_set_not_empty, fastforce) apply (wp hoare_drop_imp| simp)+ 
    (* dom_t = 0 *)
     apply (simp only: schedule_def_2) apply (rule corres_guard_imp) apply (rule_tac P=\<top> and P'=\<top> and R="\<lambda>_. \<top>" and R'="\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread"
              in corres_split) apply (rule change_current_domain_dcorres) apply (clarsimp) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r, rename_tac rq) apply (fold dc_def, rule dcorres_rhs_noop_below_True[OF set_scheduler_action_dcorres]) apply (rule corres_guard_imp) apply (rule corres_if_rhs) 
               (* No threads in ready queues *)
                apply (rule corres_alternate2) apply (rule switch_to_idle_thread_dcorres) 
              (* threads in ready queues *)
               apply (rule corres_alternate1) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule_tac P'="\<lambda>s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread"
                         in stronger_corres_guard_imp) 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 clarsimp apply (frule_tac prio="(Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})" in schedule_choose_new_thread_helper,simp,simp,simp,simp,simp) apply (clarsimp simp: invs_def valid_state_def valid_sched_def) apply (auto 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)[1] apply (clarsimp simp: invs_def valid_state_def valid_sched_def max_non_empty_queue_def) apply (frule_tac p="Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}" in idle_thread_not_in_queue,simp,simp) apply (clarsimp) apply (wp hoare_drop_imp | clarsimp)+ apply (frule max_set_not_empty, fastforce) apply (wp hoare_drop_imp | clarsimp)+ apply simp apply (wp | clarsimp)+ unfolding dc_def apply (wp next_domain_valid_etcbs | simp)+ apply (wp tcb_sched_action_transform | clarsimp simp: valid_sched_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread) Schedule_D.schedule schedule_choose_new_thread proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread) Schedule_D.schedule (do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread) Schedule_D.schedule (do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (3 subgoals):
 1. \<And>dom_t. dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 3. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 3. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'7 dom_t cur_dom) Schedule_D.schedule (do x <- gets (\<lambda>s. ready_queues s cur_dom);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 3. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 5. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>dom_t cur_dom rq. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'11 dom_t cur_dom rq) Schedule_D.schedule (do y <- if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 3. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 5. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>dom_t cur_dom rq. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'11 dom_t cur_dom rq) Schedule_D.schedule (if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 3. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 5. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>dom_t cur_dom rq. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'11 dom_t cur_dom rq) Schedule_D.schedule (if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 3. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 5. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>dom_t cur_dom rq. dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (?Q18 dom_t cur_dom rq) (?Q'18 dom_t cur_dom rq) Schedule_D.schedule (if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ?Q18 dom_t cur_dom rq s
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ?Q'18 dom_t cur_dom rq s
 4. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 5. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 7. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<forall>prio. rq prio = []\<rbrakk> \<Longrightarrow> dcorres dc (?P22 dom_t cur_dom rq) (?Q22 dom_t cur_dom rq) Schedule_D.schedule switch_to_idle_thread
 2. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) Schedule_D.schedule (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?P22 dom_t cur_dom rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?Q22 dom_t cur_dom rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 5. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 6. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 8. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<forall>prio. rq prio = []\<rbrakk> \<Longrightarrow> dcorres dc (?P22 dom_t cur_dom rq) (?Q22 dom_t cur_dom rq) (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) switch_to_idle_thread
 2. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) Schedule_D.schedule (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?P22 dom_t cur_dom rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?Q22 dom_t cur_dom rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 5. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 6. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 8. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<forall>prio. rq prio = []\<rbrakk> \<Longrightarrow> dcorres dc (?P22 dom_t cur_dom rq) (?Q22 dom_t cur_dom rq) (do y <- change_current_domain;
Schedule_D.switch_to_thread None
od) switch_to_idle_thread
 2. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) Schedule_D.schedule (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?P22 dom_t cur_dom rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?Q22 dom_t cur_dom rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 5. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 6. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 8. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) Schedule_D.schedule (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 5. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 7. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) Schedule_D.schedule (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 5. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 7. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) (do 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 change_current_domain;
Schedule_D.switch_to_thread None
od) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 5. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 7. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'22 dom_t cur_dom rq) (do 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 ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 3. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 4. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 5. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 7. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'31 dom_t cur_dom rq rv) (do 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 <- assert (runnable rv);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 3. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 5. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 6. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 7. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 9. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>dom_t cur_dom rq rv rva. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?P'22 dom_t cur_dom rq) (?Q'35 dom_t cur_dom rq rv rva) (do 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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>?Q'35 dom_t cur_dom rq rv\<rbrace>
 3. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 5. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 8. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 9. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>dom_t cur_dom rq rv rva. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?Q39 dom_t cur_dom rq rv rva) (?Q'39 dom_t cur_dom rq rv rva) (do 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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q39 dom_t cur_dom rq rv rva s
 3. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'39 dom_t cur_dom rq rv rva s'
 4. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 7. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 10. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>dom_t cur_dom rq rv rva rvb. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> dcorres dc (?Q40 dom_t cur_dom rq rv rva rvb) (?Q'39 dom_t cur_dom rq rv rva) (K_bind (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) rvb) (Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvb. ?Q40 dom_t cur_dom rq rv rva rvb s \<and> (rvb, s) \<in> fst (change_current_domain s)
 3. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'39 dom_t cur_dom rq rv rva s'
 4. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 7. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 10. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>dom_t cur_dom rq rv prio. \<lbrakk>dom_t \<noteq> 0; rq prio \<noteq> []\<rbrakk> \<Longrightarrow> dcorres dc (?Q40 dom_t cur_dom rq rv () ()) (?Q'39 dom_t cur_dom rq rv ()) (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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvb. ?Q40 dom_t cur_dom rq rv rva rvb s \<and> (rvb, s) \<in> fst (change_current_domain s)
 3. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'39 dom_t cur_dom rq rv rva s'
 4. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 7. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 10. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>dom_t cur_dom rq rv prio next_domain. \<lbrakk>dom_t \<noteq> 0; rq prio \<noteq> []\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>a. ?Q46 dom_t cur_dom rq rv () () a next_domain) (?Q'39 dom_t cur_dom rq rv ()) (do 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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvb. (\<exists>rvc. ?Q46 dom_t cur_dom rq rv rva rvb s rvc \<and> (rvc, s) \<in> fst (gets cdl_current_domain s)) \<and> (rvb, s) \<in> fst (change_current_domain s)
 3. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'39 dom_t cur_dom rq rv rva s'
 4. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 7. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 10. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>dom_t cur_dom rq rv prio next_domain rva. \<lbrakk>dom_t \<noteq> 0; rq prio \<noteq> []\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>a. ?Q53 dom_t cur_dom rq rv () () next_domain a rva) (?Q'39 dom_t cur_dom rq rv ()) (do next_thread <- select rva;
Schedule_D.switch_to_thread (Some next_thread)
od) (Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvb. (\<exists>rvc. (\<exists>rvd. ?Q53 dom_t cur_dom rq rv rva rvb rvc s rvd \<and> (rvd, s) \<in> fst (gets (active_tcbs_in_domain rvc) s)) \<and> (rvc, s) \<in> fst (gets cdl_current_domain s)) \<and> (rvb, s) \<in> fst (change_current_domain s)
 3. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'39 dom_t cur_dom rq rv rva s'
 4. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 7. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 10. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>dom_t cur_dom rq rv prio next_domain rva rvb. \<lbrakk>dom_t \<noteq> 0; rq prio \<noteq> []\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>a. ?Q59 dom_t cur_dom rq rv () () next_domain rva a rvb) (?Q'39 dom_t cur_dom rq rv ()) (Schedule_D.switch_to_thread (Some rvb)) (Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvb. (\<exists>rvc. (\<exists>rvd. (\<exists>rve. ?Q59 dom_t cur_dom rq rv rva rvb rvc rvd s rve \<and> (rve, s) \<in> fst (select rvd s)) \<and> (rvd, s) \<in> fst (gets (active_tcbs_in_domain rvc) s)) \<and> (rvc, s) \<in> fst (gets cdl_current_domain s)) \<and> (rvb, s) \<in> fst (change_current_domain s)
 3. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'39 dom_t cur_dom rq rv rva s'
 4. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 7. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 10. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rv. (\<exists>rva. (\<exists>rv. hd (rq (Max {prio. rq prio \<noteq> []})) = 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)
 2. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 6. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 10. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>dom_t cur_dom s' prio. \<lbrakk>dom_t \<noteq> 0; ?P'22 dom_t cur_dom (ready_queues s' (cur_domain s')) (transform s'); ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; invs s'; scheduler_action s' = choose_new_thread\<rbrakk> \<Longrightarrow> (\<exists>rv. (\<exists>rva. (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})), 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>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); ?P'22 dom_t cur_dom rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 6. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'22 dom_t cur_dom rq s)
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 10. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>dom_t s' prio. \<lbrakk>dom_t \<noteq> 0; ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; invs s'; scheduler_action s' = choose_new_thread; (\<exists>y. cdl_objects (transform s') (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))) = Some y) \<and> hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})) \<in> active_tcbs_in_domain (cur_domain s') (transform s')\<rbrakk> \<Longrightarrow> (\<exists>rv. (\<exists>rva. (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})), 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>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); rq (Max {prio. rq prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 6. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 10. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>dom_t s' prio y. \<lbrakk>dom_t \<noteq> 0; ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; \<forall>d p. (\<forall>t\<in>set (ready_queues s' d p). is_etcb_at t s' \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s' \<and> st_tcb_at runnable t s') \<and> distinct (ready_queues s' d p); ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; invs s'; scheduler_action s' = choose_new_thread; hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})) \<in> active_tcbs_in_domain (cur_domain s') (transform s'); cdl_objects (transform s') (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))) = Some y\<rbrakk> \<Longrightarrow> (\<exists>rv. (\<exists>rva. (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})), 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>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); rq (Max {prio. rq prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 6. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 8. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 9. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 10. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>dom_t cur_dom rq rv rva s s'. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = []); rq (Max {prio. rq prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 2. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 5. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 8. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 9. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>dom_t s' prio. \<lbrakk>dom_t \<noteq> 0; ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; scheduler_action s' = choose_new_thread; idle_thread s' = hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))\<rbrakk> \<Longrightarrow> False
 2. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 5. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 8. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 9. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>dom_t s' prio. \<lbrakk>dom_t \<noteq> 0; ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; scheduler_action s' = choose_new_thread; idle_thread s' = hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})); idle_thread s' \<noteq> hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))\<rbrakk> \<Longrightarrow> False
 2. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 5. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 7. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 8. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 9. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>dom_t cur_dom rq rv. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 dom_t cur_dom rq rv\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 2. \<And>dom_t cur_dom rq rv cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>dom_t cur_dom rq. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 dom_t cur_dom rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'31 dom_t cur_dom rq\<rbrace>
 4. \<And>dom_t cur_dom rq cs. \<lbrakk>dom_t \<noteq> 0; \<not> (\<forall>prio. rq prio = [])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; True\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 6. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'22 dom_t cur_dom rq s)
 7. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 8. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 10. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 13 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>dom_t rq prio. \<lbrakk>dom_t \<noteq> 0; rq prio \<noteq> []; rq (Max {prio. rq prio \<noteq> []}) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread)
 3. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 4. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 6. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 8. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>dom_t cur_dom rq s. \<lbrakk>dom_t \<noteq> 0; ?Q'11 dom_t cur_dom rq s\<rbrakk> \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread)
 2. \<And>dom_t cur_dom. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'7 dom_t cur_dom\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>?Q'11 dom_t cur_dom\<rbrace>
 3. \<And>dom_t cur_dom cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s cur_dom) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>dom_t. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>?Q' dom_t\<rbrace> gets cur_domain \<lbrace>?Q'7 dom_t\<rbrace>
 5. \<And>dom_t cs. dom_t \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>dom_t. \<not> dom_t \<noteq> 0 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q' dom_t) Schedule_D.schedule (do when (dom_t = 0) next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>?Q'\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread) Schedule_D.schedule (do y <- next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread) Schedule_D.schedule (do y <- next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread) (do change_current_domain;
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 \<sqinter> Schedule_D.switch_to_thread None
od) (do y <- next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. dcorres dc ?Q174 ?Q'174 (do change_current_domain;
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 \<sqinter> Schedule_D.switch_to_thread None
od) (do y <- next_domain;
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. True \<Longrightarrow> ?Q174 s
 3. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ?Q'174 s
 4. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. dcorres ?r'178 (\<lambda>_. True) (\<lambda>_. True) change_current_domain next_domain
 2. \<And>rv rv'. ?r'178 rv rv' \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread) (K_bind (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 \<sqinter> Schedule_D.switch_to_thread None) rv) (do x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 3. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 6. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread) (K_bind (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 \<sqinter> Schedule_D.switch_to_thread None) rv) (do x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 5. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 6. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread) (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 \<sqinter> Schedule_D.switch_to_thread None) (do x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 5. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 6. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q'182 rv) (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 \<sqinter> Schedule_D.switch_to_thread None) (do x <- gets (\<lambda>s. ready_queues s rv);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (x (Max {prio. x prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (x (Max {prio. x prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 7. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 8. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>rv rq. dcorres dc (\<lambda>_. True) (?Q'186 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (do y <- if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 9. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rq. dcorres dc (\<lambda>_. True) (?Q'186 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 7. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 9. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rq. dcorres dc (?Q193 rv rq) (?Q'193 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (if \<forall>prio. rq prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>rv rq s. True \<Longrightarrow> ?Q193 rv rq s
 3. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ?Q'193 rv rq s
 4. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 9. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rq. \<forall>prio. rq prio = [] \<Longrightarrow> dcorres dc (?P197 rv rq) (?Q197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) switch_to_idle_thread
 2. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 3. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?P197 rv rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 4. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?Q197 rv rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 5. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 10. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rq. \<forall>prio. rq prio = [] \<Longrightarrow> dcorres dc (?P197 rv rq) (?Q197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) switch_to_idle_thread
 2. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 3. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?P197 rv rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 4. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?Q197 rv rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 5. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 10. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rq. \<forall>prio. rq prio = [] \<Longrightarrow> dcorres dc (?P197 rv rq) (?Q197 rv rq) (Schedule_D.switch_to_thread None) switch_to_idle_thread
 2. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 3. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?P197 rv rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 4. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> ?Q197 rv rq s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 5. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 10. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 3. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 4. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 9. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'197 rv rq) (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 \<sqinter> Schedule_D.switch_to_thread None) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 3. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 4. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 9. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'197 rv rq) (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) (do ts <- get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []})));
y <- assert (runnable ts);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 3. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 4. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 9. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'204 rv rq rva) (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) (do y <- assert (runnable rva);
Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []})))
od)
 2. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 3. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 5. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 6. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 7. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>rv rq rva rvb. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?P'197 rv rq) (?Q'208 rv rq rva rvb) (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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>?Q'208 rv rq rva\<rbrace>
 3. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 5. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 7. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 8. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
A total of 17 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rq rva rvb. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?Q212 rv rq rva rvb) (?Q'212 rv rq rva rvb) (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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q212 rv rq rva rvb s
 3. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'212 rv rq rva rvb s'
 4. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 7. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 9. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 10. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
A total of 19 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rq rva rvb next_domain. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?Q213 rv rq rva rvb next_domain) (?Q'212 rv rq rva rvb) (do 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 (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvc. ?Q213 rv rq rva rvb rvc s \<and> (rvc, s) \<in> fst (gets cdl_current_domain s)
 3. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'212 rv rq rva rvb s'
 4. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 7. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 9. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 10. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
A total of 19 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rq rva rvb next_domain threads. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?Q215 rv rq rva rvb next_domain threads) (?Q'212 rv rq rva rvb) (do next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od) (Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvc. (\<exists>rvd. ?Q215 rv rq rva rvb rvc rvd s \<and> (rvd, s) \<in> fst (gets (active_tcbs_in_domain rvc) s)) \<and> (rvc, s) \<in> fst (gets cdl_current_domain s)
 3. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'212 rv rq rva rvb s'
 4. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 7. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 9. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 10. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
A total of 19 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rq rva rvb next_domain threads next_thread. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> dcorres dc (?Q217 rv rq rva rvb next_domain threads next_thread) (?Q'212 rv rq rva rvb) (Schedule_D.switch_to_thread (Some next_thread)) (Schedule_A.switch_to_thread (hd (rq (Max {prio. rq prio \<noteq> []}))))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rvc. (\<exists>rvd. (\<exists>rve. ?Q217 rv rq rva rvb rvc rvd rve s \<and> (rve, s) \<in> fst (select rvd s)) \<and> (rvd, s) \<in> fst (gets (active_tcbs_in_domain rvc) s)) \<and> (rvc, s) \<in> fst (gets cdl_current_domain s)
 3. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'212 rv rq rva rvb s'
 4. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 7. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 9. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 10. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
A total of 19 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rva. (\<exists>rv. hd (rq (Max {prio. rq prio \<noteq> []})) = 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)
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 6. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 8. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 9. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv s' prio. \<lbrakk>?P'197 rv (ready_queues s' (cur_domain s')) (transform s'); ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; invs s'; scheduler_action s' = choose_new_thread\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rva. (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})), 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'))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); ?P'197 rv rq s; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 6. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?P'197 rv rq s)
 8. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 9. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>s' prio. \<lbrakk>ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; invs s'; scheduler_action s' = choose_new_thread; (\<exists>y. cdl_objects (transform s') (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))) = Some y) \<and> hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})) \<in> active_tcbs_in_domain (cur_domain s') (transform s')\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rva. (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})), 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'))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); rq (Max {prio. rq prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 6. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 8. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 9. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>s' prio y. \<lbrakk>ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; scheduler_action s' = choose_new_thread; valid_pspace s'; hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})) \<in> active_tcbs_in_domain (cur_domain s') (transform s'); cdl_objects (transform s') (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))) = Some y; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'\<rbrakk> \<Longrightarrow> \<exists>rv. (\<exists>rva. (hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})), 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'))
 2. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); rq (Max {prio. rq prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 3. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 6. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 8. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 9. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>rv rq rva rvb s s'. \<lbrakk>\<not> (\<forall>prio. rq prio = []); rq (Max {prio. rq prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') = rq \<and> valid_etcbs s' \<and> valid_sched_except_blocked s' \<and> invs s' \<and> scheduler_action s' = choose_new_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> hd (rq (Max {prio. rq prio \<noteq> []}))) and valid_etcbs) s'
 2. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 5. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 7. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 8. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
A total of 17 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>s' prio. \<lbrakk>ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; scheduler_action s' = choose_new_thread; idle_thread s' = hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))\<rbrakk> \<Longrightarrow> False
 2. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 5. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 7. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 8. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
A total of 17 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>s' prio. \<lbrakk>ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}) \<noteq> []; ready_queues s' (cur_domain s') prio \<noteq> []; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') choose_new_thread (cur_thread s'); valid_idle_etcb s'; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; scheduler_action s' = choose_new_thread; idle_thread s' = hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []})); idle_thread s' \<noteq> hd (ready_queues s' (cur_domain s') (Max {prio. ready_queues s' (cur_domain s') prio \<noteq> []}))\<rbrakk> \<Longrightarrow> False
 2. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 5. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 7. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 8. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rq rva. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'204 rv rq rva\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 2. \<And>rv rq rva cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (runnable rva) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv rq. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>?Q'197 rv rq\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>?Q'204 rv rq\<rbrace>
 4. \<And>rv rq cs. \<not> (\<forall>prio. rq prio = []) \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state (hd (rq (Max {prio. rq prio \<noteq> []}))) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv rq s. True \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> rq (Max {prio. rq prio \<noteq> []}) \<noteq> [])
 6. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ?Q'197 rv rq s)
 7. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 8. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 16 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rq prio. \<lbrakk>rq prio \<noteq> []; rq (Max {prio. rq prio \<noteq> []}) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread)
 3. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 4. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 8. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 10. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> (invs and valid_etcbs) s) \<and> (\<not> (\<forall>prio. rq prio = []) \<longrightarrow> ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread)
 2. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 7. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 9. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rq s. ?Q'186 rv rq s \<Longrightarrow> ((\<forall>prio. rq prio = []) \<longrightarrow> invs s \<and> valid_etcbs s) \<and> ((\<exists>prio. rq prio \<noteq> []) \<longrightarrow> ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread)
 2. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q'186 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 7. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 9. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 10. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv. \<lbrace>?Q'182 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. ((\<forall>prio. r prio = []) \<longrightarrow> invs s \<and> valid_etcbs s) \<and> ((\<exists>prio. r prio \<noteq> []) \<longrightarrow> ready_queues s (cur_domain s) = r \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread)\<rbrace>
 2. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets cur_domain \<lbrace>?Q'182\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 6. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 8. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 9. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>dc\<rbrace>
 2. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 4. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 5. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q178\<rbrace> change_current_domain \<lbrace>\<lambda>rv rv'. True\<rbrace>
 2. \<lbrace>?Q'178\<rbrace> next_domain \<lbrace>\<lambda>_ s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q178) s
 4. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q'178) s
 5. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. invs s \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s)
 2. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> gets domain_time \<lbrace>\<lambda>r s. (invs s \<and> valid_etcbs s) \<and> ready_queues s (cur_domain s) = ready_queues s (cur_domain s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!