--- a/prio/Paper/Paper.thy	Tue Feb 14 02:55:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 14 03:26:18 2012 +0000
@@ -784,7 +784,7 @@
 
   \noindent
   Since @{text "th'"} is not able to run at state @{text "s' @ s"}, it is not able to 
-  issue a {text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
+  issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
   one step further, @{text "th'"} still cannot hold any resource. The situation will 
   not change in further extensions as long as @{text "th"} holds the highest precedence.
 
@@ -801,12 +801,29 @@
   @{term "cp (s' @ s) th' = prec th s"}.
   \end{theorem}
 
+  \noindent
   We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
   This theorem gives a stricter bound on the processes that can block @{text th}:
   only threads that were alive in state @{text s} and moreover held a resource.
   Finally, the theorem establishes that the blocking threads have the
   current precedence raised to the precedence of @{text th}.
 
+  We can furthermore prove that no deadlock exists in the state @{text "s' @ s"}
+  by showing that @{text "running (s' @ s)"} is not empty.
+
+  \begin{lemma}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"},
+  @{term "running (s' @ s) \<noteq> {}"}.
+  \end{lemma}
+
+  \begin{proof}
+  If @{text th} is blocked, then by following its dependants graph, we can always 
+  reach a ready thread @{text th'}, and that thread must have inherited the 
+  precedence of @{text th}.\qed
+  \end{proof}
+
+
   %The following lemmas show how every node in RAG can be chased to ready threads:
   %\begin{enumerate}
   %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):

Binary file prio/paper.pdf has changed