Is unification of patterns modulo any set of variable-preserving equations decidable?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Unification of patterns (`{a} la [Jouannaud, 1995]) modulo associativity and commutativity has been shown decidable [Jouannaud, 1995], repairing the incomplete solution in [Jouannaud, 1995]. Does it extend to equational theories whose axioms have the same set of variables on left and right hand side?

Recorded update.

Submitted by Evelyne Contejean on Mon Jan 12 15:20:45 MET 1998.

In his conference paper, Qian claimed that he has solved the problem of unifying patterns a la Miller modulo AC, but in fact he never succeeded to prove the completeness of his algorithm. Actually his algorithm is not complete, since he uses a first-order unification algorithm for pure AC-patterns as a black box. The problem was solved last year by Boudet and Contejean [Jouannaud, 1995]: the case of pure AC-patterns requieres is handled in the same spirit as the first order case, by counting things, but technically this is not exactly identical. In [Jouannaud, 1995], the proof of completeness of the algorithm is given. I must admit that [Jouannaud, 1995] takes advantage of the paper of Qian, in particular, the remark that the equations of the form

$$\lambda x_1 ... x_n F(x_1,...,x_n) = \lambda x_1 ... x_n F(x_{\pi(1)},...,x_{\pi(n)})$$

have an infinite set of solutions $\{\sigma_1,\sigma_2,...\}$ such that $\sigma_{i+1}$ is strictly more general than $\sigma_i$. This leads to the notion of constrained solution of a unification problem, and every unification problem of patterns with AC symbols admits a finite complete set of constrained unifiers, and the algorithm proposed in [Jouannaud, 1995] computes such a set.