1. a : {2...}
2. b : 
3. k : 
4. k1:. 
4. k1<k
4. 
4. (g,h:({a..b}).
4. (is_prime_factorization(a; b; g) & is_prime_factorization(a; b; h)
4. (
4. ({a..b}(g) = k1  {a..b}(g) = {a..b}(h)  g = h)
5. g : {a..b}
6. h : {a..b}
7. is_prime_factorization(a; b; g)
8. is_prime_factorization(a; b; h)
9. {a..b}(g) = k
10. {a..b}(g) = {a..b}(h)
11. j : {a..b}
12. 0<g(j)
13. prime(j)
14. j | {a..b}(g)
15. j | {a..b}(h)
16. 0<h(j)
17. {a..b}(reduce_factorization(g; j))
17. =
17. {a..b}(reduce_factorization(h; j))
  {a..b}(reduce_factorization(g; j))<k

By:	FwdThru:  Thm*  a:, b:, f:({a..b}), j:{a..b}. Thm*  2j  0<f(j)  {a..b}(reduce_factorization(f; j))<{a..b}(f) on [ 0<g(j) ] ...

None

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