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?
 A: 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*}
A: Here's a "cool" way to do it (well, at least, I think it's "cool").  If we input the assumptions into the automated theorem prover Prover9:
formulas(assumptions).
  x*1=x.
  x*(y*z)=(x*y)*z.
  x*x'=1.
end_of_list.

formulas(goals).
  1*x=x.
end_of_list.

It will return a proof:
============================== PROOF =================================

% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 12.
% Level of proof is 6.
% Maximum clause weight is 11.
% Given clauses 8.

1 1 * x = x # label(non_clause) # label(goal).  [goal].
2 x * 1 = x.  [assumption].
3 x * (y * z) = (x * y) * z.  [assumption].
4 (x * y) * z = x * (y * z).  [copy(3),flip(a)].
5 x * x' = 1.  [assumption].
6 1 * c1 != c1.  [deny(1)].
7 x * (1 * y) = x * y.  [para(2(a,1),4(a,1,1)),flip(a)].
8 x * (x' * y) = 1 * y.  [para(5(a,1),4(a,1,1)),flip(a)].
13 1 * x'' = x.  [para(5(a,1),8(a,1,2)),rewrite([2(2)]),flip(a)].
15 x * y'' = x * y.  [para(13(a,1),4(a,2,2)),rewrite([2(2)])].
16 1 * x = x.  [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
17 $F.  [resolve(16,a,6,a)].

============================== end of proof ==========================

A: Another method of proof would be:
Using the fact that $x = (x^{-1})^{-1}$, then $x^{-1} \cdot x = 1$ from axiom 3.
\begin{align*}
&1 \cdot 1 = 1 \\
&1 \cdot (x \cdot x^{-1}) = 1 \\
&(1 \cdot x) \cdot x^{-1} = x \cdot x^{-1} \\
&((1 \cdot x) \cdot x^{-1}) \cdot x = (x \cdot x^{-1}) \cdot x \\
&(1 \cdot x) \cdot (x^{-1} \cdot x) = x \cdot (x^{-1} \cdot x) \\
&(1 \cdot x) \cdot 1 = x \cdot 1 \\
&1 \cdot x = x \\
\end{align*}
