The chosen machine coding is injective and has a total decoder

By [L1], each coded machine $M$ has one definite description tuple $\mathrm{Desc}(M)$ of some fixed length $3+3(m-2)n$, and $<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>$ is exactly the tuple code of that tuple.

A total decoder first uses [L2] to parse the unary arity header and then exactly that many self-delimiting entries. If the parse fails or leaves unread bits, it returns the malformed token; otherwise it recovers one finite tuple of binary words.

If $<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>=<mi\; mathvariant="normal">⌜</mi>N<mi\; mathvariant="normal">⌝</mi>$, then the global injectivity in [L2] gives equality of the decoded tuples, including their arities, so $\mathrm{Desc}(M)=\mathrm{Desc}(N)$. By [L1], that common tuple records the same values of $m$, $s$, $n$, and every transition triple for both machines. Hence $M=N$.

The decoder then checks the shape demanded by [L1]: every entry must be a canonical binary numeral; the tuple must have length $3+3(m-2)n$ for the recovered first three numerals; one must have $m\ge 3$, $n\ge 1$, and $0\le s<n$; and every transition entry must lie in $Q_m\times {\mathrm{\Gamma }}_n\times \{0,1\}$. If any check fails, the decoder returns the malformed token. If all checks pass, those data determine one coded deterministic one-tape machine.

Step 2.1 proves injectivity, and steps 1.2 and 2.2 produce a total decoder. Therefore the chosen machine coding is injective and effectively decodable.