PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
12
1
2
2
1
2
1
2
1
1
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)
Fin(St) & (
s:St. Dec(
t:Alph*. (
t.Result(Auto)t)(t) = s))
By:
Analyze 0
Generated subgoals:
1
Fin(St)
2
s:St. Dec(
t:Alph*. (
t.Result(Auto)t)(t) = s)
About:
Fin(St) 
s:St. Dec(
t:Alph*. (
t.Result(Auto)t)(t) = s) Fin(St) & (s:St. Dec(t:Alph*. (t.Result(Auto)t)(t) = s)) Fin(St) s:St. Dec(t:Alph*. (t.Result(Auto)t)(t) = s)
