(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. x : 
2. x1:. x1<x  x1!  
  x!  
By: Compute x! * if x=0 1 else x(x-1)! fi

Generated subgoal:

1   if x=0 1 else x(x-1)! fi  
5 steps

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

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