Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
increasing
Def
increasing(
f
;
k
) ==
i
:
(
k
-1).
f
(
i
)<
f
(
i
+1)
Thm*
k
:
,
f
:(
k
). increasing(
f
;
k
)
Prop
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
nat
Sections
MarkB
generic
Doc
i:
(k-1). f(i)<f(i+1)k:, f:(k
). increasing(f;k) 
Prop == {i:| 0
i } Typei:(k-1). f(i)<f(i+1)k:, f:(k). increasing(f;k) Prop == {i:| 0i } Type
