(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
nat
3
1
2
1
1
1
1
1.
x
:
2. 2
x
3.
(
i
:{2..
x
}.
i
|
x
)
4.
b
:
5. |
b
| |
x
6. |
b
| ~
b
7. |
b
|
x
(2
|
b
| & |
b
|<
x
)
By:
SimilarTo Hyp:3
Generated subgoal:
1
8. 2
|
b
| & |
b
|<
x
i
:{2..
x
}.
i
|
x
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc