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

Thm* S:ActionSet(Alph), sL:S.car*. Fin(Alph) Fin(S.car) (TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) total_back_listify

Thm* f:(T). Fin(T) (fL:T*. t:T. f(t) mem_f(T;t;fL)) bool_listify

Thm* S:ActionSet(Alph), s:S.car. Fin(Alph) Fin(S.car) (BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s)) back_listify

Thm* Fin(T) (TL:T*. t:T. mem_f(T;t;TL)) fin_listify

Thm* L:LangOver(Alph). Fin(Alph) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto)) (R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) c (g:((x,y:Alph*//R(x,y))). Fin(x,y:Alph*//R(x,y)) & (l:Alph*. L(l) g(l)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)))) mn_12

In prior sections: finite sets list 3 autom exponent det automata