At: empty lang dec 1 1 1 1 1 1 1 1 1 1 3
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n: 
6.
f:(
n
St). Bij(
n; St; f)
7. l: Alph*
8. FinalState(Auto)((Action(Auto):l
InitialState(Auto)))
l@0:Alph*. (Action(Auto):l@0
InitialState(Auto)) = (Action(Auto):l
InitialState(Auto))
By: Witness l
Generated subgoals:None
About: