Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2). Con(A1) Con(A2) L(A1) = L(A2) A1 A2 A2 A1 A1 A2

Applied Tactic: Auto
Generated subgoals:

1. A1 A2