(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fin plus nat ooc nat 1 1
1. k : 
  (j.if j<k inl(j) else inr(j-k) fi)  (k+)
By: Analyze THEN SplitITE Concl

Generated subgoals:

None

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

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc