PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
min
is
unique
1
1
1
1
1
4
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
5.
St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
6.
Fin(Alph)
7.
Fin(St)
8.
f:
St
Alph*
9.
s:St. (Result(Auto)f(s)) = s
10.
f1:
St
(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
11.
s:
St
q:x,y:Alph*//(x LangOf(Auto)-induced Equiv y). Auto(q)
By:
Analyze 0
Generated subgoal:
1
12.
q:
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
Auto(q)
About:
Auto(q)
Alph*
s:St. (Result(Auto)f(s)) = s(x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) q:x,y:Alph*//(x LangOf(Auto)-induced Equiv y). Auto(q) Auto(q) 
