IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime nat312111211 1. x : 2. 2x 3. (i:{2..x}. i | x)
4. b : 5. |b| | x 6. |b| ~ b 7. |b|x 8. (2|b| & |b|<x)
9. |b| = 0
False
By:
FwdThru: Thm*a:. 0 | aa = 0 on [ 0 | x ] THENA Subst: |b| = 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x
(
i:{2..x
}. i | x)
False
a:
a = 0 on [ 0 | x ] THENA Subst
: |b| = 0
