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

1. f :

2.

i:

. 0

i

f(i) = i

2
3.

i:

.

0

i

f(i) = (-i)

2-1
4.

x,y:

. x

2

y

2-1
5. a1 :

6. a2 :

7. f(a1) = f(a2)
8. 0

a1
9.

0

a2
10. f(a1) = a1

2
11. f(a2) = (-a2)

2-1

a1 = a2

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

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