n:
2. n = 0 
(l:3*. LangOf(Auto
)(l)) auto3_lang
} == {k:
| i 
k < j }
Thm* n:2. n = 0 (l:3*. LangOf(Auto)(l)) auto3_lang
Thm* n:2. n = 0 (l:2*. LangOf(Auto
)(l)) auto2_lang
Thm* n:2. n = 0 (l:2*. LangOf(Auto
)(l)) auto1_lang
In prior sections: int 1 bool 1 choice 1 int 2 list 1 finite sets list 3 autom exponent relation autom det automata myhill nerode automata 5 automata 6