I see this as a general problem in higher dimensional algebra, that there will need to be "higher dimensional rewriting". John Baez has illustrated the higher dimensional thinking by displaying the picture
$$ ||| \;\; ||| || $$ $$||| \;\; ||||| $$
which is easily seen to illustrate $2 \times (3+5)= 2 \times 3 + 2 \times 5$ but the 1-dimensional formula involves various conventions, and is less transparent. We have found diagrammatic rewriting useful in dealing with rotations in double groupoids (with connections), and there is a 3-dimensional rewriting argument in Section 5 of
F.-A. Al-Agl, R. Brown, R. Steiner, `Multiple categories: the equivalence between a globular and cubical approach', Advances in Mathematics, 170 (2002) 71-118.
which proves a key braid relation (Theorem 5.2).
So there is the interesting question of how to cope say with a 5-dimensional rewrite? Maybe computers could handle it?
These situations could well occur in algebras with partial operations whose domains are defined by geometric conditions, and with strict axioms.
