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.
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
nondecreasing
Def
nondecreasing(
f
;
k
) ==
i
:
(
k
-1).
f
(
i
)
f
(
i
+1)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
nat
Sections
MarkB
generic
Doc
== {i:
| 0
i } 
Type
i:(k-1). f(i)f(i+1) == {i:| 0i } Typei:(k-1). f(i)f(i+1)
