1. a : 
2. b : 
3. f : {a..b}
4. j : {a..b}
5. 0<f(j)
6. is_prime_factorization(a; b; f)
  is_prime_factorization(a; b; reduce_factorization(f; j))

1

6. i : {a..b} 7. 0<reduce_factorization(f; j)(i)   0<f(i)

1 step

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