PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
min
auto
comp
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
(Result(MinAuto(Auto))l) = l
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
By:
Unfold `min_auto` 0
Generated subgoal:
1
(Result(A(
l.Auto(l)
))l) = l
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
About:
(Result(A(
l.Auto(l)
))l) = l 
x,y:Alph*//(x LangOf(Auto)-induced Equiv y) (Result(MinAuto(Auto))l) = l x,y:Alph*//(x LangOf(Auto)-induced Equiv y) (Result(A(l.Auto(l)))l) = l x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
