(21steps total)
Remark
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat
prime
div
each
factor
X
:
. prime(
X
)
(
a
,
b
:
.
X
|
a
b
X
|
a
X
|
b
)
By:
CompNatInd Concl THEN Analyze ...w
Generated subgoal:
1
1.
X
:
2.
X1
:
.
X1
<
X
prime(
X1
)
(
a
,
b
:
.
X1
|
a
b
X1
|
a
X1
|
b
)
3. prime(
X
)
a
,
b
:
.
X
|
a
b
X
|
a
X
|
b
20
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(21steps total)
Remark
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
X:
. prime(X) 
(a,b:. X | a
b X | a 
X | b) X:. prime(X) (a,b:. X | ab X | a X | b)
X1:. X1<X prime(X1) (a,b:. X1 | ab X1 | a X1 | b)
a,b:. X | ab X | a X | b
