(7steps total)
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
primes
sqr
roots
1
1
1.
a
:
2. prime(
a
)
3.
p
:
4.
q
:
.
p
p
=
a
q
q
p'
:
.
p'
<
p
& (
q'
:
.
p'
p'
=
a
q'
q'
)
By:
Analyze4
Generated subgoal:
1
4.
q
:
5.
p
p
=
a
q
q
p'
:
.
p'
<
p
& (
q'
:
.
p'
p'
=
a
q'
q'
)
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc