WhoCites
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites int
iseg?
int_iseg
Def {
i
...
j
} == {
k
:
|
i
k
&
k
j
}
Thm*
i
,
j
:
. {
i
...
j
}
Type
le
Def
A
B
==
B
<
A
Thm*
i
,
j
:
. (
i
j
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
{
i
...
j
}
has structure:
int_iseg(
i
;
j
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
HanoiTowers
Sections
NuprlLIB
Doc