Nuprl - Proof: prime factorization limit 1

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

1. n :

2. f : Prime

3. g : Prime

4. f is a factorization of n
5. g is a factorization of n
6.

x:{2..(n+1)

}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x)
7. x : Prime

f(x) = g(x)

By:	Analyze-1 THEN Decide: n<x

Generated subgoals:

1 7. x :
8. prime(x)
9. n<x
f(x) = g(x)
1 step

2 7. x :
8. prime(x)
9. n<x
f(x) = g(x)
3 steps

About:

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

1	7. x : 8. prime(x) 9. n<x f(x) = g(x)	1 step
2	7. x : 8. prime(x) 9. n<x f(x) = g(x)	3 steps