At: mn 13 1 1 2 1 1 1 1 1 1 1 3
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph) & Fin(St)
5. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
6. R: Alph*
Alph*Prop
7. EquivRel x,y:Alph*. x R y
8. g: (x,y:Alph*//R(x,y))
9. m: 
10. m ~ (x,y:Alph*//R(x,y))
11. 
l:Alph*. LangOf(Auto)(l) 
g(l)
12. x,y,z:Alph*. R(x,y) 
R((z @ x),z @ y)
13. (
m:. m ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & (l:Alph*. Dec(LangOf(Auto)(l)))
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
By: RWH
(RevLemmaC
Thm* Fin(T) (m:. m ~ T))
13
THENW
(Auto THEN Fold `languages` 0)
Generated subgoals:None
About:
