Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. n :

  5. 1-1-Corresp(n;St)

  6. 1-1-Corresp(St;n)

Conclusion:

n:. #(St)=n

Applied Tactic: (Unfold `card` 0 THEN InstConcl [n] ...)
Generated subgoals:

1. 0 < n