PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: min is unique 1 1 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
5. St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
6. Fin(Alph)
7. Fin(St)
8. f: StAlph*
9. s:St. (Result(Auto)f(s)) = s

Auto A(l.Auto(l))
By: Unfold `auto_iso` 0
Generated subgoal:

1 f:(St(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))). Bij(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); f) & (s:St, a:Alph. f(Auto(s,a)) = A(l.Auto(l))(f(s),a) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) & f(InitialState(Auto)) = InitialState(A(l.Auto(l))) x,y:Alph*//(x LangOf(Auto)-induced Equiv y) & (s:St. FinalState(Auto)(s) = FinalState(A(l.Auto(l)))(f(s)))

About:
quotientlistlambdauniversefunctionall
equalapplyexistsandbool