| 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 | action_auto | Alph,St:. Auto:Automata(Alph;St). l:Alph List.
(<St, l,s.Auto s l>:l I(Auto)) = Auto(l) |
| THM | pos_states | Alph,St:. Auto:Automata(Alph;St). Fin(St) ( n:  . #(St)=n ) |
| THM | reach_lemma | Alph:. S:ActionSet(Alph). si:S.car. nn:. f:nn Alph.
g:Alph nn.
Fin(S.car)
InvFuns(nn;Alph;f;g)
(n:
RL:{y:{x:S.car List| 0 < ||x||  ||x||  n + 1} |
y[(||y|| - 1)] = si}
(s:S.car
(w:Alph List. (S:wsi) = s)  mem_f(S.car;s;RL))
 (||RL|| = n + 1
(i:||RL||. j:i.  (RL[i] = RL[j]))
(s:S.car
mem_f(S.car;s;RL) (w:Alph List. (S:wsi) = s))
(k:
k nn
(RLa:S.car List
(i:{1..||RL|| }. a:Alph.
mem_f(S.car;S.act a RL[i];RL)
mem_f(S.car;S.act a RL[i];RLa))
(a:Alph
g a < k
mem_f(S.car;S.act a hd(RL);RL)
mem_f(S.car;S.act a hd(RL);RLa))
(s:S.car
mem_f(S.car;s;RLa)
(w:Alph List. (S:wsi) = s)))))) |
| THM | reach_aux | Alph:. S:ActionSet(Alph). si:S.car.
Fin(S.car)
Fin(Alph)
(RL:S.car List
s:S.car. (w:Alph List. (S:wsi) = s) mem_f(S.car;s;RL)) |
| THM | reach_list | Alph,St:. Auto:Automata(Alph;St).
Fin(St) Fin(Alph)
(RL:St List
s:St. (w:Alph List. Auto(w) = s) mem_f(St;s;RL)) |
| THM | reach_dec | Alph,St:. Auto:Automata(Alph;St).
Fin(Alph) Fin(St) (s:St. Dec(w:Alph List. Auto(w) = s)) |