1. f : Prime
2. n : 
3. n' : 
4. nn'
5. f is a factorization of n
6. f is a factorization of n'
  n = n'

1

7. x:Prime. n'<x  f(x) = 0 8. n' = {2..n'+1}(prime_mset_complete(f)) 9. x:Prime. n<x  f(x) = 0 10. n = {2..n+1}(prime_mset_complete(f))   n = n'

9 steps

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