a,s. 
Auto(s,a) >
Thm* 
Alph,St:Type, Auto:Automata(Alph;St). Action(Auto) 
ActionSet(Alph)
a == 1of(a)
Thm* Alph,States:Type, a:Automata(Alph;States). a States
AlphStates
Thm* A:Type, B:(AType), p:a:A
B(a). 1of(p) A
| auto_action |
Def Action(Auto) == < St,a,s. Auto(s,a) >
Thm* |
| DA_act |
Def a == 1of(a)
Thm* |
| pi1 |
Def 1of(t) == t.1
Thm* |
About:
 |  |  |  |  |
 |  |  |  |  |