1. k : {2...}
2. n : 
3. n1:. 
3. n1<n
3. 
3. (g:({2..k}). 
3. (2  n1 < k+1
3. (
3. ((i:{2..k}. n1i  0<g(i)  prime(i))
3. (
3. ((h:({2..k}). 
3. (({2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h)))
4. g : {2..k}
5. 2n
6. n<k+1
7. i:{2..k}. ni  0<g(i)  prime(i)
8. n = 2
9. prime(n-1)
  h:({2..k}). 
  {2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h)

By:	Inst:  Thm*  k:{2...}, g:({2..k}), z:{2..k}. Thm*  prime(z) Thm*   Thm*  (g':({2..k}).  Thm*  ({2..k}(g) = {2..k}(g') Thm*  (& g'(z) = 0 Thm*  (& (u:{2..k}. z<u  g'(u) = g(u))) Using:[k | g | n-1] ...a THEN ExistHD Hyp:-1

1

10. g' : {2..k} 11. {2..k}(g) = {2..k}(g') 12. g'(n-1) = 0 13. u:{2..k}. n-1<u  g'(u) = g(u)   h:({2..k}).    {2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h)

4 steps

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