(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
2
1
1.
x
:
2. 0<
x
3.
y
:
4.
y
y
x
-1
5.
x
-1<(
y
+1)
(
y
+1)
y
:
.
y
y
x
&
x
<(
y
+1)
(
y
+1)
By:
Decide:
x
<(
y
+1)
(
y
+1)
Generated subgoals:
1
6.
x
<(
y
+1)
(
y
+1)
y
:
.
y
y
x
&
x
<(
y
+1)
(
y
+1)
1
step
2
6.
x
<(
y
+1)
(
y
+1)
y
:
.
y
y
x
&
x
<(
y
+1)
(
y
+1)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc