(4steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
increasing
lower
bound
k
:
,
f
:(
k
),
x
:
k
. increasing(
f
;
k
)
f
(0)+
x
f
(
x
)
By:
Auto
Generated subgoal:
1
1.
k
:
2.
f
:
k
3.
x
:
k
4. increasing(
f
;
k
)
f
(0)+
x
f
(
x
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
k:
, f:(k
), x:k. increasing(f;k) 
f(0)+x
f(x) k:, f:(k), x:k. increasing(f;k) f(0)+xf(x)
k
k
f(0)+xf(x)
