Thm* 
Alph,States:Type, a:Automata(Alph;States). InitialState(a) 
States
Thm* A:Type, B:(A
Type), p:a:A
B(a). 2of(p) B(1of(p))
Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A
| DA_init |
Def InitialState(a) == 1of(2of(a))
Thm* |
| pi2 |
Def 2of(t) == t.2
Thm* |
| pi1 |
Def 1of(t) == t.1
Thm* |
About:
 |  |  |  |  |  |  |