--- a/Paper/Paper.thy	Tue Mar 30 10:36:05 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 11:32:12 2010 +0200
@@ -1183,10 +1183,9 @@
   @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
   \end{center}
 
-  TODO existance of permutations.
-
   Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
-  of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if
+  of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
+  exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
   the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
   For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
 
@@ -1195,21 +1194,26 @@
   $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\
   $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a deep non-recursive binder
      with the auxiliary binding function @{text "bn\<^isub>m"}\\
-  $\bullet$ & @{text "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x)) \<approx>gen \<approx>s fvs pi (bn\<^isub>m y\<^isub>j, (y\<^isub>j, s)"}
-     provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
-     function @{text "bn\<^isub>m"}, ...\\
-  $\bullet$ & @{text "(x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"}
-     is bound in @{text "x\<^isub>j"} \\
+  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}
+     provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
+     function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
+     free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
+     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>n"}\\
   $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
-  $\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided  @{text "bn\<^isub>m x\<^isub>n"}
-    is bound non-recursively in @{text "x\<^isub>j"} \\
+  $\bullet$ & @{term "(x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"}
+     is bound in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the
+     alpha-equivalence for @{term "x\<^isub>j"}
+     and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
+  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided  @{text "bn\<^isub>m x\<^isub>n"}
+    is bound non-recursively in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the
+     alpha-equivalence for @{term "x\<^isub>j"}
+     and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
   $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes
     the types being defined, raw)\\
   $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
   \end{tabular}
   \end{center}
 
-
 *}
 
 section {* The Lifting of Definitions and Properties *}