finite sets Sections AutomataTheory Doc

identity Def Id(x) == x

Thm* Id AA

int_seg Def {i..j} == {k:| i k < j}

Thm* m,n:. {m..n} Type

nat Def == {i:| 0i}

Thm* Type

lelt Def i j < k == ij & j < k

le Def AB == B < A

Thm* i,j:. ij Prop

not Def A == A False

Thm* (A) Prop