PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
Rl
iff
Rg
2
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
A*
Prop
By:
Unfold `languages` 6
Generated subgoals:
None
About:
A*
x,y,z:A*. (x R y) 
((z @ x) R (z @ y))
L 
A*
