Lemma: Injective event encoding

Let $x$ be a tuple of valid input locations and $\tau (x)$ its transported tuple. For $1\le k\le 2^r-1$, valid event reports, and zero history, the map

is injective and has disjoint input and output sets.

Proof. History determines $x$, and the output counter determines $k$. All other input data are retained. Modes separate the two sets.