<s>[INST] Re-write $1 \cdot x$ to $x$. Given the following bi-directional re-write rules (where $1$ is a constant, $^{-1}$ is a unary operator, $\cdot$ is a binary operator, and $x,y,z$ are arbitrary terms):
$$\begin{align*}
x \cdot 1 &= x \\
x \cdot (y \cdot z) &= (x\cdot y) \cdot z \\
x \cdot x^{-1} &= 1
\end{align*}$$
we're asked to prove that $1 \cdot x = x$ (ie, there is a chain $t_0 \to t_1 \to t_3 \to \cdots \to t_n$ with $t_0 = 1\cdot x$, $t_n = x$, and $t_i \to t_{i+1}$ meaning one of the 3 equations above re-writes $t_i$ to $t_{i+1}$ (in either direction)).
After staring at this for a while I'm beginning to doubt whether or not this is possible... can anyone a) confirm this is indeed possible and b) potentially nudge me in the right direction?
 [/INST] Yes, observe that:
\begin{align*}
1 \cdot x &= (x \cdot x^{-1}) \cdot x \\
&= x \cdot \left(x^{-1} \cdot x\right) \\
&= x \cdot \left((x^{-1} \cdot x) \cdot 1\right) \\
&= x \cdot \left((x^{-1} \cdot x) \cdot (x^{-1} \cdot (x^{-1})^{-1}) \right) \\
&= x \cdot \left(((x^{-1} \cdot x) \cdot x^{-1}) \cdot (x^{-1})^{-1} \right) \\
&= x \cdot \left((x^{-1} \cdot (x \cdot x^{-1})) \cdot (x^{-1})^{-1} \right) \\
&= x \cdot \left((x^{-1} \cdot 1) \cdot (x^{-1})^{-1} \right) \\
&= x \cdot \left(x^{-1}\cdot (x^{-1})^{-1} \right) \\
&= x \cdot  1 \\
&= x \\
\end{align*}
</s>