| DISP | automata_df | Automata(<Alph:Alph:*><States:States:*>)== Automata(<Alph><States>) |
| ABS | automata | Automata(Alph;States) ==
act:(States   Alph States)  init:States (States  ) |
| THM | automata_wf |  Alph,States: . Automata(Alph;States)  ' |
| DISP | DA_act_df |  <a:DA:E>== <a> |
| ABS | DA_act | a == a.1 |
| THM | DA_act_wf | Alph,States:. a:Automata(Alph;States).
a States Alph States |
| DISP | DA_init_df | I(<a:DA:E>)== I(<a>) |
| ABS | DA_init | I(a) == a.2.1 |
| THM | DA_init_wf | Alph,States:. a:Automata(Alph;States). I(a) States |
| DISP | DA_fin_df | F(<a:DA:E>)== F(<a>) |
| ABS | DA_fin | F(a) == a.2.2 |
| THM | DA_fin_wf | Alph,States:. a:Automata(Alph;States). F(a) States |
| ML | create_automata | Class Declaration for: a Automata(Alph;States)
Long Name: automata
Short Name: DA
Parameters:
Alph :
States :
Fields:
(a) act : States Alph States
(I(a)) init : States
(F(a)) fin : States
Universe: ' |
| DISP | compute_list_df | <DA:DA:*>(<l:list:*>)== <DA>(<l>) |
| ML | compute_list_ml | DA(l)==r if null(l) then I(DA) else DA DA(tl(l)) hd(l) fi |
| THM | compute_list_wf | Alph,St:. A:Automata(Alph;St). l:Alph List. A(l) St |
| THM | compute_list_qwf | Alph,St:. Auto:Automata(Alph;St). l:x,y:(Alph List)//(Auto(x)
= Auto(y)).
Auto(l) St |
| THM | compute_l_inv | Alph,St:. Auto:Automata(Alph;St). x,y,z:Alph List.
Auto(x) = Auto(y)   Auto(z @ x) = Auto(z @ y) |
| DISP | accept_list_df | <DA:DA:*>(<l:l:*>) == <DA>(<l>) |
| ABS | accept_list | DA(l) == F(DA) DA(l) |
| THM | accept_list_wf | Alph,St:. A:Automata(Alph;St). l:Alph List. A(l) |
| THM | accept_list_qwf | Alph,St:. Auto:Automata(Alph;St). l:x,y:(Alph List)//(Auto(x)
= Auto(y)).
Auto(l) |
| DISP | auto_lang_df | L(<DA:DA:*>)== L(<DA>) |
| ABS | auto_lang | L(DA) ==  l. DA(l) |
| THM | auto_lang_wf | Alph,St:. A:Automata(Alph;St). L(A) L(Alph) |
| THM | fin_dec_fin | n: . T:. B:T  .
1-1-Corresp(n;T)  (t:T. Dec(B t))
( m:. 1-1-Corresp(m;{t:T| B t} )) |
| THM | finite_decidable_subset | T:. B:T . Fin(T) (t:T. Dec(B t)) Fin({t:T| B t} ) |
| THM | one_one_preser_fin | T,S:. Fin(T) 1-1-Corresp(T;S) Fin(S) |
| THM | set_function | S,T:. R:S T .
(s:S. Dec(t:T. R s t))
(f:{s:S| t:T. R s t} T. s:{s:S| t:T. R s t} . R s (f s)) |
| THM | inv_of_fin_is_fin | T,S:. f:T S.
Fin(S) (s:S. Dec(t:T. f t = s)) Fin(x,y:T//(f x = f y)) |
| THM | fin_is_decid | T:. Fin(T) (x,y:T. Dec(x = y)) |
| THM | mn_12_old | Alph:. L:L(Alph).
Fin(Alph)
(St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))
(R:{r:Alph List Alph List |
EquivRel(Alph List;x,y.r x y)}
g:x,y:(Alph List)//(R x y)
Fin(x,y:(Alph List)//(R x y))
(l:Alph List. L l  (g l))
(x,y,z:Alph List. R x y R (z @ x) (z @ y))) |
| THM | mn_12 | Alph:. L:L(Alph).
Fin(Alph)
(St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))
(R:Alph List Alph List
EquivRel(Alph List;x,y.x R y)
c (g:x,y:(Alph List)//(R x y)
Fin(x,y:(Alph List)//(R x y))
(l:Alph List. L l (g l))
(x,y,z:Alph List. R x y R (z @ x) (z @ y)))) |
| THM | decid_is_comp | T:. f:T .
(t:T. Dec(f t)) (g:T . t:T. f t (g t)) |
| THM | mn_31 | Alph:. L:L(Alph).
Fin(Alph)
Fin(x,y:(Alph List)//(Rl x y)) (l:Alph List. Dec(L l))
(St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto)) |