theory Orphanage

lemma tcbSchedDequeue_not_empty:
  "\<lbrace> \<lambda>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<rbrace>
   tcbSchedDequeue thread
   \<lbrace> \<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s \<rbrace>" unfolding tcbSchedDequeue_def apply wp apply (wp hoare_vcg_ex_lift threadSet_pred_tcb_no_state) apply clarsimp apply (wp setQueue_deq_not_empty) apply clarsimp apply (rule hoare_pre_post, assumption) apply (clarsimp simp: bitmap_fun_defs) apply wp apply clarsimp apply clarsimp apply (wp setQueue_deq_not_empty)+ apply (rule_tac Q="\<lambda>rv s. \<not> st_tcb_at' P thread s" in hoare_post_imp) apply fastforce apply (wp weak_if_wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s\<rbrace> do queued <- threadGet tcbQueued thread;
when queued $ do tdom <- threadGet tcbDomain thread;
prio <- threadGet tcbPriority thread;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> thread) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) thread
od
od \<lbrace>\<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue queue' x xa. queued \<Longrightarrow> \<lbrace>?B10 queued tdom prio queue queue' x xa\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) thread \<lbrace>\<lambda>rv s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s\<rbrace>
 2. \<And>queued tdom prio queue queue' x. queued \<Longrightarrow> \<lbrace>?B8 queued tdom prio queue queue' x\<rbrace> when (null queue') $ removeFromBitmap tdom prio \<lbrace>?B10 queued tdom prio queue queue' x\<rbrace>
 3. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>?B8 queued tdom prio queue queue'\<rbrace>
 4. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 5. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 6. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 7. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 9. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue queue' x xa tcb tcba. queued \<Longrightarrow> itcbState (tcb_to_itcb' (tcbQueued_update (\<lambda>_. False) tcba)) = itcbState (tcb_to_itcb' tcba)
 2. \<And>queued tdom prio queue queue' x. queued \<Longrightarrow> \<lbrace>?B8 queued tdom prio queue queue' x\<rbrace> when (null queue') $ removeFromBitmap tdom prio \<lbrace>\<lambda>xa s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s\<rbrace>
 3. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>?B8 queued tdom prio queue queue'\<rbrace>
 4. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 5. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 6. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 7. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 9. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue queue' x. queued \<Longrightarrow> \<lbrace>?B8 queued tdom prio queue queue' x\<rbrace> when (null queue') $ removeFromBitmap tdom prio \<lbrace>\<lambda>xa s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>?B8 queued tdom prio queue queue'\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 8. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue queue' x. \<lbrakk>queued; null queue'\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 queued tdom prio queue queue' x\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>xa s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then ?Q21 queued tdom prio queue queue' x else (\<lambda>s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s)\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 8. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue queue'. \<lbrakk>queued; null queue'\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 True tdom prio queue queue' ()\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>xa s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then ?Q21 queued tdom prio queue queue' x else (\<lambda>s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s)\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 8. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue queue'. \<lbrakk>queued; null queue'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>xa a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a else (\<lambda>s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s)\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 8. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue'. \<lbrakk>queued; null queue'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a\<rbrace> do y <- do l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (tdom, invertL1Index (prioToL1Index prio)));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap ks)((tdom, invertL1Index (prioToL1Index prio)) := l2 && ~~ 2 ^ unat (prio && mask wordRadix))\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (tdom, invertL1Index (prioToL1Index prio)));
when (l2 = 0) (do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks tdom);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap ks)(tdom := l1 && ~~ 2 ^ prioToL1Index prio)\<rparr>)
od)
od \<lbrace>\<lambda>xa a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a else (\<lambda>s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s)\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 8. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue' s. \<lbrakk>queued; null queue'; \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s\<rbrakk> \<Longrightarrow> (if ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap s)((tdom, invertL1Index (prioToL1Index prio)) := ksReadyQueuesL2Bitmap s (tdom, invertL1Index (prioToL1Index prio)) && ~~ 2 ^ unat (prio && mask wordRadix))\<rparr>) (tdom, invertL1Index (prioToL1Index prio)) = 0 then \<lambda>s. \<exists>x. x \<in> set (ksReadyQueues (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom && ~~ 2 ^ prioToL1Index prio)\<rparr>) p) \<and> st_tcb_at' P x (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom && ~~ 2 ^ prioToL1Index prio)\<rparr>) else (\<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a)) (s\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap s)((tdom, invertL1Index (prioToL1Index prio)) := ksReadyQueuesL2Bitmap s (tdom, invertL1Index (prioToL1Index prio)) && ~~ 2 ^ unat (prio && mask wordRadix))\<rparr>)
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a else (\<lambda>s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s)\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 8. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a else (\<lambda>s. \<exists>x. x \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P x s)\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 7. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 True tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x a. \<exists>x. x \<in> set (ksReadyQueues a p) \<and> st_tcb_at' P x a\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> thread) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>?B5 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>?B4 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 7. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?P'56 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>\<lambda>rv s. \<exists>tcb_ptr. \<not> st_tcb_at' P tcb_ptr s \<and> filter (\<lambda>x. x \<noteq> thread) (ksReadyQueues s (tdom, rv)) = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (tdom, rv))\<rbrace>
 2. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>\<lambda>tdom s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> ?P'56 queued tdom s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 4. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom rv s. \<lbrakk>queued; \<not> st_tcb_at' P thread s\<rbrakk> \<Longrightarrow> \<exists>tcb_ptr. \<not> st_tcb_at' P tcb_ptr s \<and> filter (\<lambda>x. x \<noteq> thread) (ksReadyQueues s (tdom, rv)) = filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (tdom, rv))
 2. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?P'56 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>\<lambda>rv s. \<not> st_tcb_at' P thread s\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>\<lambda>tdom s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> ?P'56 queued tdom s\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 5. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?P'56 queued tdom\<rbrace> threadGet tcbPriority thread \<lbrace>\<lambda>rv s. \<not> st_tcb_at' P thread s\<rbrace>
 2. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain thread \<lbrace>\<lambda>tdom s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> ?P'56 queued tdom s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then ?Q3 queued else (\<lambda>s. \<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s)\<rbrace>
 4. \<And>s. (\<exists>tcb. tcb \<in> set (ksReadyQueues s p) \<and> st_tcb_at' P tcb s) \<and> \<not> st_tcb_at' P thread s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!