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. X1 | W
  X | t

By:	Rewrite'-1 by Thm*  a,b:. a | b  (c:. b = ac) ...w THEN Analyze-1

1

15. c :  16. W = X1c   X | t

13 steps

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