PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
quo
append
wf
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.
z:
A*
6.
y:
x,y:A*//(x R y)
z@
y
x,y:A*//(x R y)
By:
Unfold `member` 0
THEN
Analyze 6
Generated subgoal:
1
6.
y1:
A*
7.
y2:
A*
8.
y1 R y2
z@
y1 = z@
y2
x,y:A*//(x R y)
About:
z@
y1 = z@y2 
x,y:A*//(x R y)
A*Prop
x,y,z:A*. (x R y) 
((z @ x) R (z @ y)) z@y x,y:A*//(x R y) z@y1 = z@y2 x,y:A*//(x R y)
