\doc{Matching}
\ref{matching}
\ref{matches}

A term \fq{t1} is said to \def{match} a term \fq{t2} if it can be transformed
into \fq{t2} by some \glink{substitution}{substitution} of terms for
its variables.  When operators with ac or commutative
\llink{operator-theory}{operator theories} occur in \fq{t1} and \fq{t2}, or 
when \fq{t1} and \fq{t2} contain \llink{quantifier}{quantifiers}, \fq{t1}
matches \fq{t2} in LP if there is a substitution that transforms \fq{t1} into a
term equivalent to \fq{t2} modulo these theories and changes of bound
variables.