Selected Objects
| THM | mn_13 |  Auto:Automata(Alph;St). Fin(Alph) & Fin(St)   Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) |
| THM | Rl_quo_is_decidable | Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) (x,y:Alph*. Dec(x = y  x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) |
| THM | list_quo_choice_pls | 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)))) |
| THM | empty_alph_list | q:, x:q*. q = 0 x = nil |
| THM | list_quo_choice | 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)))) |
| THM | fin_alph_list_quo | 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)))) |
| THM | homo_is_surj | Auto:Automata(Alph;St), c:(StAlph*).
(q:St. (Result(Auto)c(q)) = q) & Fin(Alph) & Fin(St)
Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c) |
| THM | surj_is_inj | n:, f:(nn). Surj(n; n; f) Inj(n; n; f) |
| THM | surj_is_inj_gen | f:(AB). (A ~ B) & Fin(B) Surj(A; B; f) Inj(A; B; f) |
| THM | homo_is_inj | Auto:Automata(Alph;St), c:(StAlph*).
(q:St. (Result(Auto)c(q)) = q)
& Fin(Alph)
& Fin(St)
& (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y)))
Inj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c) |
| THM | min_is_unique | Auto:Automata(Alph;St).
Con(Auto) & (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & Fin(Alph) & Fin(St)
Auto  A( l.Auto(l) ) |
| def | min_auto | MinAuto(Auto) == A(l.Auto(l)) |
| THM | min_auto_sound | Auto:Automata(Alph;St). LangOf(Auto) = LangOf(MinAuto(Auto)) |
| THM | quo_list_accept | Auto:Automata(Alph;St), l:x,y:Alph*//(x LangOf(Auto)-induced Equiv y). Auto(l)  |
| THM | min_auto_comp | Auto:Automata(Alph;St), l:Alph*.
(Result(MinAuto(Auto))l) = l x,y:Alph*//(x LangOf(Auto)-induced Equiv y) |
| THM | min_auto_con | Auto:Automata(Alph;St). Fin(Alph) & Fin(St) Con(MinAuto(Auto)) |
| THM | lang_eq_imp_quo_eq | A1:Automata(Alph;S1), A2:Automata(Alph;S2).
LangOf(A1) = LangOf(A2)
x,y:Alph*//(x LangOf(A1)-induced Equiv y) = x,y:Alph*//(x LangOf(A2)-induced Equiv y) |
| THM | any_ge_min_auto | Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S).
Fin(Alph)
Fin(St) LangOf(Auto) = LangOf(A) Con(A) |S|  |x,y:Alph*//(x LangOf(Auto)-induced Equiv y)| |
| THM | any_iso_min_auto | Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S).
Fin(Alph)
Fin(S)
Con(A)
(S ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) LangOf(Auto) = LangOf(A) A MinAuto(Auto) |