The paper's Example 11: the rewriting rules applied bottom up to $q_{\mathrm{city}}$, for any annotation type $\mathbb{K}$, give $\gamma_1[\#2 : \oplus](\Pi_{\#4, \#9}(\sigma_{\#4 = \#8 \wedge \#1 < \#5} (\Pi_{\#1, \dots, \#4, \#6, \dots, \#9, \#5 \otimes \#10}(P \times P))))$, the cross product rewritten by (R2), the projection by (R1) and the duplicate elimination by (R3), the selection carried over to the composite tuples. The claim is that equation, on the queries as syntax; the equality of its two semantics is an instance of the correctness theorem. Attributes are numbered from 0 here, from 1 in the paper.