PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
quo
append
assoc
1
1
1
1
1.
Alph:
Type
2.
R:
Alph*
Alph*
Prop
3.
EquivRel x,y:Alph*. x R y
4.
x,y,z:Alph*. (x R y)
((z @ x) R (z @ y))
5.
z1:
Alph*
6.
z2:
Alph*
7.
y1:
Alph*
8.
y2:
Alph*
9.
y1 R y2
((z1 @ z2) @ y1) R (z1 @ z2 @ y2)
By:
RWH (RevLemmaC
Thm*
as,bs,cs:T*. ((as @ bs) @ cs) = (as @ (bs @ cs))) 0
Generated subgoal:
1
((z1 @ z2) @ y1) R ((z1 @ z2) @ y2)
About:
((z1 @ z2) @ y1) R ((z1 @ z2) @ y2)
Alph*
x,y,z:Alph*. (x R y) 
((z @ x) R (z @ y))
