--- a/Implementation.thy	Thu Jun 29 14:59:55 2017 +0100
+++ b/Implementation.thy	Thu Jun 29 15:31:24 2017 +0100
@@ -70,7 +70,7 @@
 *}
 
 lemma cp_rec_tG:
-  "cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)"
+  "cp s th = Max ({preced th s} \<union> cprecs (children (tG s) th) s)"
 proof -
   have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp)
   have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = 

--- a/Journal/Paper.thy	Thu Jun 29 14:59:55 2017 +0100
+++ b/Journal/Paper.thy	Thu Jun 29 15:31:24 2017 +0100
@@ -593,7 +593,8 @@
   @{thm children_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
   @{thm subtree_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
   @{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
-  \end{tabular}
+  \end{tabular}\\
+  \mbox{}\hfill\numbered{children}
   \end{isabelle}
   
   \noindent Note that forrests can have trees with infinte depth and
@@ -1825,45 +1826,32 @@
   For example Baker complained that calculating the current precedence
   in PIP is quite ``heavy weight'' in Linux (see the Introduction).
   In our model of PIP the current precedence of a thread in a state @{text s}
-  depends on all its dependants---a ``global'' transitive notion,
-  which is indeed heavy weight (see Definition shown in \eqref{cpreced}).
-  We can however improve upon this. For this let us define the notion
-  of @{term children} of a thread @{text th} in a state @{text s} as
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  ?? @{thm children_def}
-  \end{tabular}
-  \end{isabelle}
-
-  \noindent
+  depends on the precedenes of all threads in its subtree---a ``global'' transitive notion,
+  which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}).
+  We can however improve upon this. For this recall the notion
+  of @{term children} of @{text th} (defined in \eqref{children})
   where a child is a thread that is only one ``hop'' away from the thread
-  @{text th} in the @{term RAG} (and waiting for @{text th} to release
-  a resource). We can prove the following lemma.
-
-  \begin{center}
-  @{thm tG_alt_def}\\
-  ???? %@ {thm dependants_alt_tG} 
-  \end{center}
-
-  \begin{center}
-  ???? %@ {thm valid_trace.cp_alt_def3} 
-  \end{center}
+  @{text th} in the @{term TDG} (and waiting for @{text th} to release
+  a resource). With this we can prove the following lemma.
 
 
   \begin{lemma}\label{childrenlem}
-  HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
+  @{text "If"} @{thm (prem 1) valid_trace.cp_rec_tG} @{text "then"}
   \begin{center}
-  @{thm valid_trace.cp_rec_tG}.
-  %@ {thm (concl) cp_rec}.
+  @{thm (concl) valid_trace.cp_rec_tG}.
   \end{center}
   \end{lemma}
   
   \noindent
   That means the current precedence of a thread @{text th} can be
-  computed locally by considering only the current precedences of the children of @{text th}. In
+  computed locally by considering only the static precedence of @{text th}
+  and 
+  the current precedences of the children of @{text th}. In
   effect, it only needs to be recomputed for @{text th} when one of
-  its children changes its current precedence.  Once the current 
+  its children changes its current precedence.  This is much more efficient 
+  because when the  @{text cprec}-value is not changed for a child, 
+  the recursion does not need to decend into the corresponding subtree.
+  Once the current 
   precedence is computed in this more efficient manner, the selection
   of the thread with highest precedence from a set of ready threads is
   a standard scheduling operation implemented in most operating

Binary file journal.pdf has changed