theory TcbAcc_R

lemma tcbSchedEnqueue_corres:
  "corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues')
             (tcb_sched_action (tcb_sched_enqueue) t) (tcbSchedEnqueue t)" proof - have ready_queues_helper:
    "\<And>t tcb a b. \<lbrakk> ekheap a t = Some tcb;  obj_at' tcbQueued t b  ;  valid_queues' b  ;
                   ekheap_relation (ekheap a) (ksPSpace b) \<rbrakk>
                 \<Longrightarrow> t \<in> set (ksReadyQueues b (tcb_domain tcb, tcb_priority tcb))" unfolding valid_queues'_def by (fastforce dest: ekheap_relation_absD simp: obj_at'_def inQ_def etcb_relation_def projectKO_eq projectKO_tcb) show ?thesis unfolding tcbSchedEnqueue_def tcb_sched_action_def apply (rule corres_symb_exec_r [OF _ _ threadGet_inv,
             where Q'="\<lambda>rv. tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"]) defer apply (wp threadGet_obj_at'; simp_all) apply (rule no_fail_pre, wp, blast) apply (case_tac queued; simp_all) apply (rule corres_no_failI; simp add: no_fail_return) apply (clarsimp simp: in_monad ethread_get_def gets_the_def bind_assoc
                           assert_opt_def exec_gets is_etcb_at_def get_etcb_def get_tcb_queue_def
                           set_tcb_queue_def simpler_modify_def ready_queues_relation_def
                           state_relation_def tcb_sched_enqueue_def) apply (rule ready_queues_helper; auto) apply (clarsimp simp: when_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split[where r'="(=)"]) apply (rule ethreadget_corres) apply (simp add: etcb_relation_def) apply (rule corres_split[where r'="(=)"]) apply (rule ethreadget_corres) apply (simp add: etcb_relation_def) apply (rule corres_split[where r'="(=)"]) apply simp apply (rule getQueue_corres) apply (rule corres_split_noop_rhs2) apply (simp add: tcb_sched_enqueue_def split del: if_split) apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre) apply simp apply (rule setQueue_corres[unfolded dc_def]) apply (rule corres_split_noop_rhs2) apply (fastforce intro: addToBitmap_noop_corres) apply (fastforce intro: threadSet_corres_noop simp: tcb_relation_def exst_same_def) apply (wp getObject_tcb_wp  | simp add: threadGet_def)+ apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def
                           projectKO_eq project_inject) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t) proof (state)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t) proof (prove)
goal (1 subgoal):
 1. \<And>t tcb a b. \<lbrakk>ekheap a t = Some tcb; obj_at' tcbQueued t b; valid_queues' b; ekheap_relation (ekheap a) (ksPSpace b)\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues b (tcb_domain tcb, tcb_priority tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>t tcb a b. \<lbrakk>ekheap a t = Some tcb; obj_at' tcbQueued t b; \<forall>d p t. obj_at' (inQ d p) t b \<longrightarrow> t \<in> set (ksReadyQueues b (d, p)); ekheap_relation (ekheap a) (ksPSpace b)\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues b (tcb_domain tcb, tcb_priority tcb)) proof (state)
this:
\<lbrakk>ekheap ?a ?t = Some ?tcb; obj_at' tcbQueued ?t ?b; valid_queues' ?b; ekheap_relation (ekheap ?a) (ksPSpace ?b)\<rbrakk> \<Longrightarrow> ?t \<in> set (ksReadyQueues ?b (tcb_domain ?tcb, tcb_priority ?tcb))

goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t) proof (prove)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t) proof (prove)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<lbrace>tcb_at' t and Invariants_H.valid_queues and valid_queues'\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace>
 3. True \<Longrightarrow> no_fail (tcb_at' t and Invariants_H.valid_queues and valid_queues') (threadGet tcbQueued t) proof (prove)
goal (3 subgoals):
 1. \<lbrace>tcb_at' t and Invariants_H.valid_queues and valid_queues'\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace>
 2. True \<Longrightarrow> no_fail (tcb_at' t and Invariants_H.valid_queues and valid_queues') (threadGet tcbQueued t)
 3. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> no_fail (tcb_at' t and Invariants_H.valid_queues and valid_queues') (threadGet tcbQueued t)
 2. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (1 subgoal):
 1. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' tcbQueued t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (return ())
 2. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued. queued \<Longrightarrow> \<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> is_etcb_at t s \<and> tcb_at' t s' \<and> Invariants_H.valid_queues s' \<and> valid_queues' s' \<and> obj_at' tcbQueued t s' \<longrightarrow> (\<forall>x\<in>fst (return () s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) s). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation)
 2. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y. \<lbrakk>queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); \<forall>d p. ready_queues a d p = ksReadyQueues b (d, p); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; ekheap a t = Some y; tcb_at' t b; Invariants_H.valid_queues b; valid_queues' b; obj_at' tcbQueued t b\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues b (tcb_domain y, tcb_priority y))
 2. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (1 subgoal):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (1 subgoal):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres dc (?Q111 queued) (?Q'111 queued) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q111 queued s
 3. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q'111 queued s' proof (prove)
goal (6 subgoals):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres (=) (?P115 queued) (?P'115 queued) (ethread_get tcb_domain t) (threadGet tcbDomain t)
 2. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R115 queued d) (?R'115 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R115 queued\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'115 queued\<rbrace>
 5. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (?P115 queued and ?Q115 queued) s
 6. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (?P'115 queued and ?Q'115 queued) s' proof (prove)
goal (6 subgoals):
 1. \<And>queued etcb tcb'. \<lbrakk>\<not> queued; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> tcb_domain etcb = tcbDomain tcb'
 2. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R115 queued d) (?R'115 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R115 queued\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'115 queued\<rbrace>
 5. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 6. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (5 subgoals):
 1. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R115 queued d) (?R'115 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R115 queued\<rbrace>
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'115 queued\<rbrace>
 4. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 5. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (8 subgoals):
 1. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres (=) (?P123 queued d) (?P'125 queued tdom) (ethread_get tcb_priority t) (threadGet tcbPriority t)
 2. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres dc (?R122 queued d tdom prio) (?R'122 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (t # queue);
y <- if null queue then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R122 queued d tdom\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'122 queued d tdom\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. ?P123 queued d and ?Q124 queued d\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. ?P'125 queued tdom and ?Q'126 queued tdom\<rbrace>
 7. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 8. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (8 subgoals):
 1. \<And>queued d tdom etcb tcb'. \<lbrakk>\<not> queued; d = tdom; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> tcb_priority etcb = tcbPriority tcb'
 2. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres dc (?R122 queued d tdom prio) (?R'122 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (t # queue);
y <- if null queue then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R122 queued d tdom\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'122 queued d tdom\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
 7. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 8. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (7 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres dc (?R122 queued d tdom prio) (?R'122 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (t # queue);
y <- if null queue then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R122 queued d tdom\<rbrace>
 3. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'122 queued d tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
 6. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 7. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (10 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres (=) (?P136 queued d tdom prio) (?P'138 queued d tdom prioa) (get_tcb_queue d prio) (getQueue tdom prioa)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R135 queued d tdom prio prioa queue) (?R'135 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_enqueue t queue)) (do y <- setQueue tdom prioa (t # queuea);
y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R135 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'135 queued d tdom prio prioa\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. ?P136 queued d tdom prio and ?Q137 queued d tdom prio\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. ?P'138 queued d tdom prioa and ?Q'139 queued d tdom prioa\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
 9. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 10. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (10 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres (=) (?P136 False tdom tdom prioa) (?P'138 False tdom tdom prioa) (get_tcb_queue tdom prioa) (getQueue tdom prioa)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R135 queued d tdom prio prioa queue) (?R'135 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_enqueue t queue)) (do y <- setQueue tdom prioa (t # queuea);
y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R135 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'135 queued d tdom prio prioa\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. ?P136 queued d tdom prio and ?Q137 queued d tdom prio\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. ?P'138 queued d tdom prioa and ?Q'139 queued d tdom prioa\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
 9. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 10. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (9 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R135 queued d tdom prio prioa queue) (?R'135 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_enqueue t queue)) (do y <- setQueue tdom prioa (t # queuea);
y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R135 queued d tdom prio prioa\<rbrace>
 3. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'135 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
 8. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
 9. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'115 queued) s' proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?P146 queued d tdom prio prioa queue) (?P'148 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_enqueue t queue)) (setQueue tdom prioa (t # queuea))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R145 queued d tdom prio prioa queue queuea) (?R'145 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. ?R145 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. ?R'145 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P146 queued d tdom prio prioa queue and ?Q147 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'148 queued d tdom prio prioa queuea and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?P146 False tdom tdom prioa prioa queuea) (?P'148 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa (if t \<notin> set queuea then t # queuea else queuea)) (setQueue tdom prioa (t # queuea))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R145 queued d tdom prio prioa queue queuea) (?R'145 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. ?R145 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. ?R'145 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P146 queued d tdom prio prioa queue and ?Q147 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'148 queued d tdom prio prioa queuea and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea s s'. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; True; K (t \<notin> set queuea) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (K (t \<notin> set queuea)) (set_tcb_queue tdom prioa (if t \<notin> set queuea then t # queuea else queuea)) (setQueue tdom prioa (t # queuea))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R145 queued d tdom prio prioa queue queuea) (?R'145 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. ?R145 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. ?R'145 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q147 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea s s'. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>y. True) (set_tcb_queue tdom prioa (t # queuea)) (setQueue tdom prioa (t # queuea))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R145 queued d tdom prio prioa queue queuea) (?R'145 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. ?R145 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. ?R'145 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q147 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R145 queued d tdom prio prioa queue queuea) (?R'145 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null queuea then addToBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. ?R145 queued d tdom prio prioa queue queuea\<rbrace>
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. ?R'145 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q147 queued d tdom prio prioa queue\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
 10. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q115 queued) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?P157 queued d tdom prio prioa queue queuea) (?P'157 queued d tdom prio prioa queue queuea) (return ()) (if null queuea then addToBitmap tdom prioa else return ())
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R157 queued d tdom prio prioa queue queuea) (?R'157 queued d tdom prio prioa queue queuea) (return ()) (threadSet (tcbQueued_update (\<lambda>_. True)) t)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q157 queued d tdom prio prioa queue queuea\<rbrace> return () \<lbrace>\<lambda>x. ?R157 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 queued d tdom prio prioa queue queuea\<rbrace> if null queuea then addToBitmap tdom prioa else return () \<lbrace>\<lambda>x. ?R'157 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. ?P157 queued d tdom prio prioa queue queuea and ?Q157 queued d tdom prio prioa queue queuea\<rbrace>
 6. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. ?P'157 queued d tdom prio prioa queue queuea and ?Q'157 queued d tdom prio prioa queue queuea\<rbrace>
 7. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q147 queued d tdom prio prioa queue\<rbrace>
 8. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 10. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R157 queued d tdom prio prioa queue queuea) (?R'157 queued d tdom prio prioa queue queuea) (return ()) (threadSet (tcbQueued_update (\<lambda>_. True)) t)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q157 queued d tdom prio prioa queue queuea\<rbrace> return () \<lbrace>\<lambda>x. ?R157 queued d tdom prio prioa queue queuea\<rbrace>
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 queued d tdom prio prioa queue queuea\<rbrace> if null queuea then addToBitmap tdom prioa else return () \<lbrace>\<lambda>x. ?R'157 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. (\<lambda>a. True) and ?Q157 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. (\<lambda>a. True) and ?Q'157 queued d tdom prio prioa queue queuea\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q147 queued d tdom prio prioa queue\<rbrace>
 7. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q157 queued d tdom prio prioa queue queuea\<rbrace> return () \<lbrace>\<lambda>x a. True\<rbrace>
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'157 queued d tdom prio prioa queue queuea\<rbrace> if null queuea then addToBitmap tdom prioa else return () \<lbrace>\<lambda>x. tcb_at' t\<rbrace>
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q147 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_enqueue t queue) \<lbrace>\<lambda>x. (\<lambda>a. True) and ?Q157 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'149 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (t # queuea) \<lbrace>\<lambda>x. (\<lambda>a. True) and ?Q'157 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q137 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q147 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'149 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q124 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q137 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'126 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'139 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q115 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q124 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'115 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'126 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>queued s s'. \<lbrakk>\<not> queued; is_etcb_at t s; tcb_at' t s' \<and> Invariants_H.valid_queues s' \<and> valid_queues' s' \<and> obj_at' (\<lambda>obj. \<not> tcbQueued obj) t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s' \<and> (\<exists>tb. ko_at' tb t s' \<and> t \<notin> set (ksReadyQueues s' (tcbDomain ta, tcbPriority tb))) proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t)

goal:
No subgoals!