(6steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
nat
sqrt
x
:
.
y
:
.
y
y
x
&
x
<(
y
+1)
(
y
+1)
By:
NatInd Concl
Generated subgoals:
1
y
:
.
y
y
0 & 0<(
y
+1)
(
y
+1)
1
step
2
1.
x
:
2. 0<
x
3.
y
:
.
y
y
x
-1 &
x
-1<(
y
+1)
(
y
+1)
y
:
.
y
y
x
&
x
<(
y
+1)
(
y
+1)
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
x:
. 
y:. y
y
x & x<(y+1)(y+1) x:. y:. yyx & x<(y+1)(y+1) y:. yy0 & 0<(y+1)(y+1)
y:. yyx-1 & x-1<(y+1)(y+1)
y:. yyx & x<(y+1)(y+1)
