L:LangOver(Alph).
Fin(Alph) 
Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l)))
(
St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))
mn_31
P
Thm* L:LangOver(Alph).
Fin(Alph)
Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l)))
(St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))
mn_31
Thm* n:{1...}, A:Type, L:LangOver(A), R:(A*
A*Prop).
Fin(A)
(EquivRel x,y:A*. x R y)
(
n ~ (x,y:A*//(x R y)))
(x,y,z:A*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:A*//(x R y))
). l:A*. L(l) 
g(l))
(m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l)))
mn_23
Thm* R:(Alph*Alph*Prop).
Fin(Alph)
(EquivRel x,y:Alph*. x R y)
Fin(x,y:Alph*//(x R y))
(x,y,z:Alph*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
mn_23_lem_1
Thm* R:(Alph*Alph*Prop).
Fin(Alph)
(EquivRel x,y:Alph*. x R y)
Fin(x,y:Alph*//(x R y))
(x,y,z:Alph*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
mn_23_lem
In prior sections: core int 1 bool 1 int 2 finite sets list 3 autom exponent rel 1 quot 1 relation autom det automata