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* L:LangOver(Alph), R:(Alph*Alph*Prop). (EquivRel 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))). (l:Alph*. L(l) g(l)) x,y:Alph*//(x L-induced Equiv y) = x,y:Alph*//(x Rg y)) mn_23_Rl_equal_Rg

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* a,b:. (a b) a = b assert_iff_eq

Thm* p,q:. p = q = false p = q beq_neq

Thm* p,q:. p = q = true p = q beq_eq

Thm* L:LangOver(Alph), R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (g:((x,y:Alph*//(x R y))). l:Alph*. L(l) g(l)) & (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (x,y:Alph*. (x R y) (x L-induced Equiv y)) mn_23_refinment

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

Thm* R:(A*A*Prop). (EquivRel 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:LangOver(A). (l:A*. L(l) g(l)) (x,y:A*. (x L-induced Equiv y) (x Rg y))) Rl_iff_Rg

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 finite sets list 3 autom exponent rel 1 quot 1 relation autom languages det automata