1169 

  1170   \begin{exercise}\label{ex:debruijn}

  1171   Implement the function,\footnote{Personal communication of

  1172   de Bruijn to Dyckhoff.} called deBruijn n, that constructs terms of the form:

  1173   

  1174   \begin{center}

  1175   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

  1176   {\it rhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n.  P\,i}\\

  1177   {\it lhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n. P\,i = P (i + 1 mod n)}

  1178                         $\longrightarrow$ {\it rhs n}\\

  1179   {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\

  1180   \end{tabular}

  1181   \end{center}

  1182 

  1183   For n=3 this function returns the term

  1184 

  1185   \begin{center}

  1186   \begin{tabular}{l}

  1187   (P 2 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\

  1188   (P 1 = P 2 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\ 

  1189   (P 1 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1

  1190   \end{tabular}

  1191   \end{center}

  1192 

  1193   \end{exercise}