theory Move_C

lemma cancelIPC_st_tcb_at':
  "\<lbrace>\<lambda>s. t\<noteq>t' \<and> st_tcb_at' P t' s\<rbrace> cancelIPC t \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def locateSlot_conv) apply (wp sts_pred_tcb_neq' getEndpoint_wp cteDeleteOne_Reply getCTE_wp' | wpc)+ apply (rule hoare_strengthen_post [where Q="\<lambda>_. st_tcb_at' P t'"]) apply (wp threadSet_st_tcb_at2) apply simp apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def) apply (wp cancelSignal_st_tcb' sts_pred_tcb_neq' getEndpoint_wp gts_wp' | wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> t' \<and> st_tcb_at' P t' s\<rbrace> cancelIPC t \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> t' \<and> st_tcb_at' P t' s\<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;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE (t + 2 ^ cte_level_bits * tcbReplySlot));
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>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>y s. \<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> ((\<lambda>callerCap. if callerCap \<noteq> nullPointer then \<lambda>s. capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> (st_tcb_at' P t' and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap) s else st_tcb_at' P t') \<circ> (mdbNext \<circ> cteMDBNode)) cte s\<rbrace>
 2. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 3. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P 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>_. st_tcb_at' P t'\<rbrace>
 7. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject state) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) 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>
 9. \<And>s. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> ?Q2 s proof (prove)
goal (10 subgoals):
 1. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 2. \<And>state rv s. \<lbrakk>awaiting_reply' state; st_tcb_at' P t' s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> ((\<lambda>callerCap. if callerCap \<noteq> nullPointer then \<lambda>s. capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> (st_tcb_at' P t' and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap) s else st_tcb_at' P t') \<circ> (mdbNext \<circ> cteMDBNode)) cte s
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P 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>_. st_tcb_at' P t'\<rbrace>
 8. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject state) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) 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. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> ?Q2 s proof (prove)
goal (10 subgoals):
 1. \<And>state. awaiting_reply' state \<Longrightarrow> \<forall>tcb. P (tcbState tcb) \<longrightarrow> P (tcbState (tcbFault_update (\<lambda>_. None) tcb))
 2. \<And>state rv s. \<lbrakk>awaiting_reply' state; st_tcb_at' P t' s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> ((\<lambda>callerCap. if callerCap \<noteq> nullPointer then \<lambda>s. capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> (st_tcb_at' P t' and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap) s else st_tcb_at' P t') \<circ> (mdbNext \<circ> cteMDBNode)) cte s
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P 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>_. st_tcb_at' P t'\<rbrace>
 8. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject state) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s))) \<and> (awaiting_reply' state \<longrightarrow> st_tcb_at' P t' 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. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>state rv s. \<lbrakk>awaiting_reply' state; st_tcb_at' P t' s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> ((\<lambda>callerCap. if callerCap \<noteq> nullPointer then \<lambda>s. capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> (st_tcb_at' P t' and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap) s else st_tcb_at' P t') \<circ> (mdbNext \<circ> cteMDBNode)) cte s
 2. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 3. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P 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>_. st_tcb_at' P t'\<rbrace>
 7. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject state) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s))) \<and> (awaiting_reply' state \<longrightarrow> st_tcb_at' P t' 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>
 9. \<And>s. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> ?Q2 s proof (prove)
goal (8 subgoals):
 1. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 2. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 3. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 4. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 5. \<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>_. st_tcb_at' P t'\<rbrace>
 6. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 7. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject state) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s))) \<and> (awaiting_reply' state \<longrightarrow> st_tcb_at' P t' 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>
 8. \<And>s. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> \<forall>st. st_tcb_at' ((=) st) t s \<longrightarrow> (\<forall>x xa. st = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject st) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s))) \<and> (awaiting_reply' st \<longrightarrow> st_tcb_at' P t' s) \<and> (\<forall>x. st = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> t \<noteq> t' \<and> st_tcb_at' P t' s) \<and> (st = Structures_H.thread_state.Running \<longrightarrow> st_tcb_at' P t' s) \<and> (st = Structures_H.thread_state.Inactive \<longrightarrow> st_tcb_at' P t' s) \<and> (idle' st \<longrightarrow> st_tcb_at' P t' s) \<and> (\<forall>x xa xb xc xd. st = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> (\<forall>ep. ko_at' ep (blockingObject st) s \<longrightarrow> \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (epQueue ep) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s))) \<and> (st = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' P t' s) proof (prove)
goal:
No subgoals!