# Proving associativity relations by using a group acting on a set of trees?

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.

-
You need to be more explicit in ii: it is not clear that y((bc)z) or even y(b(cz)) can be arranged to (y(bc))z or (yb)(cz). How do you do that, or do without that? Gerhard "Ask Me About System Design" Paseman, 2011.12.07 – Gerhard Paseman Dec 8 '11 at 6:38
@Gerhard Paseman: True. I apologise, this is an analogous problem to the one I solved, and I didn't translate the hypotheses properly. I've edited the question but its possible that there are still some missing hypotheses. I was hoping the flavour of the problem (independently of its solvability) would be enough to provoke the answer I'm looking for. – name Dec 8 '11 at 7:29
Then essentially Bruce's answer is the way to go. That, or construct the free such object and show it does not have the desired property. Most of my experience has been using the equational route: while converting to trees has been good for visualization, the proofs (for me) don't seem any cleaner. If the real issue is pages of equations, you might be able to refactor your proof and find some useful lemmas. That also takes a while, but is very satisfying when it happens. Gerhard "Ask Me About Finite Bases" Paseman, 2011.12.08 – Gerhard Paseman Dec 8 '11 at 9:32

Thompson's group $F$ is the group "responsible" for associativity relations. It does act on binary trees. I am not sure it will help you much because you would probably have to explain to the readers what Thompson's group is, but in fact proving associativity relation amounts to manipulating with elements of $F$.