PrintForm Definitions automata 5 Sections AutomataTheory Doc

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

1m
By: Analyze 11
Generated subgoal:

111. f: m(x,y:Alph*//R(x,y))
12. g:((x,y:Alph*//R(x,y))m). InvFuns(m; x,y:Alph*//R(x,y); f; g)
13. l:Alph*. LangOf(Auto)(l) g(l)
14. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
1m

About:
natural_numberuniverselistfunctionpropquotient
applyboolallassertimplies