--- a/Journal/Paper.thy	Tue Jul 12 15:09:09 2016 +0100
+++ b/Journal/Paper.thy	Tue Aug 16 11:49:37 2016 +0100
@@ -472,7 +472,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
-  @{term "(Cs cs, Th th)"}
+  @{term "(Cs cs, Th th)"}\hfill\numbered{pairs}
   \end{isabelle}
 
   \noindent
@@ -532,17 +532,18 @@
   Isabelle, we choose to introduce our own library of graphs for
   PIP. The reason for this is that we wanted to be able to reason with
   potentially infinite graphs (in the sense of infinitely branching
-  and infinite size): the property that our RAGs are forrests of
-  finitely branching trees having only an finite depth should be a
+  and infinite size): the property that our RAGs are actually forrests
+  of finitely branching trees having only an finite depth should be a
   something we can \emph{prove} for our model of PIP---it should not
-  be an assumption we build already into our model. It seemed  for our purposes the most convenient
-  represeantation of graphs are binary relations given by 
-  sets of pairs. The pairs stand for the edges in graphs. This
-  relation-based representation is convenient since we can use the notions
-  of transitive closure operations @{term "trancl DUMMY"} and 
-  @{term "rtrancl DUMMY"}, as well as relation composition @{term "DUMMY O DUMMY"}.
-  A \emph{forrest} is defined as the relation @{text rel} that is \emph{single valued}
-  and \emph{acyclic}:
+  be an assumption we build already into our model. It seemed for our
+  purposes the most convenient represeantation of graphs are binary
+  relations given by sets of pairs from \eqref{pairs}. The pairs stand for the edges in
+  graphs. This relation-based representation is convenient since we
+  can use the notions of transitive closure operations @{term "trancl
+  DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation composition
+  @{term "DUMMY O DUMMY"}.  A \emph{forrest} is defined as the
+  relation @{text rel} that is \emph{single valued} and
+  \emph{acyclic}:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -568,6 +569,17 @@
   forrest} is a forest which is well-founded and every node has 
   finitely many children (is only finitely branching).
 
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm rtrancl_path.intros}
+  \end{isabelle} 
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm rpath_def}
+  \end{isabelle}
+
+
+  {\bf Lemma about overlapping paths}
+  
 
   We will design our PIP-scheduler  
   so that every thread can be in the possession of several resources, that is 
@@ -607,6 +619,10 @@
   @{thm cpreced_def}\hfill\numbered{cpreced}
   \end{isabelle}
 
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cp_alt_def cp_alt_def1}
+  \end{isabelle}
+
   \noindent
   where the dependants of @{text th} are given by the waiting queue function.
   While the precedence @{term prec} of any thread is determined statically