--- a/Paper/Paper.thy	Wed Mar 31 16:27:57 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 17:04:09 2010 +0200
@@ -1258,7 +1258,7 @@
   \end{center}
 
   \noindent
-  To see how these definitions work, let us consider again the term-constructors 
+  To see how these definitions work in practise, let us reconsider the term-constructors 
   @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. 
   For this specification we need to define three functions, namely
   @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
@@ -1293,13 +1293,28 @@
   @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
   that an assignment ``alone'' does not have any bound variables. Only in the
   context of a @{text Let} or @{text "Let_rec"} will some atoms become bound
-  (teh term-constructors that have binding clauses).  This is a phenomenon 
-  that has also been pointed out in \cite{ott-jfp}.
+  (the term-constructors that have binding clauses).  This is a phenomenon 
+  that has also been pointed out in \cite{ott-jfp}. We can also see that
+  given a @{text "bn"}-function for a type @{text "ty"}, then we have
+  %
+  \begin{equation}\label{bnprop}
+  @{text "fv_ty x = bn x \<union> fv_bn x"}.
+  \end{equation}
 
-  Next we define alpha-equivalence realtions for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
-  @{text "\<approx>ty\<^isub>1 \<dots> \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
+  Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+  @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
   we also need to  define auxiliary alpha-equivalence relations for the binding functions. 
-  Say we have @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"}, we also define @{text "\<approx>bn_ty\<^isub>1 \<dots> \<approx>bn_ty\<^isub>n"}.
+  Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.
+  To simplify our definitions we will use the following abbreviations for 
+  relations and free-variable acting on products.
+  %
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{text "(x\<^isub>1, y\<^isub>1) R\<^isub>1 \<otimes> R\<^isub>2 (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
+  @{text "fv\<^isub>1 \<oplus> fv\<^isub>2 (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
+  \end{tabular}
+  \end{center}
+
 
   The relations are inductively defined predicates, whose clauses have
   conclusions of the form  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume 
@@ -1311,9 +1326,9 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   \multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\
-  $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a shallow binder\\
-  $\bullet$ & @{text "x\<^isub>i \<approx>bn_ty\<^isub>i y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep 
-     non-recursive binder\\
+  $\bullet$ & none provided @{text "x\<^isub>i"} is a shallow binder\\
+  $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep 
+     non-recursive binder with the auxiliary binding function @{text bn}\\
   $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep 
      recursive binder\\
   \end{tabular}