PrintForm Definitions det automata Sections AutomataTheory Doc

At: pos states 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. n:
5. n ~ St
6. St ~ n

n:. #(St)=n
By:
Unfold `card` 0
THEN
InstConcl [n]
Generated subgoal:

1 0 < n

About:
existsuniversenatural_numberless_than