theory Schedule_R

lemma tcbSchedAppend_corres:
  notes trans_state_update'[symmetric, simp del]
  shows
  "corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action (tcb_sched_append) t) (tcbSchedAppend t)" apply (simp only: tcbSchedAppend_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, simp) apply (rule no_fail_pre, wp, simp) apply (case_tac queued) apply (simp add: unless_def when_def) apply (rule corres_no_failI) apply wp+ 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) apply (subgoal_tac "tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y))
                       = (ready_queues a (tcb_domain y) (tcb_priority y))") apply (simp add: state_relation_def ready_queues_relation_def) apply (clarsimp simp: tcb_sched_append_def state_relation_def
                         valid_queues'_def ready_queues_relation_def
                         ekheap_relation_def etcb_relation_def
                         obj_at'_def inQ_def projectKO_eq project_inject) apply (drule_tac x=t in bspec,clarsimp) apply clarsimp apply (clarsimp simp: unless_def when_def cong: if_cong) 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_append_def) apply (intro conjI impI) apply (rule corres_guard_imp) apply (rule setQueue_corres) prefer 3 apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre) apply simp apply simp apply simp apply (rule corres_split_noop_rhs2) apply (rule addToBitmap_if_null_noop_corres) apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1] apply wp+ 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

(* 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_append t) (tcbSchedAppend 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_append 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 $ queue @ [t];
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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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' (\<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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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_append 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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<lbrakk>queued; True\<rbrakk> \<Longrightarrow> no_fail (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' tcbQueued t) (return ())
 2. \<And>queued. queued \<Longrightarrow> \<forall>(s, s')\<in>state_relation. is_etcb_at t s \<and> (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' tcbQueued t) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (return () s'). \<exists>(r, t)\<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_append t queue)
od) s). (t, t') \<in> state_relation \<and> dc r r')
 3. \<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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued. queued \<Longrightarrow> \<forall>(s, s')\<in>state_relation. is_etcb_at t s \<and> (tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' tcbQueued t) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (return () s'). \<exists>(r, t)\<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_append t queue)
od) s). (t, t') \<in> state_relation \<and> dc r r')
 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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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; (a, b) \<in> state_relation; ekheap a t = Some y; tcb_at' t b; Invariants_H.valid_queues b; valid_queues' b; obj_at' tcbQueued t b\<rbrakk> \<Longrightarrow> (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain y \<and> p = tcb_priority y then tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y)) else ready_queues a d' p) a, b) \<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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued a b y. \<lbrakk>queued; (a, b) \<in> state_relation; ekheap a t = Some y; tcb_at' t b; Invariants_H.valid_queues b; valid_queues' b; obj_at' tcbQueued t b; tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y)) = ready_queues a (tcb_domain y) (tcb_priority y)\<rbrakk> \<Longrightarrow> (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain y \<and> p = tcb_priority y then tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y)) else ready_queues a d' p) a, b) \<in> state_relation
 2. \<And>queued a b y. \<lbrakk>queued; (a, b) \<in> state_relation; ekheap a t = Some y; tcb_at' t b; Invariants_H.valid_queues b; valid_queues' b; obj_at' tcbQueued t b\<rbrakk> \<Longrightarrow> tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y)) = ready_queues a (tcb_domain y) (tcb_priority y)
 3. \<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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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; (a, b) \<in> state_relation; ekheap a t = Some y; tcb_at' t b; Invariants_H.valid_queues b; valid_queues' b; obj_at' tcbQueued t b\<rbrakk> \<Longrightarrow> tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y)) = ready_queues a (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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y obja. \<lbrakk>queued; ekheap a t = Some y; Invariants_H.valid_queues b; \<forall>d p t. (\<exists>ko. ksPSpace b t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. KOTCB obj = ko \<and> tcbQueued obj \<and> tcbPriority obj = p \<and> tcbDomain obj = d \<and> ps_clear t (objBitsKO ko) b)) \<longrightarrow> t \<in> set (ksReadyQueues b (d, p)); pspace_relation (kheap a) (ksPSpace b); ksPSpace b t = Some (KOTCB obja); \<forall>x\<in>dom (ekheap a). \<exists>tcb'. ksPSpace b x = Some (KOTCB tcb') \<and> tcb_priority (the (ekheap a x)) = tcbPriority tcb' \<and> tcb_time_slice (the (ekheap a x)) = tcbTimeSlice tcb' \<and> tcb_domain (the (ekheap a x)) = tcbDomain tcb'; is_aligned t (objBitsKO (KOTCB obja)); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ps_clear t (objBitsKO (KOTCB obja)) b; \<forall>d p. ready_queues a d p = ksReadyQueues b (d, p); tcbQueued obja; 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\<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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y obja. \<lbrakk>queued; ekheap a t = Some y; Invariants_H.valid_queues b; \<forall>d p t. (\<exists>ko. ksPSpace b t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. KOTCB obj = ko \<and> tcbQueued obj \<and> tcbPriority obj = p \<and> tcbDomain obj = d \<and> ps_clear t (objBitsKO ko) b)) \<longrightarrow> t \<in> set (ksReadyQueues b (d, p)); pspace_relation (kheap a) (ksPSpace b); ksPSpace b t = Some (KOTCB obja); is_aligned t (objBitsKO (KOTCB obja)); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ps_clear t (objBitsKO (KOTCB obja)) b; \<forall>d p. ready_queues a d p = ksReadyQueues b (d, p); tcbQueued obja; 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; \<exists>tcb'. ksPSpace b t = Some (KOTCB tcb') \<and> tcb_priority (the (ekheap a t)) = tcbPriority tcb' \<and> tcb_time_slice (the (ekheap a t)) = tcbTimeSlice tcb' \<and> tcb_domain (the (ekheap a t)) = tcbDomain tcb'\<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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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. 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_append t queue)
od) (unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [t];
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_append t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
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 (?Q96 queued) (?Q'96 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_append t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
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> ?Q96 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'96 queued s' proof (prove)
goal (6 subgoals):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres (=) (?P100 queued) (?P'100 queued) (ethread_get tcb_domain t) (threadGet tcbDomain t)
 2. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R100 queued d) (?R'100 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R100 queued\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'100 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> (?P100 queued and ?Q100 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'100 queued and ?Q'100 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 (?R100 queued d) (?R'100 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R100 queued\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'100 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 ?Q100 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'100 queued) s' proof (prove)
goal (5 subgoals):
 1. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R100 queued d) (?R'100 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R100 queued\<rbrace>
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'100 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 ?Q100 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'100 queued) s' proof (prove)
goal (8 subgoals):
 1. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> corres (=) (?P108 queued d) (?P'110 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 (?R107 queued d tdom prio) (?R'107 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (queue @ [t]);
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>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R107 queued d tdom\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'107 queued d tdom\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. ?P108 queued d and ?Q109 queued d\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. ?P'110 queued tdom and ?Q'111 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 ?Q100 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'100 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 (?R107 queued d tdom prio) (?R'107 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (queue @ [t]);
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>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R107 queued d tdom\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'107 queued d tdom\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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'100 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 (?R107 queued d tdom prio) (?R'107 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (queue @ [t]);
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>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R107 queued d tdom\<rbrace>
 3. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'107 queued d tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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'100 queued) s' proof (prove)
goal (10 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres (=) (?P121 queued d tdom prio) (?P'123 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 (?R120 queued d tdom prio prioa queue) (?R'120 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_append t queue)) (do y <- setQueue tdom prioa (queuea @ [t]);
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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R120 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'120 queued d tdom prio prioa\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. ?P121 queued d tdom prio and ?Q122 queued d tdom prio\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. ?P'123 queued d tdom prioa and ?Q'124 queued d tdom prioa\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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'100 queued) s' proof (prove)
goal (10 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres (=) (?P121 False tdom tdom prioa) (?P'123 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 (?R120 queued d tdom prio prioa queue) (?R'120 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_append t queue)) (do y <- setQueue tdom prioa (queuea @ [t]);
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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R120 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'120 queued d tdom prio prioa\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. ?P121 queued d tdom prio and ?Q122 queued d tdom prio\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. ?P'123 queued d tdom prioa and ?Q'124 queued d tdom prioa\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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'100 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 (?R120 queued d tdom prio prioa queue) (?R'120 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_append t queue)) (do y <- setQueue tdom prioa (queuea @ [t]);
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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R120 queued d tdom prio prioa\<rbrace>
 3. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'120 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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'100 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 (?P131 queued d tdom prio prioa queue) (?P'133 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_append t queue)) (setQueue tdom prioa (queuea @ [t]))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P131 queued d tdom prio prioa queue and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'133 queued d tdom prio prioa queuea and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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> (t \<notin> set queuea \<longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa (queuea @ [t])) (setQueue tdom prioa (queuea @ [t]))) \<and> (t \<in> set queuea \<longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa queuea) (setQueue tdom prioa (queuea @ [t])))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P131 queued d tdom prio prioa queue and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'133 queued d tdom prio prioa queuea and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea\<rbrakk> \<Longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa (queuea @ [t])) (setQueue tdom prioa (queuea @ [t]))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<in> set queuea\<rbrakk> \<Longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa queuea) (setQueue tdom prioa (queuea @ [t]))
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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)
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P131 queued d tdom prio prioa queue and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'133 queued d tdom prio prioa queuea and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea\<rbrakk> \<Longrightarrow> corres dc (?Q146 queued d tdom prio prioa queue queuea) (?Q'146 queued d tdom prio prioa queue queuea) (set_tcb_queue tdom prioa (queuea @ [t])) (setQueue tdom prioa (queuea @ [t]))
 2. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; ?P131 False tdom tdom prioa prioa queuea s\<rbrakk> \<Longrightarrow> ?Q146 queued d tdom prio prioa queue queuea s
 3. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; ?P'133 False tdom tdom prioa prioa queuea s\<rbrakk> \<Longrightarrow> ?Q'146 queued d tdom prio prioa queue queuea s
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<in> set queuea\<rbrakk> \<Longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa queuea) (setQueue tdom prioa (queuea @ [t]))
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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)
 6. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 queued d tdom prio prioa queue queuea\<rbrace>
 7. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 queued d tdom prio prioa queue queuea\<rbrace>
 8. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P131 queued d tdom prio prioa queue and ?Q132 queued d tdom prio prioa queue\<rbrace>
 9. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'133 queued d tdom prio prioa queuea and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 10. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; ?P131 False tdom tdom prioa prioa queuea s\<rbrakk> \<Longrightarrow> True
 2. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; ?P'133 False tdom tdom prioa prioa queuea s\<rbrakk> \<Longrightarrow> True
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<in> set queuea\<rbrakk> \<Longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa queuea) (setQueue tdom prioa (queuea @ [t]))
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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)
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P131 queued d tdom prio prioa queue and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'133 queued d tdom prio prioa queuea and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 10. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<in> set queuea\<rbrakk> \<Longrightarrow> corres dc (?P131 False tdom tdom prioa prioa queuea) (?P'133 False tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa queuea) (setQueue tdom prioa (queuea @ [t]))
 2. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; ?P131 False tdom tdom prioa prioa queuea s\<rbrakk> \<Longrightarrow> True
 3. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; ?P'133 False tdom tdom prioa prioa queuea s\<rbrakk> \<Longrightarrow> True
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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)
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P131 queued d tdom prio prioa queue and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'133 queued d tdom prio prioa queuea and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 10. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea s s'. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<in> set 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 queuea) (setQueue tdom prioa (queuea @ [t]))
 2. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; True\<rbrakk> \<Longrightarrow> True
 3. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; K (t \<notin> set queuea) s\<rbrakk> \<Longrightarrow> True
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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)
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 10. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; True\<rbrakk> \<Longrightarrow> True
 2. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; K (t \<notin> set queuea) s\<rbrakk> \<Longrightarrow> True
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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)
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea s. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea; t \<notin> set queuea; K (t \<notin> set queuea) s\<rbrakk> \<Longrightarrow> True
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R130 queued d tdom prio prioa queue queuea) (?R'130 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 (?R130 queued d tdom prio prioa queue queuea) (?R'130 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?R130 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?R'130 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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 (?P155 queued d tdom prio prioa queue queuea) (?P'155 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 (?R155 queued d tdom prio prioa queue queuea) (?R'155 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>?Q155 queued d tdom prio prioa queue queuea\<rbrace> return () \<lbrace>\<lambda>x. ?R155 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'155 queued d tdom prio prioa queue queuea\<rbrace> if null queuea then addToBitmap tdom prioa else return () \<lbrace>\<lambda>x. ?R'155 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. ?P155 queued d tdom prio prioa queue queuea and ?Q155 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. ?P'155 queued d tdom prio prioa queue queuea and ?Q'155 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 10. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 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 (?R155 queued d tdom prio prioa queue queuea) (?R'155 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>?Q155 queued d tdom prio prioa queue queuea\<rbrace> return () \<lbrace>\<lambda>x. ?R155 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'155 queued d tdom prio prioa queue queuea\<rbrace> if null queuea then addToBitmap tdom prioa else return () \<lbrace>\<lambda>x. ?R'155 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q155 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'155 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 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>?Q155 queued d tdom prio prioa queue queuea\<rbrace> return () \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>\<not> queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'155 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>?Q132 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_append t queue) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q155 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'134 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'155 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>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and ?Q132 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'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and ?Q'134 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 10. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 queued tdom\<rbrace>
A total of 12 subgoals... 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> \<lbrace>?P'189 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (queuea @ [t]) \<lbrace>\<lambda>rv s. (null queuea \<longrightarrow> tcb_at' t s) \<and> (\<not> null queuea \<longrightarrow> tcb_at' t s)\<rbrace>
 2. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q122 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. True) and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>a. True)) (ready_queues_update (\<lambda>_ t' p. if t' = d \<and> p = prio then tcb_sched_append t queue else ready_queues a t' p) a))\<rbrace>
 3. \<And>queued d tdom prio prioa. \<lbrakk>\<not> queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'124 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. K (t \<notin> set queuea) and (\<lambda>s. True \<and> ?P'189 queued d tdom prio prioa queuea s)\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q109 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. True) and ?Q122 queued d tdom prio\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>\<not> queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'111 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. True) and ?Q'124 queued d tdom prioa\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q100 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q109 queued d\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q'100 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'111 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 ?Q100 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'100 queued) s' 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!