it only for star-free expressions $E$ in condition 3 (\[lem:discall-starfree\]) and then generalize to all simple expressions by induction.

\[def:discall\] We will write ${\mathit{SAT}(E)} {{\overset{\text{\tinydef}}{=}}}E'$ for the successor expression $E'$ of $E$ guaranteed by \[lem:discall\]. I.e., ${\mathit{SAT}(E)}$ is the saturation of $E$ by maximally firing discrete transitions.

Notice that by definition it holds that ${[\![E]\!]} \subseteq {[\![{\mathit{SAT}(E)}]\!]}\subseteq{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E]\!]}{\aftergroup\egroup\originalright})}$, and consequently also that ${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![{\mathit{SAT}(E)}]\!]}{\aftergroup\egroup\originalright})}={\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E]\!]}{\aftergroup\egroup\originalright})}$.

\[lem:simulation\] Suppose that $X=x_0x_1\dots x_k$ is a simple expression of length $k+1$ with ${\mathit{SAT}(X)}=x'_0x'_1\dots x'_k$ and $x_0,x'_0\in\Sigma$. Let $Y=y_0\alpha_1y_1\alpha_2\dots \alpha_k y_k$ be a simple expression with ${\mathit{SAT}(Y)}=y'_0\alpha'_1y'_1\alpha'_2\dots \alpha'_k y'_k$ and $y_0,y'_0\in\Sigma$.

If $\hat{x}_i \subseteq \hat{y}_i$ for all $i\le k$ then $\hat{x}'_i 
    \subseteq
    \hat{y}'_i 
    $ for all $i\le k$.

The assumption of the lemma provides that $\alpha_x{{\overset{\text{\tinydef}}{=}}}x_0 \subseteq \alpha_y{{\overset{\text{\tinydef}}{=}}}y_0$ and $\beta_x{{\overset{\text{\tinydef}}{=}}}\bigcup_{k\ge i>0}\hat{x}_i \subseteq \beta_y{{\overset{\text{\tinydef}}{=}}}\bigcup_{k\ge i>0}\hat{y}_i$. Therefore, by \[lem:discall-ad1\] of \[lem:discall\], we get that $$x'_0 = f(\alpha_x,\beta_x,x_0)
    \quad\subseteq\quad
    f(\alpha_y,\beta_y,y_0)
    =y'_0$$ and similarly, for all $k\ge i\ge 0$, that $\hat{x}'_i = g(\alpha_x,\beta_x,\hat{x}_i)
    ~\subseteq~
    g(\alpha_y,\beta_y,\hat{y}_i)
    = \hat{y}'_i.
    $

For $x\in\Sigma$ we write $(x+1){{\overset{\text{\tinydef}}{=}}}\{(p,{{\it int}(n+1)})\mid (p,n)\in x\}$ for the symbol where token ages are incremented by $1$.

[lemma]{}[lemepsilonsteps]{} \[lem:epsilonsteps\] $
    {[\![\emptyset E]\!]} = 
    \{M' \mid \exists M \in {[\![E]\!]} \land M{\longrightarrow_{d}}M' \land d < 1-\max(frac(M))\}
    $.

*“$\supseteq$”*: Suppose that $M$ is a non-empty 