PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
Rl
iff
Rg
1
1.
A:
Type
2.
R:
A*
A*
Prop
3.
EquivRel x,y:A*. x R y
4.
x,y,z:A*. (x R y)
((z @ x) R (z @ y))
5.
g:
(x,y:A*//(x R y))
6.
L:
LangOver(A)
7.
l:A*. L(l)
g(l)
8.
x:
A*
9.
y:
A*
(x L-induced Equiv y)
(x Rg y)
By:
Unfolds [`lang_rel`;`lquo_rel`] 0
THEN
Unfold `mn_quo_append` 0
THEN
Reduce 0
Generated subgoal:
1
(
z:A*. L(z @ x)
L(z @ y))
(
z:A*. g(z @ x)
g(z @ y))
About:
(
z:A*. L(z @ x) 
L(z @ y)) (z:A*. g(z @ x) g(z @ y))
A*Propx,y,z:A*. (x R y) 
((z @ x) R (z @ y))
l:A*. L(l) g(l) (x L-induced Equiv y) (x Rg y) (z:A*. L(z @ x) L(z @ y)) (z:A*. g(z @ x) g(z @ y))
