Nuprl - Proof: int ooc nat 1 2 a 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 2 a 1

1. f :

2.

i:

. 0

i

f(i) = i

2
3.

i:

.

0

i

f(i) = (-i)

2-1
4. x :

5. y :

6. x

2 = y

2-1

False

By:	Inst: Thm* k:, q1,q2:, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 Using:[2 \| x \| y-1 \| 0 \| 1]

Generated subgoals:

None

About:

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

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