1. x : 
  prime(x)  x<2  (i,j:{2..x}. x = ij)

By:	Rewrite by Thm*  x:. prime(x)  2x & (i:{2..x}. i | x) THEN Rewrite by Thm*  Dec(A)  ((A & B)  A  B) THEN Rewrite by Thm*  Dec(A)  (A  A)

1

2x  (i:{2..x}. i | x)  x<2  (i,j:{2..x}. x = ij)

3 steps

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