Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S).
Fin(Alph) 
Fin(S)
Con(A)
(S ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y)))
LangOf(Auto) = LangOf(A) A 
MinAuto(Auto)
any_iso_min_auto
A2
== 
f:(S1
S2).
Bij(S1; S2; f)
& (s:S1, a:Alph. f(
A1(s,a)) = A2(f(s),a))
& f(InitialState(A1)) = InitialState(A2)
& (s:S1. FinalState(A1)(s) = FinalState(A2)(f(s)) 
)
Thm* Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S).
Fin(Alph)
Fin(S)
Con(A)
(S ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y)))
LangOf(Auto) = LangOf(A) A MinAuto(Auto)
any_iso_min_auto
Thm* Auto:Automata(Alph;St).
Con(Auto)
& (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y)))
& Fin(Alph)
& Fin(St)
Auto A(
l.Auto(l)
)
min_is_unique
In prior sections: automata 4