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