Nuprl - Proof: primes sqr roots 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: primes sqr roots 1 1 1 1 1

1. a :

2. prime(a)
3. p :

4. q :

5. p

p = a

q
6.

, q:

. p

p = a

(

p':

. p'<p & q

q = a

p')
7. p' :

8. p'<p
9. q

q = a

p':

. p'<p & (

q':

. p'

p' = a

q')

By:	FwdThru: Hyp:6 on [ Hyp:9 ]

Generated subgoal:

1 10. q' :
11. q'<q
12. p'p' = aq'q'
p':. p'<p & (q':. p'p' = aq'q')
1 step

About:

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