At: mn 13 1 1 1 1 2
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. Fin(St)
6. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
LangOf(Auto) = LangOf(Auto)
By:
Unfold `lang_eq` 0
THEN
Fold `languages` 0
Generated subgoals:None
About:
