⁷In its fullest generality, it is well known that associative-commutative rewriting is an NP-complete problem. In programming practice, however, the patterns used as lefthand sides allow much more efficient matching, so that the theoretical limits only apply to “pathological” patterns not encountered in typical programming practice.