be the minimal fractional clock value among the tokens of $M'$ and based on this, define $M {{\overset{\text{\tinydef}}{=}}}\{ (p,c-d)\mid (p,c)\in N' \} $. By construction of $M$ we get $M{\longrightarrow_{d}}M'$ and also that $\max({{\it frac}(M)}) = \max({{\it frac}(M')})-d < 1$. Therefore that $1-\max({{\it frac}(M)}) < 1 -d$. Finally, observe that ${{\it frac}(M)}= \{x-d \mid x \in {{\it frac}(M')} \}$ and $0\in{{\it frac}(M)}$. It follows that ${\mathit{abs}_{}(M')}=\emptyset{\mathit{abs}_{}(M)}$ and therefore that ${\mathit{abs}_{}(M)}\in {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(E{\aftergroup\egroup\originalright})}$ and $M\in{[\![E]\!]}$. This means that $M'$ is included in the set on the right in the claim.

[lemma]{}[lemnonstarrotation]{}\[oneclock:rota\] \[lem:nonstarrotation\] Let $\alpha z$ be a simple expression where $\hat{z}=z\in\Sigma$ (the rightmost symbol is not starred). Then, ${[\![(z+1)\alpha]\!]}$ contains a marking $N$ if, and only if, there exists markings $N'\ge N$ and $M$, and a set $S\subseteq [0,1[$ so that

1.  ${{\lvertS\rvert}} = {{\lvert\alpha z\rvert}}$

2.  ${\mathit{abs}_{S}(M)}\in {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(\alpha z{\aftergroup\egroup\originalright})}$

3.  $M{\longrightarrow_{d}}N'$ for $d = 1-\max(S)$.

Suppose markings $N,N',M$, a set $S\subseteq [0,1[$ and $d\in{{\mathbb R}_{\geq 0}}$ so that the conditions 1 to 3 are satisfied. Let $S'{{\overset{\text{\tinydef}}{=}}}\{0\}\cup \{s+d\mid s\in S\setminus\{d\}\}$. Then, ${{\lvertS'\rvert}}={{\lvertS\rvert}}$ and ${\mathit{abs}_{S'}(N')} \in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}((z+1)\alpha{\aftergroup\egroup\originalright})}$, which witnesses that $N\in{[\![(z+1)\alpha]\!]}$.

Conversely, let $N\in{[\![(z+1)\alpha]\!]}$ be a non-empty marking. If ${{\lvert\alpha\rvert}} = 0$, then $N\in{[\![(z+1)]\!]}$ and so ${\mathit{abs}_{S}(N)}\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}((z+1){\aftergroup\egroup\originalright})}$ for $S{{\overset{\text{\tinydef}}{=}}}{{\it frac}(N)}=\{0\}$. This means that 