\emptyset$.

The following lemmas express the effect of TPN transitions at the level of the region abstraction. state that maximally firing of discrete transitions (the relation ${\xrightarrow{*}_{\textit{Disc}}}$) is computable and monotone. state how to represent timed-step successor markings.

[lemma]{}[lemdiscall]{} \[lem:discall\] \[lem:monotonicity\] For every non-consuming TPN ${\mathcal{N}}$ there are polynomial time computable functions $f: \Sigma \times \Sigma \times \Sigma \to \Sigma$ and $g: \Sigma \times \Sigma \times \Sigma \to \Sigma$ with the following properties.

1.  \[lem:discall-ad1\] $f$ and $g$ are monotone (w.r.t. subset ordering) in each argument.

2.  \[lem:discall-ad2\] $f(\alpha, \beta, x) \supseteq x$ and $g(\alpha, \beta, x) \supseteq x$ for all $\alpha,\beta,x \in \Sigma$.

3.  \[lem:discall-ad3\] Suppose that $E=x_0x_1\dots x_k$ is a simple expression, $\alpha {{\overset{\text{\tinydef}}{=}}}x_0$ and $\beta {{\overset{\text{\tinydef}}{=}}}\bigcup_{i>0} \hat{x}_i$, and $E' = x'_0x'_1\dots x'_k$ is the derived expression defined by conditions:

    1.  $x_0' {{\overset{\text{\tinydef}}{=}}}f(\alpha,\beta,x_0)$,

    2.  $x_i' {{\overset{\text{\tinydef}}{=}}}g(\alpha,\beta,\hat{x}_i)^*$ for $i>0$,

    3.  $x_i'$ carries a star iff $x_i$ does.

    Then ${[\![E']\!]} = \{M'' \mid \exists M \in {[\![E]\!]} \land M{{\xrightarrow{*}_{\textit{Disc}}}}M' \ge M''\}$.

A proof of this statement is in the appendix. It is essentially due to the monotonicity of discrete transition firing in TPN and the fact that iteratively firing transitions must saturate due to the nonconsuming semantics. We first prove 