bs ; a.as' a.(as' @ bs) (recursive)
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* 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* 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
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))). EquivRel u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_equi
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))). Trans u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_tran
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))). Sym u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_symm
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))). Refl(x,y:A*//(x R y);u,v.u Rg v))
lquo_rel_refl
Thm* R:(Alph*Alph*Prop).
(EquivRel x,y:Alph*. x R y)
(x,y,z:Alph*. (x R y) ((z @ x) R (z @ y)))
(z1,z2:Alph*, y:x,y:Alph*//(x R y). z1 @ z2@
y = z1@z2@y)
mn_quo_append_assoc
Thm* A:Type, R:(A*A*Prop).
(EquivRel x,y:A*. x R y)
(x,y,z:A*. (x R y) ((z @ x) R (z @ y)))
(z:A*, y:x,y:A*//(x R y). z@y 
x,y:A*//(x R y))
mn_quo_append_wf
In prior sections: list 1 list 3 autom exponent action sets det automata