Nuprl Basics - Proof: sfa doc ycomb factorial typing 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ycomb factorial typing 2

1. x :

Y((

f,x. if x=

1 else x

f(x-1) fi),x)

By:	CompNatInd Hyp:-1

Generated subgoal:

1 2. x1:. x1<x Y((f,x. if x=0 1 else xf(x-1) fi),x1)
Y((f,x. if x=0 1 else xf(x-1) fi),x)
5 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html