--- a/Paper.thy	Sun Jun 16 20:42:07 2013 -0400
+++ b/Paper.thy	Mon Jun 17 15:23:02 2013 +0800
@@ -534,20 +534,8 @@
   \noindent
   Clearly the operating system should only allow to clone a process @{text p} if the 
   process is currently alive. The cloned process will get the process
-  ID generated by the function @{term new_proc}. This process ID should
-  not already exist. Therefore we define @{term new_proc} as *}
-
-  (* HERE ????? chunhan *)
-text {*
-  \begin{isabelle}\ \ \ \ \ %%%
-  \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}
-  \end{tabular}}
-  \end{isabelle}
-
-  \noindent
-  namely the highest ID currently in existence increased by one. The 
-  admissibility rules for the other events impose similar conditions.
+  ID ``randomly'' generated by the operating system, but this process ID should
+  not already exist. The admissibility rules for the other events impose similar conditions. 
 
   However, the admissibility check by the operating system is only one
   ``side'' of the constraints the RC-Model imposes. We also need to
@@ -1276,7 +1264,6 @@
 
 
 
-
 section {*Conclusion and Related Works*}
 
 
@@ -1493,4 +1480,19 @@
   role is assigned to its creator's role.
 
 *}
+
+
+ HERE: chunhan
+Therefore we define @{term new_proc} as 
+
+  (*  *)
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent
+  namely the highest ID currently in existence increased by one.
+
 *)
\ No newline at end of file

Binary file paper.pdf has changed