1. n : {1...}
2. h : {2..(n+1)}
3. n = {2..n+1}(h)
4. is_prime_factorization(2; (n+1); h)
  f:(Prime). f is a factorization of n

1

complete_intseg_mset(2; (n+1); h) is a factorization of n

8 steps

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