(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int ooc nat 1 2 1 1 1 3 1

1. f : 
2. i:. 0i  f(i) = i2
3. i:0i  f(i) = (-i)2-1
4. x,y:x y2-1
5. a1 : 
6. a2 : 
7. f(a1) = f(a2)
8. 0a1
9. 0a2
10. f(a1) = (-a1)2-1
11. f(a2) = a22
  a1 = a2


By: Inst: Hyp:4 Using:[a2 | -a1]


Generated subgoals:

None

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

(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc