Let $q$ be a source query, $\mathbb{K}$ an m-semiring with decidable equality and an alternative linear order, $\hat I$ a $\mathbb{K}$-instance, and $\hat q$ the query obtained from $q$ by applying the rewriting rules bottom up. Then $\langle\!\langle q \rangle\!\rangle_{\hat I} = [\![\hat q]\!]_{\hat I}$: the annotated semantics of $q$ on $\hat I$, read as a plain relation with the annotation in the last column, is the multiset semantics of $\hat q$ on the composite reading of $\hat I$. This is the theorem of the paper restricted to rules (R1) to (R4): the paper's statement also covers the aggregation rule (R5), which this submission does not state; the library proves an analogue of it, on its general syntax with symbolic aggregate tokens, outside the paper's syntax.