WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc
Who Cites enum1?
enum1
Def enum1() ==
3
Thm* enum1()
Type
int_seg
Def
{i..j
} == {k:
| i
k < j }
Thm*
m,n:
. {m..n
}
Type
lelt
Def
i
j < k == i
j & j < k
le
Def
A
B ==
B < A
Thm*
i,j:
. (i
j)
Prop
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
Syntax:
enum1()
has structure:
enum1
About:
WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc