Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: Auto
Generated subgoals:

1. |S1| |S2|