(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
1
1.
x
:
2. prime(
x
)
2
x
By:
Use:[
x
]
Inst:
Thm*
p
:
. prime(
p
)
p
= 0 &
(
p
~ 1) & (
a
:
.
a
|
p
(
a
~ 1)
(
a
~
p
))
Generated subgoal:
1
3.
x
= 0
4.
(
x
~ 1)
5.
a
:
.
a
|
x
(
a
~ 1)
(
a
~
x
)
2
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
2
x
2x
p:
. prime(p) 
p = 0 & (p ~ 1) & (a:. a | p (a ~ 1) 
(a ~ p))x = 0
(x ~ 1)
a:. a | x (a ~ 1) (a ~ x)
2x
