Proving that all equivalent regular expressions are reachable via algebraic laws Given a set of laws for regular expressions, for example (ripped from this document):
$$
\begin{array}{llll}
\text{1.} & (A|B)|C = A|(B|C) &\qquad& \text{(associativity of choice)}\\
\text{2.} & (AB)C = A(BC) && \text{(associativity of sequence)}\\
\text{3.} & A|B = B|A && \text{(commutativity of choice)}\\
\text{4.} & \phi|A = A|\phi = A && \text{(choice with empty language)}\\
\text{5.} & \epsilon A = A\epsilon = A && \text{(sequence with empty string)}\\
\text{6.} & \phi A = A \phi = \phi && \text{(sequence with empty language)}\\
\text{7.} & A(B|C) = AB|AC && \text{(left distributivity)}\\
\text{8.} & (A|B)C = AC|BC && \text{(right distributivity)}\\
\text{9.} & A|A = A && \text{(idempotency of choice)}\\
\text{10.} & (A^*)^* = A^* && \text{(repeated closure)}\\
\text{11.} & \phi^* = \epsilon && \text{(closure of empty language)}\\
\text{12.} & \epsilon^* = \epsilon && \text{(closure of empty string)}\\
\end{array}$$
Now, given any two regular expressions $A$ and $B$ which are equivalent (recognize precisely the same language), is there always a way to rewrite $A$ to $B$ by repeatedly applying these laws as rewriting rules? How would one approach proving that there are no equivalent regular expressions not reachable by rewriting from each other using these laws?
EDIT: As JiK points out, we also need at least $A(A^*) = (A^*)A$, and there might be other necessary rules missing. I guess this just demonstrates why a way to prove reachability between equivalent expressions seems necessary.
 A: This has been an open problem for some years until a negative answer was given independently by Redko [4] and Conway [1, pp. 105-118]): every complete system of identities for the regular expressions is necessarily infinite.
Conway [1, pp. 116-119] conjectured a "good" complete system and this conjecture was ultimately proved by Krob [2, 3]. Interestingly, this system involves identities attached to finite groups.
On the positive side, Salomaa [5] proved that there exists a complete system composed of two identities and of an axiom scheme (which permits essentially to formally solve linear systems). 
[1] J.H. Conway, Regular Algebras and Finite Machines (Chapman & Hall, London, 1974).
[2] D.Krob, A complete system of ${\scr B}$-rational identities. Automata, languages and programming (Coventry, 1990), 60--73, Lecture Notes in Comput. Sci., 443, Springer, New York, 1990.
[3] D.Krob, Complete systems of ${\scr B}$-rational identities. Theoret. Comput. Sci. 89 (1991), no. 2, 207--343. 
[4] V.N. Redko, On the determining totality of an algebra of regular events, Ukrain. Mat. Z. 16 (1964), 120-126 (in Russian).
[5] A. Salomaa, Two complete axiom systems for the algebra of regular events. J. Assoc. Comput. Mach. 13 (1966), 158--169.
