I was wondering what kind of tools are available (if any) for avoiding pages of bracket manipulations in proving associativity properties.
To be concrete, a (more easily stated) analogue of the particular problem I have in mind is:
We have $M$ a magma (a set with a binary operation) and six elements $a, b, c, x, y, z$. I want to prove that $(xy)z = x(yz)$ and I know that
i) right composition with any of $a, b, c$ is injective (e.g. the map $M \to M$ given by $m \mapsto ma$ is injective),
ii) we have the associativity relation for any triple that does not contain two consecutive expressions that contain one of $x, y, z$, (e.g. $z(ab) = (za)b$ and $y((ab)z) = (y(ab))z$),
iii) any pair consisting of one element of $a, b, c$ and one from $z, y, x$ is commutative (e.g. $ax = xa$).
The idea is to convert $x(y(z(a(bc))))$ into $a(x(b(y(cz))))$ where we can then rearrange the brackets.
It feels to me like there should exist a framework for doing this cleanly without having to dirty my hands or the readers eyes with pages of equations (which by the way, I have already written out for my version of the problem and am dreading converting into LaTeX).
A potential framework to my mind is to write such a nested bracketed expression like this as a tree with the $x, y, z, a, b, c$ as leaves. Then the relations i, ii, iii correspond to operations converting one tree to another. In a perfect world, one can prove that my relations are sufficient to generate all possible trees with $a, b, c, x, y, z$ as leaves.