Property 2: grantPoints is not transitive.

For all loyalty applets $L$ and $L'$ it is the case that a call to $\mathit{L.grantPoints}$ never triggers a call to $\mathit{L'.grantPoints}$. That is, the $\mathit{grantPoints}$ method is neither transitive nor recursive.

$$\begin{array}{ll} \phi_{2.1} \;\stackrel {\Delta}{=}& loyalt... ...}\;\mathsf{triggers}\; \\ & loyaltyB.grantPoints \end{array}$$