(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ycomb factorial typing 2 1 1 1
1. x : 
2. x1:. x1<x  Y((f,x. if x=0 1 else xf(x-1) fi),x1)  
3. x = 0
  xY((f,x. if x=0 1 else xf(x-1) fi),x-1)  
By: BackThru: Thm* i,j:. ij  

Generated subgoals:

1   x  
Trivial
2   Y((f,x. if x=0 1 else xf(x-1) fi),x-1)  
1 step

About:
ifthenelseintnatural_numbersubtractmultiplyless_than
lambdaapplyycombequalmemberimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc