# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269942341 -7200
# Node ID 62b87efcef29ccfc8190d684f52cd674a7c5f811
# Parent  70c5e688f67788563b1cf16d6392572f3326ac12
alpha_bn

diff -r 70c5e688f677 -r 62b87efcef29 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 11:32:12 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 11:45:41 2010 +0200
@@ -1214,6 +1214,22 @@
   \end{tabular}
   \end{center}
 
+  The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
+  for their respective types, the difference is that they ommit checking the arguments that
+  are bound. We assumed that there are no bindings in the type on which the binding function
+  is defined so, there are no permutations involved. For a binding function clause 
+  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
+  \begin{center}
+  \begin{tabular}{cp{7cm}}
+  $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\
+  $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not a nominal datatype and does not occur in @{text "rhs"}\\
+  $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a nominal datatype occuring in @{text "rhs"}
+    under the binding function @{text "bn\<^isub>m"}\\
+  $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\
+  \end{tabular}
+  \end{center}
+
 *}
 
 section {* The Lifting of Definitions and Properties *}