Def  Y(f) == (x.f(x(x)))(x.f(x(x)))

is mentioned by

Def  find_first_iter(v.p(v); v.f(v); a) Def  == if p(a) a else find_first_iter(v.p(v); v.f(v); f(a)) fi Def  (recursive)	[find_first_iter]
Def  least i:. p(i) == if p(0) 0 else (least i:. p(i+1))+1 fi  (recursive)	[least]
Def  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)	[compose_iter]
Def  a  xs == Case of xs; nil  False ; x.ys  a = x  A  (a  ys) Def  (recursive)	[is_list_mem]

In prior sections: num thy 1 IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html