PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
31
1
1
1
1
1
1
1
1
1
1
1
1
1
1
1.
Alph:
Type
2.
L:
LangOver(Alph)
3.
EquivRel x,y:Alph*. x L-induced Equiv y
4.
Fin(Alph)
5.
Fin(x,y:Alph*//L-induced Equiv(x,y))
6.
l:Alph*. Dec(L(l))
7.
g:
Alph*
8.
t:Alph*. L(t)
g(t)
9.
a:
Alph
10.
s1:
Alph*
11.
s2:
Alph*
12.
L-induced Equiv(s1,s2)
L-induced Equiv(a.s1,a.s2)
By:
Unfold `lang_rel` 0
THEN
Reduce 0
THEN
Unfold `lang_rel` -1
THEN
Reduce -1
Generated subgoal:
1
12.
z:Alph*. L(z @ s1)
L(z @ s2)
z:Alph*. L(z @ (a.s1))
L(z @ (a.s2))
About:
z:Alph*. L(z @ s1) 
L(z @ s2)
z:Alph*. L(z @ (a.s1)) L(z @ (a.s2))l:Alph*. Dec(L(l))
t:Alph*. L(t) g(t) L-induced Equiv(a.s1,a.s2)z:Alph*. L(z @ s1) L(z @ s2) z:Alph*. L(z @ (a.s1)) L(z @ (a.s2))
