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.
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.