PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: mn 13 1 1 2 1 1 1 1 1
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. Fin(x,y:Alph*//R(x,y))
10. l:Alph*. LangOf(Auto)(l) g(l)
11. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)

Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
By: RWH (LemmaC Thm* Fin(T) (m:. m ~ T)) 9
Generated subgoal:

19. m:. m ~ (x,y:Alph*//R(x,y))
10. l:Alph*. LangOf(Auto)(l) g(l)
11. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))

About:
quotientlistuniverseandfunctionprop
applyboolallassertimplies