Thms
languages
Sections
AutomataTheory
Doc
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
About:
| i
k & kj }
i,j:. {i...j} 
TypeB == 
B < A
i,j:. ij PropA == A 
False
A:Prop. (A) Prop| ik & kj }
B == B < A
A == A False
