A successful parse is canonical

For every Boolean word $w$ and every finite formula $F$, if the parser described here succeeds on $w$ with result $F$, then $E(F)=w$. The hypothesis is an exact successful parse result, and the conclusion is equality of the entire word, not merely a prefix or a logically equivalent formula. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. The parser $\operatorname{parse}(w)$ works as follows. Its outer recursion starts with fuel $|w|+1$, returns the empty formula on an empty remainder even at fuel zero, and otherwise fails at fuel zero; with positive fuel it parses one clause from the current nonempty remainder using clause fuel equal to that remainder’s length plus one, then recurses on the returned suffix with outer fuel reduced by one. Clause parsing fails at fuel zero; with positive fuel it consumes $[\mathrm{true},\mathrm{true}]$ as the end of an empty remaining clause, or parses one literal and recurses on its suffix with clause fuel reduced by one. Literal parsing requires an initial pair $[\mathrm{false},b]$ for the sign. On the remainder $r$ it starts data fuel $|r|+1$: zero data fuel fails; with positive data fuel $[\mathrm{true},\mathrm{false}]$ ends the digit sequence, while $[\mathrm{false},d]$ contributes digit $d$ and decreases fuel by one; all other cases fail. The collected digits are interpreted little-endian and accepted only if they equal the canonical binary digits of the resulting natural number. A parsed literal is that sign/index pair together with the suffix after its delimiter; any failed subparse makes the containing parse fail. Success of the outer parse requires consuming the complete input. The supplied body is admitted with sorry; no proof of this assertion is supplied there.