(7steps 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 factorial wf 1 1
1. x : 
2. x1:. x1<x  x1!  
  if x=0 1 else x(x-1)! fi  
By: SplitITE Concl

Generated subgoals:

1 3. x = 0
  1  
Auto
2 3. x  0
  x(x-1)!  
3 steps

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

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