requiring either $({\mathit{False}_{j}},1)$ or $({\mathit{False}_{k}},1)$, which are not contained in $M_0$ by assumption that $M_{{\boldsymbol{v}}}$ encodes ${\boldsymbol{v}}$. Therefore $({\mathit{False}_{i}},0)\notin M_{n-1}$.

2.  Case ${\boldsymbol{v'}}[i]=0$. W.l.o.g., ${\boldsymbol{v}}[j] =0$. Therefore, $({\mathit{False}_{j}},1) \in (M_{{\boldsymbol{v}}}+1) \le M_{i-1}$. By construction of the net, there exists transition $i.L$ with ${\mathit{Pre}}(i.L) = {({\mathit{False}_{j}},1)}$ and ${\mathit{Post}}(i.L) = {\mathit{Pre}}(i.L) + {({\mathit{False}_{i}},0)}$. This justifies the step $M_{i-1} {\longrightarrow_{i.L}} M_{i}$, with $(False_i, 0) \in M_i\le M_{n-1}$. Notice again that no marking reachable from $M_0$ using only discrete steps can contain the token $({\mathit{True}_{i}},0)$. This is because these can only be produced by transitions $i.B$, requiring both $({\mathit{True}_{j}},1),({\mathit{True}_{k}},1)\in M_{0}$, contradicting our assumptions. Hence, $({\mathit{True}_{i}},0)\notin M_{n-1}$.

We conclude that the constructed marking $M_{n-1}$ is an encoding of ${\boldsymbol{v'}}$.

For the other part of the claim, assume that there exist markings $M_{{\boldsymbol{v}}}$ and $M_{{\boldsymbol{v'}}}$ which are encodings of vectors ${\boldsymbol{v}}$ and ${\boldsymbol{v'}}$, respectively, with $M_{{\boldsymbol{v}}}{\longrightarrow_{1}}{{\xrightarrow{*}_{\textit{Disc}}}}M_{{\boldsymbol{v'}}}$. We will show that $F({\boldsymbol{v}})={\boldsymbol{v}}'$. Recall that $F({\boldsymbol{v}})[i]{{\overset{\text{\tinydef}}{=}}}{\boldsymbol{v}}[j]\otimes {\boldsymbol{v}}[k]$, where $0\le j,k< n$ and $\otimes \in \{\wedge, \vee \}$. We will show for each $i <  n$ that ${\boldsymbol{v}}'[i] = {\boldsymbol{v}}[j]\otimes {\boldsymbol{v}}[k]$. Again, consider the constraint $i'$, and assume w.l.o.g. that $i' = j \land k$ (the other case is analogous). There are two cases.

1.  Case ${\boldsymbol{v'}}[i]=1$. By definition 