Nuprl - Proof: prime elim 1 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime elim 1 1 1 2

1. p :

2. prime(p)
3.

p = 0
4.

(p ~ 1)
5.

b,c:

. (b ~ 1)

(c ~ 1)

p = b

c
6. a :

7. c :

8. p = a

c
9.

a = 0

(a ~ 1)

(a ~ p)

By:	Decide (c = 0)

Generated subgoals:

1 10. c = 0
(a ~ 1) (a ~ p)
1 step

2 10. c = 0
(a ~ 1) (a ~ p)
5 steps

About:

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

1	10. c = 0 (a ~ 1) (a ~ p)	1 step
2	10. c = 0 (a ~ 1) (a ~ p)	5 steps