function application of N x N -> N
A more formal way to define the down function is
$$
\mathit{down}(x,y) =
\begin{cases}
(x-1,y) &amp; \text{if } x &gt; 0, \\
(y-1,0) &amp; \text{if } x = 0 \text{ and } y &gt; 0, \\
\text{undefined} &amp; \text{if } x=y=0.
\end{cases}
$$