PrintForm
Definitions
det
automata
Sections
AutomataTheory
Doc
At:
pos
states
1
1
1
1
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
n:
5.
n ~ St
6.
f:
St
n
7.
g:(
n
St). InvFuns(St;
n; f; g)
8.
n = 0
9.
InitialState(Auto)
St
0 < n
By:
Assert (f(InitialState(Auto))
0)
Generated subgoals:
None
About:
n ~ St
n
g:(nSt). InvFuns(St; n; f; g)
St
0 < n 0)
