(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
2
2
1.
x
:
2. prime(
x
)
3.
i
: {2..
x
}
4.
i
|
x
i
= 1
i
=
x
By:
SimilarTo (
i
~ 1)
(
i
~
x
)
THEN
Backchain
[
Thm*
a
,
b
:
. (
a
~
b
)
a
=
b
;
Thm*
p
:
. prime(
p
)
p
= 0 &
(
p
~ 1) & (
a
:
.
a
|
p
(
a
~ 1)
(
a
~
p
))]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
}
i = 1 
i = x
}
i = 1 i = x (i ~ x)
a,b:. (a ~ b) 
a = b
p:
. prime(p) 
p = 0 & (p ~ 1) & (a:. a | p (a ~ 1) (a ~ p))]
