(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.
x
:
2. 2
x
3.
(
i
:{2..
x
}.
i
|
x
)
4.
b
:
5.
b
|
x
(
b
~ 1)
(
b
~
x
)
By:
SideProof
Generated subgoal:
1
5. |
b
| |
x
6. |
b
| ~
b
(|
b
| ~ 1)
(|
b
| ~
x
)
9
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc