Thm* Auto:Automata(Alph;St). Fin(St) (n:. #(St)=n ) pos_states
In prior sections: int 1 int 2 finite sets action sets
Auto:Automata(Alph;St). Fin(St) 
(
n:
. #(St)=n ) pos_states
== {i:
| 0 < i }
Auto:Automata(Alph;St). Fin(St) (n:. #(St)=n ) pos_states