(9steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
neg
y
:
. prime(-
y
)
prime(
y
)
By:
x
:
. prime(-
x
)
prime(
x
) Asserted
Generated subgoals:
1
x
:
. prime(-
x
)
prime(
x
)
6
steps
2
1.
x
:
. prime(-
x
)
prime(
x
)
y
:
. prime(-
y
)
prime(
y
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
y:
. prime(-y) 
prime(y) y:. prime(-y) prime(y)x:. prime(-x) 
prime(x) Asserted x:. prime(-x) prime(x)
x:. prime(-x) prime(x)
y:. prime(-y) prime(y)
