PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
any
iso
min
auto
1
1
2
1
1
1
1
1
1
1
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
S:
Type
5.
A:
Automata(Alph;S)
6.
Fin(Alph)
7.
Fin(S)
8.
Con(A)
9.
S ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
10.
LangOf(Auto) = LangOf(A)
11.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
12.
EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
13.
A
A(
l.A(l)
)
14.
a:
Alph
15.
s1:
Alph*
16.
s2:
Alph*
17.
z:Alph*. LangOf(Auto)(z @ s1)
LangOf(Auto)(z @ s2)
(a.s1) LangOf(Auto)-induced Equiv (a.s2)
By:
Unfold `lang_rel` 0
THEN
Reduce 0
THEN
Analyze 0
Generated subgoal:
1
18.
z:
Alph*
LangOf(Auto)(z @ (a.s1))
LangOf(Auto)(z @ (a.s2))
About:
LangOf(Auto)(z @ (a.s1)) 
LangOf(Auto)(z @ (a.s2))
A(
l.A(l)
)
z:Alph*. LangOf(Auto)(z @ s1) LangOf(Auto)(z @ s2) (a.s1) LangOf(Auto)-induced Equiv (a.s2) LangOf(Auto)(z @ (a.s1)) LangOf(Auto)(z @ (a.s2))
