theory Ipc_R

lemma cancelIPC_ResumeCurrentThread_imp_notct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
   cancelIPC t
   \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>"
  (is "\<lbrace>?PRE t'\<rbrace> _ \<lbrace>_\<rbrace>") proof - have aipc: "\<And>t t' ntfn.
    \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
    cancelSignal t ntfn
    \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>" apply (simp add: cancelSignal_def) apply (wp)[1] apply (wp hoare_convert_imp)+ apply (rule_tac P="\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread"
                 in hoare_weaken_pre) apply (wpc) apply (wp | simp)+ apply (wpc, wp+) apply (rule_tac Q="\<lambda>_. ?PRE t'" in hoare_post_imp, clarsimp) apply (wp) apply simp done have cdo: "\<And>t t' slot.
    \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
    cteDeleteOne slot
    \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>" apply (simp add: cteDeleteOne_def unless_def split_def) apply (wp) apply (wp hoare_convert_imp)[1] apply (wp) apply (rule_tac Q="\<lambda>_. ?PRE t'" in hoare_post_imp, clarsimp) apply (wp hoare_convert_imp | simp)+ done show ?thesis apply (simp add: cancelIPC_def Let_def) apply (wp, wpc) prefer 4 \<comment> \<open>state = Running\<close> apply wp prefer 7 \<comment> \<open>state = Restart\<close> apply wp apply (wp)+ apply (wp hoare_convert_imp)[1] apply (wpc, wp+) apply (rule_tac Q="\<lambda>_. ?PRE t'" in hoare_post_imp, clarsimp) apply (wp cdo)+ apply (rule_tac Q="\<lambda>_. ?PRE t'" in hoare_post_imp, clarsimp) apply ((wp aipc hoare_convert_imp)+)[6] apply (wp) apply (wp hoare_convert_imp)[1] apply (wpc, wp+) apply (rule_tac Q="\<lambda>_. ?PRE t'" in hoare_post_imp, clarsimp) apply (wp) apply (rule_tac Q="\<lambda>_. ?PRE t'" in hoare_post_imp, clarsimp) apply (wp) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t t' ntfn. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t t' ntfn. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>t t' ntfn ntfna y ntfn'. \<lbrace>?B4 t t' ntfn ntfna y ntfn'\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna) \<lbrace>\<lambda>ya s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>t t' ntfn ntfna y. \<lbrace>?B3 t t' ntfn ntfna y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>?B4 t t' ntfn ntfna y\<rbrace>
 3. \<And>t t' ntfn ntfna. \<lbrace>?B2 t t' ntfn ntfna\<rbrace> assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>?B3 t t' ntfn ntfna\<rbrace>
 4. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>?B2 t t' ntfn\<rbrace>
 5. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (5 subgoals):
 1. \<And>t t' ntfn ntfna y. \<lbrace>\<lambda>s. \<not> ?P14 t t' ntfn ntfna y s\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>ntfn' s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>t t' ntfn ntfna y. \<lbrace>?R14 t t' ntfn ntfna y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>rv s. ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>t t' ntfn ntfna. \<lbrace>?B2 t t' ntfn ntfna\<rbrace> assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>\<lambda>y s. ?P14 t t' ntfn ntfna y s \<longrightarrow> ?R14 t t' ntfn ntfna y s\<rbrace>
 4. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>?B2 t t' ntfn\<rbrace>
 5. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (6 subgoals):
 1. \<And>t t' ntfn ntfna y. \<lbrace>?Q16 t t' ntfn ntfna y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>ntfn' s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>t t' ntfn ntfna y s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q16 t t' ntfn ntfna y s
 3. \<And>t t' ntfn ntfna y. \<lbrace>?R14 t t' ntfn ntfna y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>rv s. ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>t t' ntfn ntfna. \<lbrace>?B2 t t' ntfn ntfna\<rbrace> assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>\<lambda>y s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R14 t t' ntfn ntfna y s\<rbrace>
 5. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>?B2 t t' ntfn\<rbrace>
 6. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (7 subgoals):
 1. \<And>t t' ntfn ntfna y. remove1 t (ntfnQueue (ntfnObj ntfna)) = [] \<Longrightarrow> \<lbrace>?R27 t t' ntfn ntfna y\<rbrace> return $ Structures_H.ntfn.IdleNtfn \<lbrace>\<lambda>ntfn' s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>t t' ntfn ntfna y x21 x22. remove1 t (ntfnQueue (ntfnObj ntfna)) = x21 # x22 \<Longrightarrow> \<lbrace>?R28 t t' ntfn ntfna y x21 x22\<rbrace> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>ntfn' s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 3. \<And>t t' ntfn ntfna y s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> (remove1 t (ntfnQueue (ntfnObj ntfna)) = [] \<longrightarrow> ?R27 t t' ntfn ntfna y s) \<and> (\<forall>x xa. remove1 t (ntfnQueue (ntfnObj ntfna)) = x # xa \<longrightarrow> ?R28 t t' ntfn ntfna y x xa s)
 4. \<And>t t' ntfn ntfna y. \<lbrace>?R14 t t' ntfn ntfna y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>rv s. ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>t t' ntfn ntfna. \<lbrace>?B2 t t' ntfn ntfna\<rbrace> assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>\<lambda>y s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R14 t t' ntfn ntfna y s\<rbrace>
 6. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>?B2 t t' ntfn\<rbrace>
 7. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (4 subgoals):
 1. \<And>t t' ntfn ntfna. \<lbrace>?R14 t t' ntfn ntfna ()\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna) \<lbrace>\<lambda>rv s. ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>t t' ntfn ntfna. \<lbrace>?B2 t t' ntfn ntfna\<rbrace> assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>\<lambda>y s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R14 t t' ntfn ntfna y s\<rbrace>
 3. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>?B2 t t' ntfn\<rbrace>
 4. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (2 subgoals):
 1. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna s. (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (remove1 t (ntfnQueue (ntfnObj ntfna)) = [] \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa. remove1 t (ntfnQueue (ntfnObj ntfna)) = x # xa \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 2. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (2 subgoals):
 1. \<And>t t' ntfn. \<lbrace>?Q1 t t' ntfn\<rbrace> getNotification ntfn \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> ksCurThread a \<noteq> t'\<rbrace>
 2. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q1 t t' ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>t t' ntfn s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> ?t'\<rbrace> cancelSignal ?t ?ntfn \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> ?t'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t t' slot. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t' slot. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>t' slot cte final p y. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B5 t' slot cte final p y\<rbrace> emptySlot slot capability.NullCap \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>t' slot cte final p. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B4 t' slot cte final p\<rbrace> assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap) \<lbrace>?B5 t' slot cte final p\<rbrace>
 3. \<And>t' slot cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B3 t' slot cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>?B4 t' slot cte final\<rbrace>
 4. \<And>t' slot cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 t' slot cte\<rbrace> isFinalCapability cte \<lbrace>?B3 t' slot cte\<rbrace>
 5. \<And>t' slot. \<lbrace>?Q t' slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 t' slot cte else (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 6. \<And>t' slot s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q t' slot s proof (prove)
goal (5 subgoals):
 1. \<And>t' slot cte final p. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B4 t' slot cte final p\<rbrace> assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap) \<lbrace>\<lambda>y s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>t' slot cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B3 t' slot cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>?B4 t' slot cte final\<rbrace>
 3. \<And>t' slot cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 t' slot cte\<rbrace> isFinalCapability cte \<lbrace>?B3 t' slot cte\<rbrace>
 4. \<And>t' slot. \<lbrace>?Q t' slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 t' slot cte else (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 5. \<And>t' slot s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q t' slot s proof (prove)
goal (4 subgoals):
 1. \<And>t' slot cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B3 t' slot cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>\<lambda>p s. capRemovable (fst p) slot \<and> snd p = capability.NullCap \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>t' slot cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 t' slot cte\<rbrace> isFinalCapability cte \<lbrace>?B3 t' slot cte\<rbrace>
 3. \<And>t' slot. \<lbrace>?Q t' slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 t' slot cte else (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 4. \<And>t' slot s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q t' slot s proof (prove)
goal (4 subgoals):
 1. \<And>t' slot cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B3 t' slot cte final\<rbrace> finaliseCapTrue_standin (cteCap cte) final \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> ksCurThread a \<noteq> t'\<rbrace>
 2. \<And>t' slot cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 t' slot cte\<rbrace> isFinalCapability cte \<lbrace>?B3 t' slot cte\<rbrace>
 3. \<And>t' slot. \<lbrace>?Q t' slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 t' slot cte else (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 4. \<And>t' slot s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q t' slot s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> ?t'\<rbrace> cteDeleteOne ?slot \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> ?t'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R23 state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R14 state s)\<rbrace>
 10. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (10 subgoals):
 1. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R23 state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R14 state s)\<rbrace>
 10. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R14 state s)\<rbrace>
 9. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R14 state s)\<rbrace>
 9. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (8 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 8. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (11 subgoals):
 1. \<And>state x11 x12 ep y ep'. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?B47 state x11 x12 ep y ep'\<rbrace> setEndpoint (blockingObject state) ep' \<lbrace>\<lambda>ya s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state x11 x12 ep y. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?B46 state x11 x12 ep y\<rbrace> case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep \<lbrace>?B47 state x11 x12 ep y\<rbrace>
 3. \<And>state x11 x12 ep. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?B45 state x11 x12 ep\<rbrace> assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False)) \<lbrace>?B46 state x11 x12 ep\<rbrace>
 4. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> getEndpoint (blockingObject state) \<lbrace>?B45 state x11 x12\<rbrace>
 5. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 9. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 10. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state x11 x12 ep y. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?B46 state x11 x12 ep y\<rbrace> case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep \<lbrace>\<lambda>ep' s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state x11 x12 ep. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?B45 state x11 x12 ep\<rbrace> assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False)) \<lbrace>?B46 state x11 x12 ep\<rbrace>
 3. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> getEndpoint (blockingObject state) \<lbrace>?B45 state x11 x12\<rbrace>
 4. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 10. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (8 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> getEndpoint (blockingObject state) \<lbrace>\<lambda>ep s. \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 2. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 8. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (8 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R29 state x11 x12\<rbrace> getEndpoint (blockingObject state) \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> ksCurThread a \<noteq> t'\<rbrace>
 2. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R29 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 8. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>state y slot. awaiting_reply' state \<Longrightarrow> \<lbrace>?B85 state y slot\<rbrace> getCTE slot \<lbrace>(\<lambda>callerCap. if callerCap \<noteq> nullPointer then \<lambda>s. capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' else (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')) \<circ> (mdbNext \<circ> cteMDBNode)\<rbrace>
 2. \<And>state y. awaiting_reply' state \<Longrightarrow> \<lbrace>?B84 state y\<rbrace> getThreadReplySlot t \<lbrace>?B85 state y\<rbrace>
 3. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B84 state\<rbrace>
 4. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 9. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>state y slot. awaiting_reply' state \<Longrightarrow> \<lbrace>?B85 state y slot\<rbrace> getCTE slot \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> ksCurThread a \<noteq> t'\<rbrace>
 2. \<And>state y. awaiting_reply' state \<Longrightarrow> \<lbrace>?B84 state y\<rbrace> getThreadReplySlot t \<lbrace>?B85 state y\<rbrace>
 3. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B84 state\<rbrace>
 4. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 9. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (idle' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 3. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (6 subgoals):
 1. \<And>state x71 x72 x73 x74 x75 ep y ep'. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?B130 state x71 x72 x73 x74 x75 ep y ep'\<rbrace> setEndpoint (blockingObject state) ep' \<lbrace>\<lambda>ya s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state x71 x72 x73 x74 x75 ep y. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?B129 state x71 x72 x73 x74 x75 ep y\<rbrace> case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep \<lbrace>?B130 state x71 x72 x73 x74 x75 ep y\<rbrace>
 3. \<And>state x71 x72 x73 x74 x75 ep. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?B128 state x71 x72 x73 x74 x75 ep\<rbrace> assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False)) \<lbrace>?B129 state x71 x72 x73 x74 x75 ep\<rbrace>
 4. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> getEndpoint (blockingObject state) \<lbrace>?B128 state x71 x72 x73 x74 x75\<rbrace>
 5. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (idle' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 6. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>state x71 x72 x73 x74 x75 ep y. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?B129 state x71 x72 x73 x74 x75 ep y\<rbrace> case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep \<lbrace>\<lambda>ep' s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
 2. \<And>state x71 x72 x73 x74 x75 ep. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?B128 state x71 x72 x73 x74 x75 ep\<rbrace> assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False)) \<lbrace>?B129 state x71 x72 x73 x74 x75 ep\<rbrace>
 3. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> getEndpoint (blockingObject state) \<lbrace>?B128 state x71 x72 x73 x74 x75\<rbrace>
 4. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (idle' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 5. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> getEndpoint (blockingObject state) \<lbrace>\<lambda>ep s. \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 2. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (idle' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 3. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 state x71 x72 x73 x74 x75\<rbrace> getEndpoint (blockingObject state) \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> ksCurThread a \<noteq> t'\<rbrace>
 2. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (idle' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 3. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (awaiting_reply' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (idle' state \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t') \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t')\<rbrace>
 2. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> ksCurThread a \<noteq> t'\<rbrace>
 2. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t' proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>

goal:
No subgoals!