PrintForm
Definitions
det
automata
Sections
AutomataTheory
Doc
At:
pos
states
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
Fin(St)
n:
. #(St)=n
By:
Analyze 4
THEN
RWH (LemmaC
Thm*
(
f:(A
B). Bij(A; B; f))
(A ~ B)) 5
THEN
Inst
Thm*
(T ~ S)
(S ~ T) [
n;St]
Generated subgoal:
1
4.
n:
5.
n ~ St
6.
St ~
n
n:
. #(St)=n
About:
n ~ Stn
n:
. #(St)=n n:. #(St)=n f:(A
B). Bij(A; B; f)) 
(A ~ B))
5
(S ~ T)
[n;St]n ~ Stn n:. #(St)=n 
