--- a/Journal/Paper.thy	Fri Apr 21 20:17:13 2017 +0800
+++ b/Journal/Paper.thy	Tue Apr 25 14:05:57 2017 +0100
@@ -392,7 +392,7 @@
   \noindent
   In this definition @{term "length s"} stands for the length of the list
   of events @{text s}. Again the default value in this function is @{text 0}
-  for threads that have not been created yet. An actor of an event is
+  for threads that have not been created yet. An \emph{actor} of an event is
   defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -401,6 +401,8 @@
     @{thm (rhs) actor.simps(5)}\\
   @{thm (lhs) actor.simps(1)} & @{text "\<equiv>"} & 
     @{thm (rhs) actor.simps(1)}\\
+  @{thm (lhs) actor.simps(4)} & @{text "\<equiv>"} & 
+    @{thm (rhs) actor.simps(4)}\\
   @{thm (lhs) actor.simps(2)} & @{text "\<equiv>"} & 
     @{thm (rhs) actor.simps(2)}\\
   @{thm (lhs) actor.simps(3)} & @{text "\<equiv>"} & 
@@ -408,10 +410,10 @@
   \end{tabular}}
   \end{isabelle}
 
-
-
-
-
+  \noindent
+  This allows us to define what actions a set of threads @{text ths} might
+  perform in a list of events @{text s}, namely
+  @{thm actions_of_def[THEN eq_reflection]}.
   A \emph{precedence} of a thread @{text th} in a 
   state @{text s} is the pair of natural numbers defined as
   
@@ -590,15 +592,15 @@
   forrest} is a forrest which is well-founded and every node has 
   finitely many children (is only finitely branching).
 
-  \endnote{
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{thm rtrancl_path.intros}
-  \end{isabelle} 
-  
+  %\endnote{
   %\begin{isabelle}\ \ \ \ \ %%%
-  %@{thm rpath_def}
+  %@ {thm rtrancl_path.intros}
+  %\end{isabelle} 
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %@ {thm rpath_def}
   %\end{isabelle}
-  }
+  %}
 
 
   %\endnote{{\bf Lemma about overlapping paths}}
@@ -614,8 +616,7 @@
   ``chase'' outgoing arrows leading to a single root of a tree.
   
   The use of relations for representing RAGs allows us to conveniently define
-  the notion of the \emph{dependants} of a thread using the transitive closure
-  operation for relations, written ~@{term "trancl DUMMY"}. This gives
+  the notion of the \emph{dependants} of a thread
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm dependants_raw_def}
@@ -642,10 +643,11 @@
   @{thm cpreced_def3}\hfill\numbered{cpreced}
   \end{isabelle}
 
-  \endnote{
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cp_alt_def cp_alt_def1}
-  \end{isabelle}}
+  %\endnote{
+  %\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
@@ -1163,24 +1165,24 @@
   \end{proof}
 
 
-  \endnote{
-  In what follows we will describe properties of PIP that allow us to
-  prove Theorem~\ref{mainthm} and, when instructive, briefly describe
-  our argument. Recall we want to prove that in state @{term "s' @ s"}
-  either @{term th} is either running or blocked by a thread @{term
-  "th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
-  can show that
+  %\endnote{
+  %In what follows we will describe properties of PIP that allow us to
+  %prove Theorem~\ref{mainthm} and, when instructive, briefly describe
+  %our argument. Recall we want to prove that in state @ {term "s' @ s"}
+  %either @{term th} is either running or blocked by a thread @ {term
+  %"th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
+  %can show that
 
 
-  \begin{lemma}
-  If @{thm (prem 2) eq_pv_blocked}
-  then @{thm (concl) eq_pv_blocked}
-  \end{lemma}
+  %\begin{lemma}
+  %If @{thm (prem 2) eq_pv_blocked}
+  %then @{thm (concl) eq_pv_blocked}
+  %\end{lemma}
 
-  \begin{lemma}
-  If @{thm (prem 2) eq_pv_persist}
-  then @{thm (concl) eq_pv_persist}
-  \end{lemma}}
+  %\begin{lemma}
+  %If @{thm (prem 2) eq_pv_persist}
+  %then @{thm (concl) eq_pv_persist}
+  %\end{lemma}}
 
   \endnote{{\bf OUTLINE}
 
@@ -1677,10 +1679,10 @@
   
   Consider the states @{text "s upto t"}. It holds that all the states where
   @{text "th"} runs and all the states where @{text "th"} does not run is 
-  equalt to @{text "1 + len t"}. That means
+  equalt to @{text "len t"}. That means
 
   \begin{center}
-  @{text "states where th does not run = 1 + len t - states where th runs"} (*)
+  @{text "states where th does not run = len t - states where th runs"} (*)
   \end{center}
 
   It also holds that all the actions of @{text "th"} are less or equal to 
@@ -1693,7 +1695,7 @@
   That means in $(*)$ we have 
 
   \begin{center}
-  @{text "states where th does not run \<le> 1 + len t - len (actions_of {th} t)"}
+  @{text "states where th does not run \<le> len t - len (actions_of {th} t)"}
   \end{center}
 
   If we look at all the events that can occur in @{text "s upto t"}, we have that