1214   \end{tabular}

  1215   \end{center}

  1216 

  1217   The alpha-equivalence relations for binding functions are similar to the alpha-equivalences

  1218   for their respective types, the difference is that they ommit checking the arguments that

  1219   are bound. We assumed that there are no bindings in the type on which the binding function

  1220   is defined so, there are no permutations involved. For a binding function clause 

  1221   @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent

  1222   @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:

  1223   \begin{center}

  1224   \begin{tabular}{cp{7cm}}

  1225   $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\

  1226   $\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"}\\

  1227   $\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"}

  1228     under the binding function @{text "bn\<^isub>m"}\\

  1229   $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\