%
\label{thm:comp-assoc}
Composition in $\mathcal{P}$ is associative:
for all programs $P, Q, R$,
\[
    \boxed{[R] \circ ([Q] \circ [P])
    = ([R] \circ [Q]) \circ [P].}
\]

Let $P, Q, R$ be programs.

$[R] \circ ([Q] \circ [P])
= [R] \circ [\text{NF}(Q \cdot P)]
= [\text{NF}(R \cdot \text{NF}(Q \cdot P))]$.

$([R] \circ [Q]) \circ [P]
= [\text{NF}(R \cdot Q)] \circ [P]
= [\text{NF}(\text{NF}(R \cdot Q) \cdot P)]$.

By the NF-Confluence Lemma~\ref{lem:nf-confluence},
$\text{NF}(R \cdot \text{NF}(Q \cdot P))
= \text{NF}(R \cdot Q \cdot P)
= \text{NF}(\text{NF}(R \cdot Q) \cdot P)$.
The key step is that normalization commutes with concatenation:
normalizing a sub-expression before concatenating
yields the same final normal form as normalizing the
entire expression at once.
This follows from the confluence of the reduction system.