that asks that every transition takes at most one token each place, is merely a syntactic convenience. A net satisfying this condition can be constructed by adding a few extra places and intermediate transitions to first distribute tokens to those extra places for the original transition to consume.

So let’s assume w.l.o.g., that ${\mathcal{N}}$ satisfies this condition and let ${\mathcal{N}}'$ be the non-consuming variant derived from ${\mathcal{N}}$ where for all transitions $T$, ${\mathit{Post}}_{{\mathcal{N}}'}(t){{\overset{\text{\tinydef}}{=}}}{\mathit{Post}}_{\mathcal{N}}(t)\oplus{\mathit{Pre}}_{\mathcal{N}}(t)$. Notice that then, for every discrete step $M {\longrightarrow_{t}}M'$ we have that $M \leq M'$. We prove the following claim.

*For every place $p$ and transition $t$ of ${\mathcal{N}}$ there exists $M\in{\mathit{Cover}_{{\mathcal{N}}}({\mathbb{N}}\cdot\{(p,{0}\})}$ enabling $t$ in ${\mathcal{N}}$ if, and only if there exists $M'\in{\mathit{Cover}_{{\mathcal{N}}'}({\mathbb{N}}\cdot\{(p,0)\})}$ that enables $t$ in ${\mathcal{N}}'$.*

The “${\mathcal{N}}\to{\mathcal{N}}'$” direction follows from the observation that the pointwise ordering $\le$ on markings, is a simulation: If $M{\xrightarrow{}}N$ and $M'\ge M$ then there exists an $N'\ge N$ with $M'{\xrightarrow{}}N'$. For the other direction, suppose there exists a witnessing path $$m\cdot\{(p,{0})\}~=~M_0{\xrightarrow{}}M_1{\xrightarrow{}}M_2{\xrightarrow{}}\cdots{\xrightarrow{}}M_k{\xrightarrow{t}}$$ of length $k$ in ${\mathcal{N}}'$. We can inductively derive a witnessing path in ${\mathcal{N}}$ backwards, again using the fact that $\le$ is a simulation. First note that if $M'$ enables $t$, then every $m'\cdot M'$ with $m'>0$ enables 