(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.
a
:
2. prime(
a
)
(
p
:
,
q
:
.
p
p
=
a
q
q
)
By:
BackThru:
Thm*
P
:(
Prop). (
x
:
.
P
(
x
)
(
x'
:
.
x'
<
x
&
P
(
x'
)))
(
x
:
.
P
(
x
))
Generated subgoal:
1
3.
p
:
4.
q
:
.
p
p
=
a
q
q
p'
:
.
p'
<
p
& (
q'
:
.
p'
p'
=
a
q'
q'
)
5
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
(
p:, q:
. p
p = aqq)
(p:, q:. pp = aqq)
P:(
Prop). (x:. P(x) 
(x':. x'<x & P(x'))) (x:. P(x))
q:. pp = aqq
p':. p'<p & (q':. p'p' = aq'q')
