(23steps total)
PrintForm
Definitions
hol
prim
rec
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hless
def
1
2
1
3
1
1
1.
m
:
2.
n
:
3.
P
:
4.
n
:
.
P
(
n
+1)
P
(
n
)
5.
P
(
m
)
6.
P
(
n
)
7.
m
>
n
8.
k
:
P
(
n
+
k
)
P
(
n
)
By:
Assert (0
n
+
k
) THEN StrongAuto
Generated subgoals:
1
0
n
+
k
Auto
2
9. 0
n
+
k
10.
P
(
n
+
k
)
P
(
n
)
8
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(23steps total)
PrintForm
Definitions
hol
prim
rec
Sections
HOLlib
Doc
n:
P(n)
P(n)
P(n+k) 
n+k) THEN StrongAuto
