IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
composite with prime factor11111 1. x :
2. x1:. x1<x 2x1 prime(x1) (i,j:{2..x1}. x1 = ij & prime(i))
3. 2x 4. prime(x)
5. i : {2..x}
6. j : {2..x}
7. x = ij 8. prime(i)
i,j:{2..x}. x = ij & prime(i)
By:
Witness: i | j ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html