| THM | mn_13 |  Alph,St: . Auto:Automata(Alph;St).
Fin(Alph)  Fin(St)   Fin(x,y:(Alph List)//(x Rl y)) |
| THM | Rl_quo_is_decidable | Alph,St:. Auto:Automata(Alph;St).
Fin(Alph) Fin(St) (x,y:Alph List. Dec(x = y)) |
| THM | list_quo_choice_pls | q:  . E:q List   q List  .
EquivRel(q List;x,y.x E y) (x,y:q List. Dec(x E y))
( h:q List q List
(x,y:q List. x E y  h x = h y) (x:q List. x E (h x))) |
| THM | empty_alph_list | q:. x:q List. q = 0 x = [] |
| THM | list_quo_choice | q:. E:q List q List .
EquivRel(q List;x,y.x E y) (x,y:q List. Dec(x E y))
(h:q List q List
(x,y:q List. x E y h x = h y) (x:q List. x E (h x))) |
| THM | fin_alph_list_quo | Alph:. E:Alph List Alph List .
Fin(Alph)
EquivRel(Alph List;x,y.x E y)
(x,y:Alph List. Dec(x E y))
(h:Alph List Alph List
(x,y:Alph List. x E y h x = h y)
(x:Alph List. x E (h x))) |
| THM | homo_is_surj | Alph,St:. Auto:Automata(Alph;St). c:St Alph List.
(q:St. Auto(c q) = q) Fin(Alph) Fin(St)
Surj(St;x,y:(Alph List)//(x Rl y);c) |
| THM | surj_is_inj | n:. f:n n. Surj(n;n;f) Inj(n;n;f) |
| THM | surj_is_inj_gen | A,B:. f:A B.
1-1-Corresp(A;B) Fin(B) Surj(A;B;f) Inj(A;B;f) |
| THM | homo_is_inj | Alph,St:. Auto:Automata(Alph;St). c:St Alph List.
(q:St. Auto(c q) = q)
Fin(Alph)
Fin(St)
1-1-Corresp(St;x,y:(Alph List)//(x Rl y))
Inj(St;x,y:(Alph List)//(x Rl y);c) |
| THM | min_is_unique | Alph,St:. Auto:Automata(Alph;St).
Con(Auto)
1-1-Corresp(St;x,y:(Alph List)//(x Rl y))
Fin(Alph)
Fin(St)
Auto  A( l.Auto(l) ) |
| DISP | min_auto_df | MinAuto(<Auto:Auto:*>)== MinAuto(<Auto>) |
| ABS | min_auto | MinAuto(Auto) == A(l.Auto(l)) |
| THM | min_auto_wf | Alph,St:. Auto:Automata(Alph;St).
MinAuto(Auto)  Automata(Alph;x,y:(Alph List)//(x Rl y)) |
| THM | min_auto_sound | Alph,St:. Auto:Automata(Alph;St). L(Auto) = L(MinAuto(Auto)) |
| THM | quo_list_accept | Alph,St:. Auto:Automata(Alph;St). l:x,y:(Alph List)//(x Rl y).
Auto(l)  |
| THM | min_auto_comp | Alph,St:. Auto:Automata(Alph;St). l:Alph List.
MinAuto(Auto)(l) = l |
| THM | min_auto_con | Alph,St:. Auto:Automata(Alph;St).
Fin(Alph) Fin(St) Con(MinAuto(Auto)) |
| THM | lang_eq_imp_quo_eq | Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2).
L(A1) = L(A2)
x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rl y) |
| THM | any_ge_min_auto | Alph,St:. Auto:Automata(Alph;St). S:. A:Automata(Alph;S).
Fin(Alph)
Fin(St)
L(Auto) = L(A)
Con(A)
|S|  |x,y:(Alph List)//(x Rl y)| |
| THM | any_iso_min_auto | Alph,St:. Auto:Automata(Alph;St). S:. A:Automata(Alph;S).
Fin(Alph)
Fin(S)
Con(A)
1-1-Corresp(S;x,y:(Alph List)//(x Rl y))
L(Auto) = L(A)
A MinAuto(Auto) |