At: any ge min auto 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. S: Type
5. A: Automata(Alph;S)
6. Fin(Alph)
7. Fin(St)
8. LangOf(Auto) = LangOf(A)
9. Con(A)
10. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
11. EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
|S| 
|x,y:Alph*//(x LangOf(Auto)-induced Equiv y)|
By: Inst
Thm* 
A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) 
A1 
A2 |S1| |S2|
[Alph;S;x,y:Alph*//(x LangOf(Auto)-induced Equiv y);A;MinAuto(Auto)]
Generated subgoals:| 1 | Con(MinAuto(Auto)) |
| 2 | A MinAuto(Auto) |
About:
