theory IpcCancel_R

lemma tcbSchedDequeue_corres':
  "corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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 valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"]) defer apply (wp threadGet_obj_at', simp, simp) apply (wp, simp) apply (case_tac queued) defer apply (simp add: unless_def when_def) apply (rule corres_no_failI) apply (wp) apply (clarsimp simp: in_monad ethread_get_def get_etcb_def set_tcb_queue_def is_etcb_at_def state_relation_def gets_the_def gets_def get_def return_def bind_def assert_opt_def get_tcb_queue_def modify_def put_def) apply (subgoal_tac "t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))") prefer 2 apply (force simp: tcb_sched_dequeue_def valid_inQ_queues_def
           ready_queues_relation_def obj_at'_def inQ_def projectKO_eq project_inject) apply (simp add: ready_queues_relation_def) apply (simp add: unless_def when_def) apply (rule corres_guard_imp) apply (rule corres_split[where r'="(=)"]) apply (rule ethreadget_corres, simp add: etcb_relation_def) apply (simp split del: if_split) apply (rule corres_split_eqr) apply (rule ethreadget_corres, simp add: etcb_relation_def) apply (rule corres_split_eqr[OF getQueue_corres]) apply (simp split del: if_split) apply (subst bind_return_unit, rule corres_split[where r'=dc]) apply (simp add: tcb_sched_dequeue_def) apply (rule setQueue_corres) apply (rule corres_split_noop_rhs) apply (clarsimp, rule removeFromBitmap_corres_noop) apply (simp add: dc_def[symmetric]) apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1] apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_queues\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. tcb_at' t and valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace>
 3. True \<Longrightarrow> no_fail (tcb_at' t and valid_inQ_queues) (threadGet tcbQueued t) proof (prove)
goal (3 subgoals):
 1. \<lbrace>tcb_at' t and valid_inQ_queues\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. tcb_at' t and valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace>
 2. True \<Longrightarrow> no_fail (tcb_at' t and valid_inQ_queues) (threadGet tcbQueued t)
 3. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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 valid_inQ_queues) (threadGet tcbQueued t)
 2. \<And>queued. corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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 valid_inQ_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; valid_inQ_queues b; obj_at' (\<lambda>obj. \<not> tcbQueued obj) t b\<rbrakk> \<Longrightarrow> ready_queues_relation (\<lambda>d' p. if d' = tcb_domain y \<and> p = tcb_priority y then tcb_sched_dequeue t (ready_queues a (tcb_domain y) (tcb_priority y)) else ready_queues a d' p) (ksReadyQueues b)
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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; valid_inQ_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> ready_queues_relation (\<lambda>d' p. if d' = tcb_domain y \<and> p = tcb_priority y then tcb_sched_dequeue t (ready_queues a (tcb_domain y) (tcb_priority y)) else ready_queues a d' p) (ksReadyQueues 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; valid_inQ_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 valid_inQ_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; valid_inQ_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; valid_inQ_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> ready_queues_relation (\<lambda>d' p. if d' = tcb_domain y \<and> p = tcb_priority y then tcb_sched_dequeue t (ready_queues a (tcb_domain y) (tcb_priority y)) else ready_queues a d' p) (ksReadyQueues b)
 3. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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; valid_inQ_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> ready_queues_relation (\<lambda>d' p. if d' = tcb_domain y \<and> p = tcb_priority y then tcb_sched_dequeue t (ready_queues a (tcb_domain y) (tcb_priority y)) else ready_queues a d' p) (ksReadyQueues b)
 2. \<And>queued. queued \<Longrightarrow> corres dc (is_etcb_at t) (tcb_at' t and valid_inQ_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 valid_inQ_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 valid_inQ_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 (?Q151 queued) (?Q'151 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> ?Q151 queued s
 3. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q'151 queued s proof (prove)
goal (6 subgoals):
 1. \<And>queued. queued \<Longrightarrow> corres (=) (?P155 queued) (?P'155 queued) (ethread_get tcb_domain t) (threadGet tcbDomain t)
 2. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R155 queued d) (?R'155 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>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R155 queued\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'155 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (?P155 queued and ?Q155 queued) s
 6. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (?P'155 queued and ?Q'155 queued) s proof (prove)
goal (5 subgoals):
 1. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R155 queued d) (?R'155 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>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R155 queued\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'155 queued\<rbrace>
 4. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
 5. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'155 queued) s proof (prove)
goal (5 subgoals):
 1. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R155 True tdom) (?R'155 True tdom) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue tdom prio;
set_tcb_queue tdom 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>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>?R155 queued\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>?R'155 queued\<rbrace>
 4. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
 5. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'155 queued) s proof (prove)
goal (8 subgoals):
 1. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres (=) (?P173 True tdom) (?P'169 True tdom) (ethread_get tcb_priority t) (threadGet tcbPriority t)
 2. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R162 queued d tdom prio) (?R'162 queued d tdom prio) (do queue <- get_tcb_queue tdom prio;
set_tcb_queue tdom prio (tcb_sched_dequeue t queue)
od) (do 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 d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>?R162 queued d tdom\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'162 queued d tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. ?P173 queued a and ?Q171 queued a\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. ?P'169 queued a and ?Q'167 queued a\<rbrace>
 7. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
 8. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'155 queued) s proof (prove)
goal (7 subgoals):
 1. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R162 queued d tdom prio) (?R'162 queued d tdom prio) (do queue <- get_tcb_queue tdom prio;
set_tcb_queue tdom prio (tcb_sched_dequeue t queue)
od) (do 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 d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>?R162 queued d tdom\<rbrace>
 3. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>?R'162 queued d tdom\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
 6. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
 7. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'155 queued) s proof (prove)
goal (9 subgoals):
 1. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R181 queued d tdom prio rv) (?R'181 queued d tdom prio rv) (set_tcb_queue tdom prio (tcb_sched_dequeue t rv)) (do y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv);
y <- if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>?R181 queued d tdom prio\<rbrace>
 3. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>?R'181 queued d tdom prio\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 7. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
 8. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
 9. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'155 queued) s proof (prove)
goal (9 subgoals):
 1. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R181 True tdom tdom prio rv) (?R'181 True tdom tdom prio rv) (set_tcb_queue tdom prio (tcb_sched_dequeue t rv)) (do y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv);
y <- if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>?R181 queued d tdom prio\<rbrace>
 3. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>?R'181 queued d tdom prio\<rbrace>
 4. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 5. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 7. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
 8. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
 9. \<And>queued s. \<lbrakk>queued; (tcb_at' t and valid_inQ_queues and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'155 queued) s proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?P208 tdom prio rv True tdom tdom prio rv) (?P'202 tdom prio rv True tdom tdom prio rv) (set_tcb_queue tdom prio (tcb_sched_dequeue t rv)) (setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv))
 2. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R191 queued d tdom prio rv x) (?R'191 queued d tdom prio rv y) (return ()) (do y <- if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>?R191 queued d tdom prio rv\<rbrace>
 4. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>?R'191 queued d tdom prio rv\<rbrace>
 5. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. ?P211 queued d tdom prio a and ?Q210 queued d tdom prio a\<rbrace>
 6. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. ?P'205 queued d tdom prio a and ?Q'204 queued d tdom prio a\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
A total of 12 subgoals...
flex-flex pairs:
\<lambda>tdom. ?P211 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?P208 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?P'205 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?P'202 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?P208 tdom prio rv True tdom tdom prio rv) (?P'202 tdom prio rv True tdom tdom prio rv) (set_tcb_queue tdom prio (filter (\<lambda>x. x \<noteq> t) rv)) (setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv))
 2. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R191 queued d tdom prio rv x) (?R'191 queued d tdom prio rv y) (return ()) (do y <- if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 3. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>?R191 queued d tdom prio rv\<rbrace>
 4. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>?R'191 queued d tdom prio rv\<rbrace>
 5. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. ?P211 queued d tdom prio a and ?Q210 queued d tdom prio a\<rbrace>
 6. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. ?P'205 queued d tdom prio a and ?Q'204 queued d tdom prio a\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
A total of 12 subgoals...
flex-flex pairs:
\<lambda>tdom. ?P211 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?P208 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?P'205 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?P'202 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal (11 subgoals):
 1. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R191 queued d tdom prio rv x) (?R'191 queued d tdom prio rv y) (return ()) (do y <- if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
 2. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>?R191 queued d tdom prio rv\<rbrace>
 3. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>?R'191 queued d tdom prio rv\<rbrace>
 4. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q210 queued d tdom prio a\<rbrace>
 5. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'204 queued d tdom prio a\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 8. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
 10. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
A total of 11 subgoals...
flex-flex pairs:
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal (13 subgoals):
 1. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> corres dc (?P229 queued d tdom prio rv x) (?P'225 queued d tdom prio rv y) (return ()) (if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return ())
 2. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R227 queued d tdom prio rv x) (?R'217 queued d tdom prio rv x y) (return ()) (threadSet (tcbQueued_update (\<lambda>_. False)) t)
 3. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 queued d tdom prio rv y\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return () \<lbrace>\<lambda>xa. ?R'217 queued d tdom prio rv x y\<rbrace>
 4. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>\<lambda>a. ?P229 queued d tdom prio rv a and ?R227 queued d tdom prio rv a\<rbrace>
 5. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>\<lambda>a. ?P'225 queued d tdom prio rv a and ?Q'223 queued d tdom prio rv a\<rbrace>
 6. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q210 queued d tdom prio a\<rbrace>
 7. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'204 queued d tdom prio a\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 9. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
A total of 13 subgoals...
flex-flex pairs:
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R227 queued d tdom prio rv x) (?R'217 queued d tdom prio rv x y) (return ()) (threadSet (tcbQueued_update (\<lambda>_. False)) t)
 2. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 queued d tdom prio rv y\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return () \<lbrace>\<lambda>xa. ?R'217 queued d tdom prio rv x y\<rbrace>
 3. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?R227 queued d tdom prio rv a\<rbrace>
 4. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'223 queued d tdom prio rv a\<rbrace>
 5. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q210 queued d tdom prio a\<rbrace>
 6. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'204 queued d tdom prio a\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
A total of 12 subgoals...
flex-flex pairs:
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal (12 subgoals):
 1. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> corres dc (?R227 True tdom tdom prio rv ()) (?R'217 True tdom tdom prio rv () ()) (return ()) (threadSet (tcbQueued_update (\<lambda>_. False)) t)
 2. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 queued d tdom prio rv y\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return () \<lbrace>\<lambda>xa. ?R'217 queued d tdom prio rv x y\<rbrace>
 3. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?R227 queued d tdom prio rv a\<rbrace>
 4. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'223 queued d tdom prio rv a\<rbrace>
 5. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q210 queued d tdom prio a\<rbrace>
 6. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'204 queued d tdom prio a\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 8. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 10. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
A total of 12 subgoals...
flex-flex pairs:
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal (11 subgoals):
 1. \<And>queued d tdom prio rv x y. \<lbrakk>queued; d = tdom; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'223 queued d tdom prio rv y\<rbrace> if null (filter (\<lambda>x. x \<noteq> t) rv) then removeFromBitmap tdom prio else return () \<lbrace>\<lambda>x. obj_at' (\<lambda>x. queued) t\<rbrace>
 2. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 tdom prio rv True tdom tdom prio rv\<rbrace> set_tcb_queue tdom prio (tcb_sched_dequeue t rv) \<lbrace>\<lambda>a. (\<lambda>a. queued) and (\<lambda>a. queued)\<rbrace>
 3. \<And>queued d tdom prio rv. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 tdom prio rv True tdom tdom prio rv\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) rv) \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'223 queued d tdom prio rv a\<rbrace>
 4. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 queued d tdom prio\<rbrace> get_tcb_queue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q210 queued d tdom prio a\<rbrace>
 5. \<And>queued d tdom prio. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'181 queued d tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a. (\<lambda>a. queued) and ?Q'204 queued d tdom prio a\<rbrace>
 6. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 True tdom\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q181 queued d tdom prio\<rbrace>
 7. \<And>queued d tdom. \<lbrakk>queued; d = tdom\<rbrakk> \<Longrightarrow> \<lbrace>?Q'167 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio. (\<lambda>_. True) and ?Q'181 queued d tdom prio\<rbrace>
 8. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q155 queued\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>a. is_etcb_at t and ?Q171 queued a\<rbrace>
 9. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q'155 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a. obj_at' (\<lambda>x. queued) t and ?Q'167 queued a\<rbrace>
 10. \<And>queued s. \<lbrakk>queued; is_etcb_at t s\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q155 queued) s
A total of 11 subgoals...
flex-flex pairs:
\<lambda>tdom. ?Q210 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q206 tdom prio rv True tdom tdom prio rv
\<lambda>tdom. ?Q'204 True tdom tdom \<equiv>\<^sup>? \<lambda>tdom prio rv. ?Q'200 tdom prio rv True tdom tdom prio rv proof (prove)
goal:
No subgoals!