PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
min
auto
sound
1
1
2
1
2
1
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
l:
Alph*
5.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
6.
(Result(A(
l.FinalState(Auto)(Result(Auto)l)))l) = l
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
7.
z:
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
Auto(z)
By:
Analyze 7
Generated subgoal:
1
7.
z1:
Alph*
8.
z2:
Alph*
9.
z1 LangOf(Auto)-induced Equiv z2
Auto(z1)
= Auto(z2)
About: