Metamath Proof Explorer


Theorem erclwwlkntr

Description: .~ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypotheses erclwwlkn.w
|- W = ( N ClWWalksN G )
erclwwlkn.r
|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion erclwwlkntr
|- ( ( x .~ y /\ y .~ z ) -> x .~ z )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w
 |-  W = ( N ClWWalksN G )
2 erclwwlkn.r
 |-  .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 vex
 |-  x e. _V
4 vex
 |-  y e. _V
5 vex
 |-  z e. _V
6 1 2 erclwwlkneqlen
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
7 6 3adant3
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
8 1 2 erclwwlkneqlen
 |-  ( ( y e. _V /\ z e. _V ) -> ( y .~ z -> ( # ` y ) = ( # ` z ) ) )
9 8 3adant1
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( # ` y ) = ( # ` z ) ) )
10 1 2 erclwwlkneq
 |-  ( ( y e. _V /\ z e. _V ) -> ( y .~ z <-> ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) )
11 10 3adant1
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z <-> ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) )
12 1 2 erclwwlkneq
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y <-> ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) )
13 12 3adant3
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y <-> ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) )
14 simpr1
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> x e. W )
15 simplr2
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> z e. W )
16 oveq2
 |-  ( n = m -> ( y cyclShift n ) = ( y cyclShift m ) )
17 16 eqeq2d
 |-  ( n = m -> ( x = ( y cyclShift n ) <-> x = ( y cyclShift m ) ) )
18 17 cbvrexvw
 |-  ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) <-> E. m e. ( 0 ... N ) x = ( y cyclShift m ) )
19 oveq2
 |-  ( n = k -> ( z cyclShift n ) = ( z cyclShift k ) )
20 19 eqeq2d
 |-  ( n = k -> ( y = ( z cyclShift n ) <-> y = ( z cyclShift k ) ) )
21 20 cbvrexvw
 |-  ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) <-> E. k e. ( 0 ... N ) y = ( z cyclShift k ) )
22 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 22 clwwlknbp
 |-  ( z e. ( N ClWWalksN G ) -> ( z e. Word ( Vtx ` G ) /\ ( # ` z ) = N ) )
24 eqcom
 |-  ( ( # ` z ) = N <-> N = ( # ` z ) )
25 24 biimpi
 |-  ( ( # ` z ) = N -> N = ( # ` z ) )
26 23 25 simpl2im
 |-  ( z e. ( N ClWWalksN G ) -> N = ( # ` z ) )
27 26 1 eleq2s
 |-  ( z e. W -> N = ( # ` z ) )
28 27 ad2antlr
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> N = ( # ` z ) )
29 23 simpld
 |-  ( z e. ( N ClWWalksN G ) -> z e. Word ( Vtx ` G ) )
30 29 1 eleq2s
 |-  ( z e. W -> z e. Word ( Vtx ` G ) )
31 30 ad2antlr
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> z e. Word ( Vtx ` G ) )
32 31 adantl
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> z e. Word ( Vtx ` G ) )
33 simprr
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) )
34 32 33 cshwcsh2id
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
35 oveq2
 |-  ( N = ( # ` z ) -> ( 0 ... N ) = ( 0 ... ( # ` z ) ) )
36 oveq2
 |-  ( ( # ` z ) = ( # ` y ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
37 36 eqcoms
 |-  ( ( # ` y ) = ( # ` z ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
38 37 adantr
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
39 38 adantl
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
40 35 39 sylan9eq
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( 0 ... N ) = ( 0 ... ( # ` y ) ) )
41 40 eleq2d
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( m e. ( 0 ... N ) <-> m e. ( 0 ... ( # ` y ) ) ) )
42 41 anbi1d
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) <-> ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) ) )
43 35 eleq2d
 |-  ( N = ( # ` z ) -> ( k e. ( 0 ... N ) <-> k e. ( 0 ... ( # ` z ) ) ) )
44 43 anbi1d
 |-  ( N = ( # ` z ) -> ( ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) <-> ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) )
45 44 adantr
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) <-> ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) )
46 42 45 anbi12d
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) ) <-> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) ) )
47 35 rexeqdv
 |-  ( N = ( # ` z ) -> ( E. n e. ( 0 ... N ) x = ( z cyclShift n ) <-> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
48 47 adantr
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( E. n e. ( 0 ... N ) x = ( z cyclShift n ) <-> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
49 34 46 48 3imtr4d
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
50 28 49 mpancom
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
51 50 exp5l
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( m e. ( 0 ... N ) -> ( x = ( y cyclShift m ) -> ( k e. ( 0 ... N ) -> ( y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) ) )
52 51 imp41
 |-  ( ( ( ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... N ) ) /\ x = ( y cyclShift m ) ) /\ k e. ( 0 ... N ) ) -> ( y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
53 52 rexlimdva
 |-  ( ( ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... N ) ) /\ x = ( y cyclShift m ) ) -> ( E. k e. ( 0 ... N ) y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
54 53 ex
 |-  ( ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... N ) ) -> ( x = ( y cyclShift m ) -> ( E. k e. ( 0 ... N ) y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
55 54 rexlimdva
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... N ) x = ( y cyclShift m ) -> ( E. k e. ( 0 ... N ) y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
56 21 55 syl7bi
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... N ) x = ( y cyclShift m ) -> ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
57 18 56 syl5bi
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
58 57 exp31
 |-  ( ( x e. W /\ y e. W ) -> ( z e. W -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) ) )
59 58 com15
 |-  ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> ( z e. W -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) ) )
60 59 impcom
 |-  ( ( z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) )
61 60 3adant1
 |-  ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) )
62 61 impcom
 |-  ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
63 62 com13
 |-  ( ( x e. W /\ y e. W ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
64 63 3impia
 |-  ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
65 64 impcom
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) )
66 14 15 65 3jca
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> ( x e. W /\ z e. W /\ E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
67 1 2 erclwwlkneq
 |-  ( ( x e. _V /\ z e. _V ) -> ( x .~ z <-> ( x e. W /\ z e. W /\ E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
68 67 3adant2
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ z <-> ( x e. W /\ z e. W /\ E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
69 66 68 syl5ibrcom
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> x .~ z ) )
70 69 exp31
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> x .~ z ) ) ) )
71 70 com24
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) )
72 71 ex
 |-  ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
73 72 com4t
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
74 13 73 sylbid
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
75 74 com25
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) ) )
76 11 75 sylbid
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) ) )
77 9 76 mpdd
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) )
78 77 com24
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( ( # ` x ) = ( # ` y ) -> ( y .~ z -> x .~ z ) ) ) )
79 7 78 mpdd
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( y .~ z -> x .~ z ) ) )
80 79 impd
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x .~ y /\ y .~ z ) -> x .~ z ) )
81 3 4 5 80 mp3an
 |-  ( ( x .~ y /\ y .~ z ) -> x .~ z )