\begin{eqnarray*}
&{}&{\bf function}\ {\tt CNF}\,(\phi)\!:\\
&{}&\hbox{/* precondition: \(\phi\) implication free and in \({\tt NNF}\)
*/}\\
&{}&\hbox{/* postcondition: \({\tt CNF}\, (\phi)\)
computes an equivalent \({\tt CNF}\) for
\(\phi\) */}\\
&{}&{\bf begin\ function}\\
&{}&\ \ \ {\bf case}\\
&{}&\ \ \ \ \ \ \phi\ \hbox{is a literal}\colon \ {\bf return}\ \phi\\
&{}&\ \ \ \ \ \ \phi\ \hbox{is }\phi _1\land\phi _2\colon \ {\bf
return}\
{\tt CNF}\, (\phi _1)\land {\tt CNF}\, (\phi _2)\\
&{}&\ \ \ \ \ \ \phi\ \hbox{is }\phi _1\lor\phi _2\colon \ {\bf return}\

{\tt DISTR}\, ({\tt CNF}\, (\phi _1), {\tt CNF}\, (\phi _2))\\
&{}&\ \ \ {\bf end\ case}\\
&{}&{\bf end\ function}
\end{eqnarray*}