(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.
m
:
2.
n
:
3.
P
:(
). (
n
:
.
P
(
n
+1)
P
(
n
)) &
P
(
m
) &
P
(
n
)
m
<
n
By:
Analyze 3 THEN StrongAuto
Generated subgoal:
1
3.
P
:
4.
n
:
.
P
(
n
+1)
P
(
n
)
5.
P
(
m
)
6.
P
(
n
)
m
<
n
19
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
P:(
). (
n:. P(n+1) 
P(n)) & P(m) & 
P(n)
m<n
P:(). (n:. P(n+1) P(n)) & P(m) & P(n)
m<n
n:. P(n+1) P(n)
P(n)
m<n
