es55 (by N.Fazio)

- Y 
Y == \f.(\x.f(xx))(\x.f(xx)) -> \f. f((\x.f(xx))(\x.f(xx))) 
Quindi Y è definito.

- Y not 
Y not == (\f.(\x.f(xx))(\x.f(xx))) (\p. if p false true) ->> 
->> (\f.(\x.f(xx))(\x.f(xx))) (\p. p false true) -> 
-> (\x.(\p. p false true)(xx))(\x.(\p. p false true)(xx)) ->> 
->> (\x.(xx) false true))(\x. (xx) false true)) -> 
-> ((\x. (xx) false true))(\x. (xx) false true))) false true 
A partire da questo momento in poi l'unica beta-riduzione possibile è quella che sostituisce a 
(xx) il termine ((\x. (xx) false true)(\x. (xx) false true)): 
l'effetto non è altro che quello di aggiungere alla fine una coppia false true. 
Pertanto la testa non cambierà e non otterremo alcuna hnf: quindi Y not è non-definito.

- K == \xy.x (Quindi K non è altro che true!) 
K è già in hnf: quindi K è definito.

- Y I 
Y I == (\f.(\x.f(xx))(\x.f(xx))) (\x.x) -> (\x.(\x.x)(xx))(\x.(\x.x)(xx)) -> 
-> (\x.(xx))(\x.(xx)) -> (\x.(xx))(\x.(xx)) 
Da questo momento in poi la beta riduzione porta sempre allo stesso termine: quindi Y I è non-definito.

- x omega 
x omega == x(\x.xx)(\x.xx) 
x omega è già in hnf: quindi x omega è definito.

- Y(K x) 
Y(K x) == (\f.(\x.f(xx))(\x.f(xx)))((\xy.x)x) -> (\f.(\x.f(xx))(\x.f(xx)))(\y.x) -> 
-> (\x.(\y.x)(xx))(\x.(\y.x)(xx)) ->> (\x.x)(\x.x) -> \x.x == I 
Siamo pervenuti ad un termine in hnf: pertanto Y(K x) è definito.
[[FB: E' vero, il termine e' definito, pero' nelle riduzioni che mostrano che si 
riduce ad una head normal form, c'e' un errore che riguarda variabili legate e libere, quale?]]

- n 
n == \fx.f(f(...(f x) ...) 
n è già in hnf.