& = & \{ R\oset{m_R}{\rat}
    Y\mid \exists (L\oset{m_L}{\rat} X), (X\oset{\psi}{\to}
    A).\ \big(\phi = \psi\circ m_L \land \\
    && \qquad (L\oset{m_L}{\rat} X)
    \oset{p}{\Rightarrow} (R\oset{m_R}{\rat} Y)\big)\}
  \end{aligned}$$ ]{}

This result does not yet enable us to construct post-conditions. While the set of co-matches is fully characterized, this can only be achieved by fixing the right-hand side $R$ and thus ensuring that However, as soon as we forget about the co-match, this effect is gone and can only be retrieved by adding annotations, which will be introduced next.

Annotated Objects {#sec:annotated-objects}
=================

We now endow objects with annotations, thus making object languages more expressive. In particular we will use ordered monoids in order to annotate objects. Similar annotations have already been studied in [@k:ver-mobile] in the context of type systems and in [@ckn:graph-languages-type-graphs-journal] with the aim of studying decidability and closure properties, but not for abstract rewriting.

An *ordered monoid* $(\mathcal{M},+,\leq)$ consists of a set $\mathcal{M}$, a partial order $\le$ and a binary operation $+$ such that $(\mathcal{M},+)$ is a monoid with unit $0$ (which is the bottom element wrt. $\le$) and the partial order is compatible with the monoid operation. In particular $a\le b$ implies $a+c\le b+c$ and $c+a\le c+b$ for all 