| else -> A(m-1, A(m,n-1))
A(0,y) = y+1
- A(1,y) = y+2
- A(2,y) = 2y + 3
+ A(1,y) = 2+(y+3) - 3
+ A(2,y) = 2(y+3) - 3
A(3,y) = 2^(y+3) - 3
A(4,y) = 2^(2^(2^...2)) [where there are y+3 2s] - 3
...
<pre><code>Θ′ ≡ (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
Y′ ≡ \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))</code></pre>
-Θ′ has the advantage that <code>f (Θ′ f)</code> really *reduces to* <code>Θ′ f</code>.
+<code>Θ′</code> has the advantage that <code>f (Θ′ f)</code> really *reduces to* <code>Θ′ f</code>.
<code>f (Y′ f)</code> is only convertible with <code>Y′ f</code>; that is, there's a common formula they both reduce to. For most purposes, though, either will do.