--- a/Paper/Paper.thy	Wed Feb 09 06:09:46 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 09 07:27:30 2011 +0000
@@ -24,7 +24,7 @@
   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
   L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
   Lam ("\<lambda>'(_')" [100] 100) and 
-  Trn ("_, _" [100, 100] 100) and 
+  Trn ("'(_, _')" [100, 100] 100) and 
   EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
   transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
   Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999)
@@ -433,11 +433,24 @@
   the other terms contain the empty string. 
 
 
-  Our proof of Thm.~\ref{myhillnerodeone}
-  will be by transforming the equational system into a \emph{solved form}
-  maintaining the invariants \eqref{inv1} and \eqref{inv2}. From the solved
-  form we will be able to read off the regular expressions using our 
-  variant of Arden's Lemma (Lem.~\ref{arden}).
+  Our proof of Thm.~\ref{myhillnerodeone} will be by transforming the
+  equational system into a \emph{solved form} maintaining the invariants
+  \eqref{inv1} and \eqref{inv2}. From the solved form we will be able to read
+  off the regular expressions. 
+
+  In order to transform an equational system into solved form, we have two main 
+  operations: one that takes an equation of the form @{text "X = rhs"} and removes
+  the recursive occurences of @{text X} in @{text rhs} using our variant of Arden's 
+  Lemma (Lem.~\ref{arden}). The other operation takes an equation @{text "X = rhs"}
+  and substitutes @{text X} throughout the rest of the equational system
+  adjusting the regular expressions approriately. To define them we need the
+  operation 
+
+  \begin{center}
+  @{thm attach_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+  @{thm attach_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  \end{center}
+
 
 *}