PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
min
auto
con
1
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
Fin(Alph) & Fin(St)
5.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
Con(MinAuto(Auto))
By:
Unfold `connected` 0
THEN
UnivCD
Generated subgoal:
1
6.
s:
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
l:Alph*. (Result(MinAuto(Auto))l) = s
About:
l:Alph*. (Result(MinAuto(Auto))l) = s Con(MinAuto(Auto)) l:Alph*. (Result(MinAuto(Auto))l) = s
