\begin{eqnarray*}
&{}&{\bf function}\ {\tt DISTR}\,(\eta _1,\eta _2)\!:\\
{}&{}&\hbox{/* precondition: \(\eta _1\) and \(\eta _2\) are in \({\tt CNF}\)
*/}\\
{}&{}&\hbox{/* postcondition: \({\tt DISTR}\,(\eta _1,\eta _2)\)
computes a \({\tt CNF}\) for \(\eta _1\lor \eta _2\) */}\\
&{}&{\bf begin\ function}\\
&{}&\ \ \ {\bf case}\\
&{}&\ \ \ \ \ \ \eta _1\ \hbox{is }\eta _{11}\land \eta _{12}\colon \
{\bf return}\ {\tt DISTR}\, (\eta _{11}, \eta _2)\land {\tt DISTR}\,
(\eta _{12}, \eta _2)\\
&{}&\ \ \ \ \ \ \eta _2\ \hbox{is }\eta _{21}\land \eta _{22}\colon \
{\bf return}\ {\tt DISTR}\, (\eta _1, \eta _{21})\land {\tt DISTR}\,
(\eta _1, \eta _{22})\\
&{}&\ \ \ \ \ \ \hbox{otherwise (= no conjunctions)}
\colon \
{\bf return}\ \eta _1\lor \eta _2\\
&{}&\ \ \ {\bf end\ case}\\
&{}&{\bf end\ function}
\end{eqnarray*}