1. X : 
2. prime(X)
3. X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)
4. W : 
5. W1:. W1<W  0<W1  W1<X  (t:. X | tW1  X | t)
6. 0<W
7. W<X
8. t : 
9. u : 
10. tW = Xu
11. W = 1
12. X1 : {2...}
13. X1W
14. prime(X1)
15. c : 
16. W = X1c
  X | t

By:	Rewrite10 by W = X1c ...

1

17. tX1c = Xu   X | t

12 steps

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