Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. S :

  5. A : Automata(Alph;S)

  6. Fin(Alph)

  7. Fin(St)

  8. L(Auto) = L(A)

  9. Con(A)

  10. EquivRel(Alph List;x,y.x Rl y)

  11. EquivRel(Alph List;x,y.x Rl y)

Conclusion:

|S| |x,y:(Alph List)//(x Rl y)|

Applied Tactic: InstLemma `refine_ge` [Alph;S;x,y:(Alph List)//(x Rl y);A;MinAuto(Auto)] THEN Auto
Generated subgoals:

1. Con(MinAuto(Auto))

2. A MinAuto(Auto)