Occurrence identity

For example, identifying $a_0$ and $a_1$ in

creates a cycle in the quotient although the occurrence graph is acyclic. A concrete rewrite calculus therefore needs an occurrence construction and a residual theorem, not merely equality of local states.