| DISP | auto_iso_df | auto_iso(<A1:first_automation:*>;<S1:first_state_set:*>;
<Alph:alphabet:*>;<S2:second_state_set:*>;<A2:second_automation:*>)
== <A1>  <A2>
<A1:A1:*> <A2:A2:*>== <A1> <A2> |
| ABS | auto_iso | A1 A2 ==
 f:S1   S2
Bij(S1;S2;f)
 ( s:S1. a:Alph. f ( A1 s a) = A2 (f s) a)
f I(A1) = I(A2)
(s:S1. F(A1) s = F(A2) (f s)) |
| THM | auto_iso_wf | Alph,S1,S2: . A1:Automata(Alph;S1). A2:Automata(Alph;S2).
A1 A2   |
| THM | auto_iso_sym | Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2).
A1 A2   A2 A1 |
| DISP | refine_df | refine(<A1:automation_1:*>;<S1:state_set_1:*>;<Alph:alphabet:*>;
<S2:state_set_2:*>;<A2:automation_2:*>)
== <A1>  <A2>
<A1:A1:*> <A2:A2:*> == <A1> <A2> |
| ABS | refine | A1 A2 == x,y:Alph List. A1(x) = A1(y) A2(x) = A2(y) |
| THM | refine_wf | Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2).
A1 A2 |
| DISP | connected_df | connected(<A:automation:*>;<Alph:alphabet:*>;<St:state_set:*>)
== Con(<A>)
Con(<A:A:*>)== Con(<A>) |
| ABS | connected | Con(A) == s:St. l:Alph List. A(l) = s |
| THM | connected_wf | Alph,St:. A:Automata(Alph;St). Con(A) |
| DISP | card_le_df | |<S:S:*>|  |<T:T:*>|== |<S>| |<T>| |
| ABS | card_le | |S| |T| == f:S T. Inj(S;T;f) |
| THM | card_le_wf | S,T:. |S| |T| |
| DISP | card_ge_df | |<S:S:*>|  |<T:T:*>|== |<S>| |<T>| |
| ABS | card_ge | |S| |T| == f:S T. Surj(S;T;f) |
| THM | card_ge_wf | S,T:. |S| |T| |
| COM | le_vs_ge_com |  |S| |T| does not imply |T| |S| |
| THM | refine_ge | Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2).
Con(A1) Con(A2) A1 A2 |S1| |S2| |
| THM | refine_iso | Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2).
Con(A1) Con(A2) L(A1) = L(A2) A1 A2 A2 A1 A1 A2 |
| DISP | lang_auto_df | A(<g:g:*>)== A(<g>) |
| ABS | lang_auto | A(g) == < s,a.(a::s), [], g> |
| THM | lang_auto_wf | Alph:. L:L(Alph). g:x,y:(Alph List)//(x Rl y)  .
A(g) Automata(Alph;x,y:(Alph List)//(x Rl y)) |
| THM | lang_auto_compute | Alph:. L:L(Alph). g:x,y:(Alph List)//(x Rl y) . l:Alph List.
A(g)(l) = l |
| THM | lang_auto_lem | Alph:. L:L(Alph). g:x,y:(Alph List)//(x Rl y) .
(l:Alph List. L l   (g l)) L(A(g)) = L |
| THM | lang_auto_is_min | Alph,St:. Auto:Automata(Alph;St).
g:x,y:(Alph List)//(x Rl y) .
Auto A(g) |
| THM | homo_init | Alph,St:. Auto:Automata(Alph;St).
g:x,y:(Alph List)//(x Rl y) . c:St Alph List.
(q:St. Auto(c q) = q) c I(Auto) = [] |
| THM | homo_step | Alph,St:. Auto:Automata(Alph;St).
g:x,y:(Alph List)//(x Rl y) . c:St Alph List.
(q:St. Auto(c q) = q)
(q:St. a:Alph. c (Auto q a) = A(g) (c q) a) |