PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
12
1
2
2
1
2
1
2
1
1
2
1.
Alph:
Type
2.
L:
LangOver(Alph)
3.
Fin(Alph)
4.
St:
Type
5.
Auto:
Automata(Alph;St)
6.
Fin(St)
7.
L = LangOf(Auto)
8.
EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)
s:St. Dec(
t:Alph*. (
t.Result(Auto)t)(t) = s)
By:
Reduce 0
Generated subgoal:
1
s:St. Dec(
t:Alph*. (Result(Auto)t) = s)
About:
s:St. Dec(
t:Alph*. (Result(Auto)t) = s) s:St. Dec(t:Alph*. (
t.Result(Auto)t)(t) = s) s:St. Dec(t:Alph*. (Result(Auto)t) = s)
