Thm* E:(Alph*Alph*Prop). Fin(Alph) & (EquivRel x,y:Alph*. x E y) & (x,y:Alph*. Dec(x E y)) (h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))) fin_alph_list_quo

Thm* q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))) list_quo_choice

Thm* q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))) list_quo_choice_pls

Thm* Auto:Automata(Alph;St). Fin(Alph) & Fin(St) (x,y:Alph*. Dec(x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) Rl_quo_is_decidable

In prior sections: core int 1 bool 1 rel 1 choice 1 int 2 finite sets list 3 autom exponent quot 1 relation autom det automata myhill nerode