1. X : 
2. prime(X)
3. W:. 0<W  W<X  (t:. X | tW  X | t)
4. a : 
5. b : 
6. X | ab
7. x : 
8. r : X
9. a = xX+r
10. y : 
11. s : X
12. b = yX+s
13. r = 0
  X | rs

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

1

14. e :  15. ab = Xe   X | rs

4 steps

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