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

i:

. f(i) = n

By:	Inst: Thm* a:, b:. q:, r:b. a = qb+r Using:[n \| 2] THEN ExistHD Hyp:-1

Generated subgoal:

1 6. q :
7. r : 2
8. n = q2+r
i:. f(i) = n
5 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