Nuprl - Proof: int ooc nat 1

(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

f:(

). Bij(

;

; f)

By:	SimilarTo f:(). (i:. 0i f(i) = i2 ) & (i:. 0i f(i) = (-i)2-1 )

Generated subgoals:

1   f:(). (i:. 0i  f(i) = i2) & (i:. 0i  f(i) = (-i)2-1)
6 steps

2 1. f :
2. i:. 0i  f(i) = i2
3. i:. 0i  f(i) = (-i)2-1
  Bij(; ; f)
19 steps

About:

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

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