Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. S :

  5. A : Automata(Alph;S)

  6. Fin(Alph)

  7. Fin(S)

  8. Con(A)

  9. 1-1-Corresp(S;x,y:(Alph List)//(x Rl y))

  10. L(Auto) = L(A)

Conclusion:

A MinAuto(Auto)

Applied Tactic: InstLemma `lang_rel_equi` [Alph;L(Auto)] THENA Auto THEN InstLemma `lang_rel_equi` [Alph; L(A)] THENA Auto
Generated subgoals:

1. A MinAuto(Auto)