(21steps total) PrintForm Definitions rfunction 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fincr wf 1
  {f | i:  if i=0  else {f(i-1)...} fi}  Type
By: With (i,j. i<j) Analyze

Generated subgoals:

1     Type
Auto
2   (i,j. i<j)  Type
Auto
3   WellFnd{[1]}(;u,v.(i,j. i<j)(u,v))
4 steps
4 1. i : 
2. f : {f | i:{z:| z (i,j. i<j) i }  if i=0  else {f(i-1)...} fi}
  if i=0  else {f(i-1)...} fi  Type
13 steps

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

(21steps total) PrintForm Definitions rfunction 1 Sections StandardLIB Doc