- let Y = \T.(\x.T(xx))(\x.T(xx)) in
- Y Y = \T.(\x.T(xx))(\x.T(xx)) Y
- = (\x.Y(xx))(\x.Y(xx))
- = Y((\x.Y(xx))(\x.Y(xx)))
- = Y(Y((\x.Y(xx))(\x.Y(xx))))
- = Y(Y(Y(...(Y(YY))...)))
+<pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
+Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
+ ~~> (\x. Y (x x)) (\x. Y (x x))
+ ~~> Y ((\x. Y (x x)) (\x. Y (x x)))
+ ~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
+ ~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>