theory TcbAcc_R

lemma tcbSchedDequeue_corres:
  "corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues)
             (tcb_sched_action tcb_sched_dequeue t) (tcbSchedDequeue t)" apply (simp only: tcbSchedDequeue_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 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) defer apply (simp add: when_def) apply (rule corres_no_failI) apply (wp) apply (clarsimp simp: in_monad ethread_get_def set_tcb_queue_def is_etcb_at_def state_relation_def) apply (subgoal_tac "t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))") prefer 2 subgoal by (force simp: tcb_sched_dequeue_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def
                            ready_queues_relation_def obj_at'_def inQ_def projectKO_eq project_inject) apply (subst gets_the_exec) apply (simp add: get_etcb_def) apply (subst gets_the_exec) apply (simp add: get_etcb_def) apply (simp add: exec_gets simpler_modify_def get_etcb_def ready_queues_relation_def cong: if_cong get_tcb_queue_def) apply (simp add: when_def) apply (rule corres_guard_imp) apply (rule corres_split[where r'="(=)"]) apply (rule ethreadget_corres, simp add: etcb_relation_def) apply (rule corres_split[where r'="(=)"]) apply (rule ethreadget_corres, simp add: etcb_relation_def) apply (rule corres_split[where r'="(=)"]) apply (simp, rule getQueue_corres) apply (rule corres_split_noop_rhs2) apply (simp add: tcb_sched_dequeue_def) apply (rule setQueue_corres) apply (rule corres_split_noop_rhs) apply (clarsimp, rule removeFromBitmap_corres_noop) apply (rule threadSet_corres_noop; simp_all add: tcb_relation_def exst_same_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues) (tcb_sched_action tcb_sched_dequeue t) (tcbSchedDequeue t) proof (prove)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (do queued <- threadGet tcbQueued t;
when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) 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 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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<lbrace>tcb_at' t and Invariants_H.valid_queues\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. tcb_at' t and Invariants_H.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) (threadGet tcbQueued t) proof (prove)
goal (3 subgoals):
 1. \<lbrace>tcb_at' t and Invariants_H.valid_queues\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. tcb_at' t and Invariants_H.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) (threadGet tcbQueued t)
 3. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. no_fail (tcb_at' t and Invariants_H.valid_queues) (threadGet tcbQueued t)
 2. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) 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 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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) 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 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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued. \<not> queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (return ())
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<lbrakk>\<not> queued; True\<rbrakk> \<Longrightarrow> no_fail (tcb_at' t and Invariants_H.valid_queues and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) (return ())
 2. \<And>queued. \<not> queued \<Longrightarrow> \<forall>(s, s')\<in>state_relation. is_etcb_at t s \<and> (tcb_at' t and Invariants_H.valid_queues and obj_at' (\<lambda>obj. \<not> tcbQueued obj) 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_dequeue t queue)
od) s). (t, t') \<in> state_relation \<and> dc r r')
 3. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued. \<not> queued \<Longrightarrow> \<forall>(s, s')\<in>state_relation. is_etcb_at t s \<and> (tcb_at' t and Invariants_H.valid_queues and obj_at' (\<lambda>obj. \<not> tcbQueued obj) 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_dequeue t queue)
od) s). (t, t') \<in> state_relation \<and> dc r r')
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- gets_the (get_etcb t);
tcba <- gets_the (get_etcb t);
queue <- get_tcb_queue (tcb_domain tcb) (tcb_priority tcba);
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain tcb \<and> p = tcb_priority tcba then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). case x of (r, t) \<Rightarrow> pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- gets_the (get_etcb t);
tcba <- gets_the (get_etcb t);
queue <- get_tcb_queue (tcb_domain tcb) (tcb_priority tcba);
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain tcb \<and> p = tcb_priority tcba then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). case x of (r, t) \<Rightarrow> pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 2. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b\<rbrakk> \<Longrightarrow> t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))
 3. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b\<rbrakk> \<Longrightarrow> t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))
 2. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- gets_the (get_etcb t);
tcba <- gets_the (get_etcb t);
queue <- get_tcb_queue (tcb_domain tcb) (tcb_priority tcba);
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain tcb \<and> p = tcb_priority tcba then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). case x of (r, t) \<Rightarrow> pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 3. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> queued_; pspace_relation (kheap a_) (ksPSpace b_); ekheap_relation (ekheap a_) (ksPSpace b_); sched_act_relation (scheduler_action a_) (ksSchedulerAction b_); ready_queues_relation (ready_queues a_) (ksReadyQueues b_); 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_; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b_\<rbrakk> \<Longrightarrow> t \<notin> set (ready_queues a_ (tcb_domain y_) (tcb_priority y_)) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- gets_the (get_etcb t);
tcba <- gets_the (get_etcb t);
queue <- get_tcb_queue (tcb_domain tcb) (tcb_priority tcba);
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain tcb \<and> p = tcb_priority tcba then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). case x of (r, t) \<Rightarrow> pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> get_etcb t a \<noteq> None
 2. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do tcb <- gets_the (get_etcb t);
queue <- get_tcb_queue (tcb_domain (the (get_etcb t a))) (tcb_priority tcb);
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain (the (get_etcb t a)) \<and> p = tcb_priority tcb then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 3. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do tcb <- gets_the (get_etcb t);
queue <- get_tcb_queue (tcb_domain (the (get_etcb t a))) (tcb_priority tcb);
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain (the (get_etcb t a)) \<and> p = tcb_priority tcb then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> get_etcb t a \<noteq> None
 2. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do queue <- get_tcb_queue (tcb_domain (the (get_etcb t a))) (tcb_priority (the (get_etcb t a)));
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain (the (get_etcb t a)) \<and> p = tcb_priority (the (get_etcb t a)) then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 3. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (2 subgoals):
 1. \<And>queued a b y. \<lbrakk>\<not> queued; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); 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; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b; t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do queue <- get_tcb_queue (tcb_domain (the (get_etcb t a))) (tcb_priority (the (get_etcb t a)));
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain (the (get_etcb t a)) \<and> p = tcb_priority (the (get_etcb t a)) then tcb_sched_dequeue t queue else ready_queues es d' p) es)
od) a). pspace_relation (kheap t) (ksPSpace b) \<and> ekheap_relation (ekheap t) (ksPSpace b) \<and> sched_act_relation (scheduler_action t) (ksSchedulerAction b) \<and> ready_queues_relation (ready_queues t) (ksReadyQueues b) \<and> ghost_relation (kheap t) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) t) (cdt t) (ctes_of b) \<and> cdt_list_relation (cdt_list t) (cdt t) (ctes_of b) \<and> revokable_relation (is_original_cap t) (null_filter (caps_of_state t)) (ctes_of b) \<and> (arch_state t, ksArchState b) \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState b) \<and> cur_thread t = ksCurThread b \<and> idle_thread t = ksIdleThread b \<and> machine_state t = ksMachineState b \<and> work_units_completed t = ksWorkUnitsCompleted b \<and> domain_index t = ksDomScheduleIdx b \<and> domain_list t = ksDomSchedule b \<and> cur_domain t = ksCurDomain b \<and> domain_time t = ksDomainTime b
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (1 subgoal):
 1. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (1 subgoal):
 1. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.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_dequeue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) proof (prove)
goal (3 subgoals):
 1. \<And>queued. queued \<Longrightarrow> corres dc (?Q74 queued) (?Q'74 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_dequeue t queue)
od) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> ?Q74 queued s
 3. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q'74 queued s proof (prove)
goal (6 subgoals):
 1. \<And>queued. queued \<Longrightarrow> corres (=) (?P78 queued) (?P'78 queued) (ethread_get tcb_domain t) (threadGet tcbDomain t)
 2. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R78 queued d) (?R'78 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_dequeue t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R78 queued\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'78 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (?P78 queued and ?Q78 queued) s
 6. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (?P'78 queued and ?Q'78 queued) s proof (prove)
goal (5 subgoals):
 1. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R78 queued d) (?R'78 queued tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_dequeue t queue)
od) (do prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R78 queued\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'78 queued\<rbrace>
 4. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
 5. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'78 queued) s proof (prove)
goal (8 subgoals):
 1. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres (=) (?P86 queued d) (?P'88 queued tdom) (ethread_get tcb_priority t) (threadGet tcbPriority t)
 2. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres dc (?R85 queued d tdom prio) (?R'85 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_dequeue t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R85 queued d tdom\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'85 queued d tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. ?P86 queued d and ?Q87 queued d\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. ?P'88 queued tdom and ?Q'89 queued tdom\<rbrace>
 7. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
 8. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'78 queued) s proof (prove)
goal (7 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres dc (?R85 queued d tdom prio) (?R'85 queued d tdom prioa) (do queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_dequeue t queue)
od) (do queue <- getQueue tdom prioa;
y <- setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>?R85 queued d tdom\<rbrace>
 3. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'85 queued d tdom\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
 6. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
 7. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'78 queued) s proof (prove)
goal (10 subgoals):
 1. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> corres (=) (?P99 queued d tdom prio) (?P'101 queued d tdom prioa) (get_tcb_queue d prio) (getQueue tdom prioa)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R98 queued d tdom prio prioa queue) (?R'98 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_dequeue t queue)) (do y <- setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea);
y <- if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R98 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'98 queued d tdom prio prioa\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. ?P99 queued d tdom prio and ?Q100 queued d tdom prio\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. ?P'101 queued d tdom prioa and ?Q'102 queued d tdom prioa\<rbrace>
 7. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 8. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
 9. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
 10. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'78 queued) s proof (prove)
goal (9 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R98 queued d tdom prio prioa queue) (?R'98 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_dequeue t queue)) (do y <- setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea);
y <- if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>?R98 queued d tdom prio prioa\<rbrace>
 3. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>?R'98 queued d tdom prio prioa\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 7. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
 8. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
 9. \<And>queued s. \<lbrakk>queued; (tcb_at' t and Invariants_H.valid_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'78 queued) s proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?P109 queued d tdom prio prioa queue) (?P'111 queued d tdom prio prioa queuea) (set_tcb_queue d prio (tcb_sched_dequeue t queue)) (setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R108 queued d tdom prio prioa queue queuea) (?R'108 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_dequeue t queue) \<lbrace>\<lambda>x. ?R108 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'112 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea) \<lbrace>\<lambda>x. ?R'108 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P109 queued d tdom prio prioa queue and ?Q110 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'111 queued d tdom prio prioa queuea and ?Q'112 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?P109 True tdom tdom prioa prioa queuea) (?P'111 True tdom tdom prioa prioa queuea) (set_tcb_queue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea)) (setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea))
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R108 queued d tdom prio prioa queue queuea) (?R'108 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_dequeue t queue) \<lbrace>\<lambda>x. ?R108 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'112 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea) \<lbrace>\<lambda>x. ?R'108 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. ?P109 queued d tdom prio prioa queue and ?Q110 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. ?P'111 queued d tdom prio prioa queuea and ?Q'112 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R108 queued d tdom prio prioa queue queuea) (?R'108 queued d tdom prio prioa queue queuea) (return ()) (do y <- if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_dequeue t queue) \<lbrace>\<lambda>x. ?R108 queued d tdom prio prioa queue queuea\<rbrace>
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'112 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea) \<lbrace>\<lambda>x. ?R'108 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. queued) and ?Q110 queued d tdom prio prioa queue\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. (\<lambda>a. queued) and ?Q'112 queued d tdom prio prioa queuea\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 8. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
 10. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?P118 queued d tdom prio prioa queue queuea) (?P'118 queued d tdom prio prioa queue queuea) (return ()) (if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return ())
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R118 queued d tdom prio prioa queue queuea) (?R'118 queued d tdom prio prioa queue queuea) (return ()) (threadSet (tcbQueued_update (\<lambda>_. False)) t)
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'118 queued d tdom prio prioa queue queuea\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return () \<lbrace>\<lambda>x. ?R'118 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_dequeue t queue) \<lbrace>\<lambda>x. ?P118 queued d tdom prio prioa queue queuea and ?R118 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'112 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea) \<lbrace>\<lambda>x. ?P'118 queued d tdom prio prioa queue queuea and ?Q'118 queued d tdom prio prioa queue queuea\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. queued) and ?Q110 queued d tdom prio prioa queue\<rbrace>
 7. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. (\<lambda>a. queued) and ?Q'112 queued d tdom prio prioa queuea\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> corres dc (?R118 queued d tdom prio prioa queue queuea) (?R'118 queued d tdom prio prioa queue queuea) (return ()) (threadSet (tcbQueued_update (\<lambda>_. False)) t)
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'118 queued d tdom prio prioa queue queuea\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return () \<lbrace>\<lambda>x. ?R'118 queued d tdom prio prioa queue queuea\<rbrace>
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_dequeue t queue) \<lbrace>\<lambda>x. (\<lambda>a. queued) and ?R118 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'112 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea) \<lbrace>\<lambda>x. (\<lambda>a. queued) and ?Q'118 queued d tdom prio prioa queue queuea\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. queued) and ?Q110 queued d tdom prio prioa queue\<rbrace>
 6. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. (\<lambda>a. queued) and ?Q'112 queued d tdom prio prioa queuea\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'118 queued d tdom prio prioa queue queuea\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) queuea) then removeFromBitmap tdom prioa else return () \<lbrace>\<lambda>x. tcb_at' t\<rbrace>
 2. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 queued d tdom prio prioa queue\<rbrace> set_tcb_queue d prio (tcb_sched_dequeue t queue) \<lbrace>\<lambda>x. (\<lambda>a. queued) and (\<lambda>a. True)\<rbrace>
 3. \<And>queued d tdom prio prioa queue queuea. \<lbrakk>queued; d = tdom; prio = prioa; queue = queuea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'112 queued d tdom prio prioa queuea\<rbrace> setQueue tdom prioa (filter (\<lambda>x. x \<noteq> t) queuea) \<lbrace>\<lambda>x. (\<lambda>a. queued) and ?Q'118 queued d tdom prio prioa queue queuea\<rbrace>
 4. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 queued d tdom prio\<rbrace> get_tcb_queue d prio \<lbrace>\<lambda>queue. (\<lambda>a. queued) and ?Q110 queued d tdom prio prioa queue\<rbrace>
 5. \<And>queued d tdom prio prioa. \<lbrakk>queued; d = tdom; prio = prioa\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 queued d tdom prioa\<rbrace> getQueue tdom prioa \<lbrace>\<lambda>queuea. (\<lambda>a. queued) and ?Q'112 queued d tdom prio prioa queuea\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q87 queued d\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>a. queued) and ?Q100 queued d tdom prio\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'89 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prioa. (\<lambda>a. queued) and ?Q'102 queued d tdom prioa\<rbrace>
 8. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q78 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>d. is_etcb_at t and ?Q87 queued d\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'78 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom. tcb_at' t and ?Q'89 queued tdom\<rbrace>
 10. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q78 queued) s
A total of 11 subgoals... proof (prove)
goal:
No subgoals!