At: mn 12 1 2 2 1 2 1 2 2 1 2
1. Alph: Type
2. L: Alph*
Prop
3. Fin(Alph)
4. St: Type
5. Auto: Automata(Alph;St)
6. Fin(St)
7. L = LangOf(Auto)
8. EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)
9. l: Alph*
10. LangOf(Auto)(l)
Auto(l)
By:
Unfold `auto_lang` 10
THEN
Reduce 10
Generated subgoals:None
About:
