AC-unification of higher-order patterns

We present a complete algorithm for the unification of higher-order patterns module the associative-commutative theory of some constants +(1),..., +(n). Given an AC-unification problem over higher-order patterns, the output of the algorithm is a finite set DAG solved forms [9], constrained by some flexible-flexible equations with the same head on both sides. Indeed, in the presence of AC constants, such equations are always solvable, but they have no minimal complete set of unifiers [13]. We prove that the algorithm terminates, is sound, and that any solution of the original unification problem is an instance of one of the computed solutions which satisfies the constraints.