545   @{thm holdents_def}\\

   545   @{thm holdents_def}\\

   546   @{thm detached_def}

   546   @{thm detached_def}

   547   \end{tabular}

   547   \end{tabular}

   548   \end{isabelle}

   548   \end{isabelle}

   549 

   549 

   552   

   552   

   553   Finally we can define what a \emph{valid state} is in our model of PIP. For

   553   Finally we can define what a \emph{valid state} is in our model of PIP. For

   554   example we cannot expect to be able to exit a thread, if it was not

   554   example we cannot expect to be able to exit a thread, if it was not

   555   created yet. 

   555   created yet. 

   556   These validity constraints on states are characterised by the

   556   These validity constraints on states are characterised by the