Auto:Automata(Alph;St)
, g:((x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
). Auto 
A(g)
lang_auto_is_min
A2
== x,y:Alph*. (Result(A1)x) = (Result(A1)y) 
S1 
(Result(A2)x) = (Result(A2)y) S2
Thm* Auto:Automata(Alph;St)
, g:((x,y:Alph*//(x LangOf(Auto)-induced Equiv y))). Auto A(g)
lang_auto_is_min
Thm* A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) LangOf(A1) = LangOf(A2) A1 A2 & A2 A1 A1 
A2
refine_iso
Thm* A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) A1 A2 |S1| 
|S2|
refine_ge