In rewrite theory, you often want confluence of your system: if
$$ u_1\leftarrow t\rightarrow u_2$$

Then there is some term $v$ such that
$$ u_1\rightarrow v\leftarrow u_2$$

It is possible to tell whether a set of rewrite rules is confluent by examining the [critical pairs](http://en.wikipedia.org/wiki/Critical_pair_%28logic%29): pairs of rules $t_1\rightarrow u_1,t_2\rightarrow u_2$ and an instance $\theta$ such that

 1. $t'_1\theta = t_2\theta$
 2. $t'_1$ is a subterm of $t_1$ at position $p$.

You can then add the equation $u_1\theta = t_1[u_2\theta]_p$ to make the system confluent.

This suggest an approach to your problem: look at your equations as rewrite rules, then consider the critical pairs: they tell you which equations need to hold to make your system confluent.