label=right:[$i.L$]{}\] [$x=1$]{}; (iR) \[transition, right=of Fk, label=right:[$i.R$]{}\] [$x=1$]{}; (Tj) edge node\[above\][$x$]{} (iB); (Tk) edge node\[above\][$y$]{} (iB); (iB) edge node\[above\][$0$]{} (Ti);

(Fj) edge node\[above\][$x$]{} (iL); (iL) edge node\[above\][$0$]{} (Fi);

(iL) edge node\[above\] (Fj); (iR) edge node\[above\][ ]{}(Fk); (iB) edge node\[above\](Tj); (iB) edge node\[above\](Tk);

(Fk) edge node\[above\][$x$]{} (iR); (iR) edge node\[above\][$0$]{} (Fi);

For every bit $0\le i<n$, the net contains two places ${\mathit{True}_{i}}$ and ${\mathit{False}_{i}}$. A marking $M_{{\boldsymbol{v}}} \le P{\times}{{\mathbb R}_{\geq 0}}$ is an *encoding* of a vector ${\boldsymbol{v}}\in\{0,1\}^n$ if for every $0 \leq i < n$ the following hold.

1.  $({\mathit{True}_{i}},0) \in M_{{\boldsymbol{v}}}\iff {\boldsymbol{v}}[i]=1$.

2.  $({\mathit{False}_{i}},0) \in M_{{\boldsymbol{v}}}\iff {\boldsymbol{v}}[i]=0$.

3.  If $(p,c)\in M_{{\boldsymbol{v}}} $ then $c=0$ or $c\geq 1$.

Note that in particular one cannot have both $({\mathit{True}_{i}},0)$ and $({\mathit{False}_{i}},0)$ in $M_{{\boldsymbol{v}}}$. For every constraint $i'=j\land k$ we introduce three transitions, $i.L, i.R$, and $i.B$, where $$\begin{aligned}
        {\mathit{Pre}}(i.B) &{{\overset{\text{\tinydef}}{=}}}{({\mathit{True}_{j}},x) + ({\mathit{True}_{k}},y)}
        &&
        {\mathit{Post}}(i.B) {{\overset{\text{\tinydef}}{=}}}{\mathit{Pre}}(i.B) + {({\mathit{True}_{i}},0)}\\
        {\mathit{Pre}}(i.L) &{{\overset{\text{\tinydef}}{=}}}{({\mathit{False}_{j}},x)}
        &&
        {\mathit{Post}}(i.L) {{\overset{\text{\tinydef}}{=}}}{\mathit{Pre}}(i.L) + ({\mathit{False}_{i}},0)\\
        {\mathit{Pre}}(i.R) &{{\overset{\text{\tinydef}}{=}}}{({\mathit{False}_{k}},x)}
        &&
        {\mathit{Post}}(i.R) {{\overset{\text{\tinydef}}{=}}}{\mathit{Pre}}(i.R) + ({\mathit{False}_{i}},0)
    \end{aligned}$$ and the guard for all transitions is $G(x)=G(y)=1$. See \[fig:LB\] for an illustration. For disjunctions $i'=j\lor k$ the transitions are defined analogously, with ${\mathit{True}_{}}$ and ${\mathit{False}_{}}$ inverted. The correctness proof of our construction rests on the following simple observation.

[lemma]{}[claimone]{}\[claim1\] 