t(C^{\prime})\left[{x}\coloneqq{v}\right](s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of substitution) $\displaystyle=$ (Definition of wrlp)

Thus, the claim is proven.

######  Lemma C.25.

$\textsf{{wrlp}}\llbracket\textnormal{{diverge}}\rrbracket\left(X\mid\xi\right)=1$.

######  Proof C.26.

We prove by induction on $n$ that
$\textsf{{wrlp}}_{n}\llbracket\textnormal{{diverge}}\rrbracket\left(X\mid\xi\right)=1$.
Then the same holds for the limit.

For the induction base $n=0$, we immediately have
$\textsf{{wrlp}}_{0}\llbracket\textnormal{{diverge}}\rrbracket\left(X\mid\xi\right)=1$.

Now we assume that the statement holds for some arbitrary but fixed $n$ as our
induction hypothesis.

For the induction step, we have:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{diverge}}\rrbracket\left(X\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wrlp}}_{n}\llbracket\textnormal{{diverge}}\rrbracket\left(X\mid\xi\right)\mathbin{{\star}}\xi)$
($\dagger$, see below) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(1\mathbin{{\star}}\xi)$
(Induction Hypothesis) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
1$ (Statement 17)

Now we still miss $\dagger$, which we prove as:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\mid\textnormal{{diverge}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(\textnormal{{diverge}},(s,h))\bigg{\\}}$ (Definition of step)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \sum\left[1\cdot
t(\textnormal{{diverge}})(s,h)\mid\textnormal{{diverge}},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{div}]{1}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\right]$ (Operational semantics of divergence)
$\displaystyle=$ $\displaystyle t(\textnormal{{diverge}})(s,h)$ (Set is
singleton)

Furthermore we have
$\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{diverge}}\rrbracket\left(X\mid\xi\right)\leq
1$ by Lemma B.5. Thus, the claim is proven.

######  Lemma C.29.

For an atomic region free chpGCL program $C$, a mapping $t\colon
C\to\mathbb{E}_{\leq 1}$ and an expectation $X$ with
$\text{Vars}\,(X)\cap\text{Write}(C)=\emptyset$ we have

Step C.30

######  Proof C.32.

First, we notice that due to $\text{Vars}\,(X)\cap\text{Write}(C)=\emptyset$
we have $\text{Vars}\,(X)\subseteq\mathsf{Vars}\setminus\text{Write}(C)$. Now
we prove the claim by structural induction on the program $C$.

For $C=\;\downarrow\;$ we have since
$\text{Act}(\;\downarrow\;,(s,h))=\emptyset$, thus the inequality holds
trivially due to step being bounded by $1$ above (cf. Lemma B.5).

For $C=\textnormal{{diverge}}$ we have (cf. Lemma C.25)

For $C=x\mathrel{\textnormal{{:=}}}e$ we have

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h)\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\left[(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h)\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\text{assign}]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h)\right]$ ($\text{Act}(C,(s,h))$ is singleton)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sum\left[(t(C^{\prime})(s^{\prime},h_{1})\cdot X(s^{\prime},h_{2})\mid
C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[\text{assign}]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h_{1})\right]$ (for any $h_{1}\mathbin{{\star}}h_{2}=h$
and every heap allows the assign action) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\sum\left[(t(C^{\prime})(s^{\prime},h_{1})\cdot X(s,h_{2})\mid
C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[\text{assign}]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h_{1})\right]$ (by Lemmas C.7 and C.10 and
$\text{Vars}\,(X)\subseteq\mathsf{Vars}\setminus\text{Write}(C)$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\left[(t(C^{\prime})(s^{\prime},h_{1})\mid C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[\text{assign}]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h_{1})\right]\cdot X(s,h_{2})$ (Constant factors can be
shifted outside) $\displaystyle=$

Since the inequality holds for all $h_{1}\mathbin{{\star}}h_{2}=h$ we also
have

$\displaystyle\leavevmode\nobreak\ \sup\\{$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ ($

For
$C=\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\}$
the proof is analogous to the case $C=x\mathrel{\textnormal{{:=}}}e$.

For
$C=\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}$
the proof is analogous to the case $C=x\mathrel{\textnormal{{:=}}}e$.

For
$C=\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C^{\prime}}\,\right\\}$
the proof is analogous to the case $C=x\mathrel{\textnormal{{:=}}}e$.

For
$C={x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{0},\dots,e_{n}\right)$
We now have that:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h)\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right\\}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Definition of step) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot\sup\\{t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\\}\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of $\mathbin{{\star}}$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[\sup\\{t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\\}\mid
C,(s,h)\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h))\bigg{\\}}$ (Operational semantics of
allocation) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sup\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})]\Big{|}\leavevmode\nobreak\
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\Big{\\}}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h))\bigg{\\}}$ (Sum over singleton or
empty bag) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\bigg{\\}}$ (Statement
6) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Reducing bag for sum and set for
supremum) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Since
$\text{Act}(C,(s,h_{1}))\supseteq\text{Act}(C,(s,h)$)) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Lemmas C.7 and C.10 and
$\text{Vars}\,(X)\subseteq\mathsf{Vars}\setminus\text{Write}(C)$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Definition of operational semantics)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\mid
C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
\text{alloc-}\ell\in\text{Act}(C,(s,h_{1}))\Big{\\}}\cdot
X(s,h_{2})\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Constant factors can be shifted
outside) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \sup\bigg{\\{}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ ($
(Definition of $\mathbin{{\star}}$)

For $C=\mathtt{free}(x)$ we have

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[(t(C^{\prime})\mathbin{{\star}}X)(s,h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Operational semantics of disposal) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[\sup\\{t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h^{\prime}_{2})\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\\}\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of $\mathbin{{\star}}$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sup\left\\{\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime})]\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\right\\}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Sum over singleton or empty bag)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\left\\{\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime})]\mid
a\in\text{Act}(C,(s,h))\right\\}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\bigg{\\}}$ (Statement
6) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Reducing the bag for sum)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Since either
$\\{\text{free}\\}=\text{Act}(C,(s,h_{1})),\text{Act}(C,(s,h))$ or
$\\{\text{free-abt}\\}=\text{Act}(C,(s,h_{1}))$) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime}_{1})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Operational semantics of disposal)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\mid
C,(s,h_{1})\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\cdot
X(s,h_{2})\;\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Constant factors can be shifted
outside) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \sup\bigg{\\{}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ ($
(Definition of $\mathbin{{\star}}$)

For $C=x\mathrel{\textnormal{{:=}}}\texttt{<}\,e\,\texttt{>}$ we have

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Operational semantics of lookup) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[\sup\\{t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\\}\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of $\mathbin{{\star}}$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sup\left\\{\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s^{\prime},h^{\prime})]\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\right\\}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Sum over singleton or empty bag)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\left\\{\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s^{\prime},h^{\prime})]\mid
a\in\text{Act}(C,(s,h))\right\\}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\bigg{\\}}$ (Statement
6) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h_{2})\mid
C,(s^{\prime},h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Reducing the bag for sum)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s^{\prime},h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Since either
$\\{\text{lookup}\\}=\text{Act}(C,(s,h_{1})),\text{Act}(C,(s,h))$ or
$\\{\text{lookup-abt}\\}=\text{Act}(C,(s,h_{1}))$) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s^{\prime},h_{2})\mid C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Operational semantics of lookup)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Lemmas C.7 and C.10 and
$\text{Vars}\,(X)\subseteq\mathsf{Vars}\setminus\text{Write}(C)$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s^{\prime},h^{\prime}_{1})\mid
C,(s,h_{1})\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\cdot
X(s,h_{2})\;\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Constant factors can be shifted
outside) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \sup\bigg{\\{}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ ($
(Definition of $\mathbin{{\star}}$)

For $C=\texttt{<}\,e\,\texttt{>}\mathrel{\textnormal{{:=}}}e^{\prime}$ we have

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[(t(C^{\prime})\mathbin{{\star}}X)(s,h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Operational semantics of mutation) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[\sup\\{t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h^{\prime}_{2})\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\\}\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of $\mathbin{{\star}}$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sup\left\\{\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime})]\mid
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\right\\}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Sum over singleton or empty bag)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\left\\{\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h^{\prime}_{2})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime})]\mid
a\in\text{Act}(C,(s,h))\right\\}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
h^{\prime}_{1}\mathbin{{\star}}h^{\prime}_{2}=h^{\prime}\bigg{\\}}$ (Statement
6) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Reducing the bag for sum)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1}\mathbin{{\star}}h_{2})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1}\mathbin{{\star}}h_{2})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Since either
$\\{\text{mutation}\\}=\text{Act}(C,(s,h_{1})),\text{Act}(C,(s,h))$ or
$\\{\text{mutation-abt}\\}=\text{Act}(C,(s,h_{1}))$) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\cdot
X(s,h_{2})\mid C,(s,h_{1})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime}_{1})]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Operational semantics of mutation)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\bigg{\\{}\inf\Big{\\{}\sum[t(C^{\prime})(s,h^{\prime}_{1})\mid
C,(s,h_{1})\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime}_{1})]$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h_{1}))\Big{\\}}\cdot
X(s,h_{2})\;\bigg{|}\leavevmode\nobreak\
h_{1}\mathbin{{\star}}h_{2}=h\bigg{\\}}$ (Constant factors can be shifted
outside) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \sup\bigg{\\{}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ ($
(Definition of $\mathbin{{\star}}$)

Now we assume as induction hypothesis that for arbitrary but fixed $C_{1}$ and
$C_{2}$ the assumption already holds.

For $C={C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}}$ we have two cases, either
$C_{1}=\;\downarrow\;$ or $C_{1}\neq\;\downarrow\;$. We only consider the case
that $C_{1}\neq\;\downarrow\;$, since the case $C_{1}=\;\downarrow\;$ is
analogous.

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot(t({C_{1}^{\prime}}{\,;}\leavevmode\nobreak\
{C_{2}})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})\Big{]}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Operational semantics of sequential
composition and assumption that $C_{1}\neq\;\downarrow\;$) $\displaystyle=$
(Definition of step) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ ($
(Induction Hypothesis) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\ ($
(Analogous to the previous transformation)

For $C=\left.C_{1}\;\middle\|\;C_{2}\right.$ we have four cases, one for every
case that we have for any $i=1$ or $i=2$ either $C_{i}\neq\;\downarrow\;$ or
$C_{i}=\;\downarrow\;$. We first prove it for the case that
$C_{1}\neq\;\downarrow\;$ and $C_{2}\neq\;\downarrow\;$. Other cases are
analogous.

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(t(C^{\prime})\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\Bigg{\\{}\inf\bigg{\\{}\sum\left[p\cdot(t(\left.C_{1}^{\prime}\;\middle\|\;C_{2}\right.)\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C_{1},(s,h))\bigg{\\}},$ $\displaystyle\leavevmode\nobreak\
\qquad\inf\bigg{\\{}\sum\left[p\cdot(t(\left.C_{1}\;\middle\|\;C_{2}^{\prime}\right.)\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C_{2},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{2}^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C_{2},(s,h))\bigg{\\}}\Bigg{\\}}$ (Statement 4)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \inf\Bigg{\\{}$
(Definition of step) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\inf\Bigg{\\{}($ (Induction Hypothesis) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\Bigg{\\{}\sup\big{\\{}($
$\displaystyle\leavevmode\nobreak\ \qquad\leavevmode\nobreak\ \sup\big{\\{}($
(Definition of $\mathbin{{\star}}$) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\ \sup\Bigg{\\{}\inf\big{\\{}($ (Statement 6)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \sup\left\\{\right\\}$
(Similar to the previos transformation) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ ($ (Definition of $\mathbin{{\star}}$)

Thus, the claim is proven.

######  Lemma C.68.

For a chpGCL program $C$ and expectations $X$ and $Y$ with
$\text{Vars}\,(X)\cap\text{Write}(C)=\emptyset$ we have

$\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)\mathbin{{\star}}X\quad\leq\quad\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}X\right)\leavevmode\nobreak\ .$

######  Proof C.69.

We have $\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)=\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)$ by Theorem B.23.
Furthermore, if for all $n$ we have $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X\leq\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mathbin{{\star}}Y\mid\left[{\textsf{{{emp}}}}\right]\right)$
we also have that $\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X\leq\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)$.
We prove the claim now by a nested induction. The first induction is on the
level of atomic regions.

We now assume that $C$ does not have any atomic regions. The second induction
is on $n$, For the base case $n=0$, we prove now first that
$\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X=1\mathbin{{\star}}X\leq
1=\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)$.
Next, we assume that the claim holds for a fixed but arbitrary $n$ as our
induction hypothesis $\dagger$. For our induction step, we have that either
$C=\;\downarrow\;$ in which case
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)=Y\mathbin{{\star}}X=\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X$.
For the other case that $C\neq\;\downarrow\;$ we have:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)$
$\displaystyle=$ ($\left[{\textsf{{{emp}}}}\right]$ is neutral element)
$\displaystyle\geq$ (Induction Hypothesis $\dagger$ and monotonicity of step)
$\displaystyle\geq$ (Lemma C.29) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X$
($\left[{\textsf{{{emp}}}}\right]$ is neutral element)

Next we assume that the claim holds for an arbitrary but fixed level of atomic
regions in the program $C^{\prime}$ as our induction hypothesis $\spadesuit$.

We again prove the induction step by an induction over $n$. For the induction
basis we have $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X=1\mathbin{{\star}}X\leq
1=\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)$.
Thus, we assume that the claim holds for a fixed but arbitrary $n$ as our
induction hypothesis $\dagger\dagger$. For the induction step we have two
cases. If $C=\;\downarrow\;$ we have
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)=Y\mathbin{{\star}}X=\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X$
and if $C\neq\;\downarrow\;$ we have:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)$
$\displaystyle=$ ($\left[{\textsf{{{emp}}}}\right]$ is neutral element)
$\displaystyle\geq$ (Left to prove) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)\mathbin{{\star}}X$
($\left[{\textsf{{{emp}}}}\right]$ is neutral element)

We require a similar proof as in Lemma C.29 together with our induction
hypothesis $\dagger\dagger$ to prove the left to prove part. There we only
miss the case for atomic regions. Thus, we assume
$C=\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\}$ and prove first for
$n=0$ that:

$\displaystyle=$ (Case assumption) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot\textsf{{wrlp}}_{0}\llbracket
C^{\prime\prime}\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime},h^{\prime})\Big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Definition of step) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\sum\left[p\cdot\textsf{{wrlp}}_{0}\llbracket
C^{\prime\prime}\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime},h^{\prime})\right]$ (Operational semantics of
atomic regions) $\displaystyle=$
$\displaystyle\quad\sum\left[p\cdot\textsf{{wrlp}}_{0}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot\textsf{{wrlp}}_{0}\llbracket\textnormal{{diverge}}\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\quad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}$ (Separating terminating and diverging
pathes) $\displaystyle=$
$\displaystyle\quad\sum\left[p\cdot\textsf{{wrlp}}_{0}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot 1\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}$ ($\textsf{{wrlp}}_{0}$ is always $1$)
$\displaystyle=$ $\displaystyle\quad\sum\left[p\cdot
1\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot 1\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}$ ($\textsf{{wrlp}}_{0}$ is always $1$)
$\displaystyle=$ $\displaystyle\quad\sum\left[p\cdot 1\mid
C^{\prime},(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot 1\Big{|}\leavevmode\nobreak\
C^{\prime},(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\Big{\\}}$ (Operational semantics of atomic
regions) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C^{\prime}\rrbracket\left(1\right)$ (Definition of
wlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C^{\prime}\rrbracket\left(1\mathbin{{\star}}X\right)$
(Monotonicitiy of wlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C^{\prime}\rrbracket\left(1\right)\mathbin{{\star}}X$
($\spadesuit$) $\displaystyle=$ (Similar to above)

and next for $n>0$ that:

$\displaystyle=$ (Case assumption) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot\textsf{{wrlp}}_{n}\llbracket
C^{\prime\prime}\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime},h^{\prime})\Big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Definition of step) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\sum\left[p\cdot\textsf{{wrlp}}_{n}\llbracket
C^{\prime\prime}\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime},h^{\prime})\right]$ (Operational semantics of
atomic regions) $\displaystyle=$
$\displaystyle\quad\sum\left[p\cdot\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot\textsf{{wrlp}}_{n}\llbracket\textnormal{{diverge}}\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\quad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}$ (Separating terminating and diverging
pathes) $\displaystyle=$
$\displaystyle\quad\sum\left[p\cdot\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot 1\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}$ (Lemma C.25) $\displaystyle=$
$\displaystyle\quad\sum\left[p\cdot(Y\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot 1\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}$ ($\textsf{{wrlp}}_{n}$ of
$\;\downarrow\;$ is always the postexpectation for $n>0$) $\displaystyle=$
$\displaystyle\quad\sum\left[p\cdot(Y\mathbin{{\star}}X)(s^{\prime},h^{\prime})\mid
C^{\prime},(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot 1\Big{|}\leavevmode\nobreak\
C^{\prime},(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\Big{]}$ (Operational semantics of atomic
regions) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C^{\prime}\rrbracket\left(Y\mathbin{{\star}}X\right)$
(Definition of wlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C^{\prime}\rrbracket\left(Y\right)\mathbin{{\star}}X$
($\spadesuit$) $\displaystyle=$ (Similar to above)

Thus, the claim is proven.

######  Theorem C.81.

For an chpGCL program $C$, a mapping
$t\colon\textnormal{{{chpGCL}}}\to\mathbb{E}_{\leq 1}$ and an expectation $X$
with $\text{Vars}\,(X)\cap\text{Write}(C)=\emptyset$ we have

Step C.82

######  Proof C.84.

Follows from Lemmas C.29 and C.68 by structural induction on the program $C$.

##  Appendix D Proofs for Conservativity Properties

######  Lemma D.1 (Conservativeness of qualitative wrlp).

For qualitative $X$ and non-probabilistic program $C$ we have

$\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\in\\{0,1\\}\leavevmode\nobreak\ .$

######  Proof D.2.

The factor $p$ in step is always $1$ due to the absence of probabilistic
constructs in $C$. The countable sum in step inflates to a sum of singleton or
to the empty set. The sum of an empty set is $0$, the sum of a singleton is
the value of its only element. From this point, the rest is a straight forward
induction on $n$.

######  Definition D.3 (Framing Enabled Programs).

A non-probabilistic program $C$ is framing enabled if for their respective
$MDP$ semantics we have for all states $C,(s,h)$, all heaps $h_{F}$ with
$h\mathrel{\bot}h_{F}$ and all enabled actions
$a\in\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))$ that if there exists
$C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})$ then also
$C,(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$.

######  Theorem D.4.

Every non-probabilistic chpGCL program $C$ is framing enabled.

######  Proof D.5.

We prove this by induction over the structure of $C$.

For the terminated program, non-terminating program, assignment, sequential
composition, atomic region, conditional choice, loop, disposal, lookup and
mutation we have $|\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))|\leq 1$. If
$\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))=\emptyset$ the claim holds
immediately. Thus we assume that
$\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))=\\{a\\}$. Now we furthermore assume
that $C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s,h^{\prime})$ to show that the framing enabled condition holds.
Then we also have for all these programs that $\text{Act}(C,(s,h))=\\{a\\}$.
Now let $\varphi(s^{\prime\prime},h^{\prime\prime})=1$ iff
$s^{\prime\prime}=s^{\prime}$, $h^{\prime\prime}=h^{\prime}$ and
$\psi(s^{\prime\prime},h^{\prime\prime})=1$ iff $h^{\prime\prime}=h_{F}$. If
then the premise that $C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime})$ is not
satisfied. Thus we have that due to Lemma D.1. Then we also have that $1=($
due to Theorem C.81. Then

implies $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[(\varphi\mathbin{{\star}}\psi)(s^{\prime\prime},h^{\prime\prime})\mid
C,(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime\prime},h^{\prime\prime})\right]$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))\bigg{\\}}=1$ (Definition of
qualitative step) implies $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[\varphi(s^{\prime},h^{\prime})\cdot\psi(s^{\prime},h_{F})\mid
C,(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})\right]$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))\bigg{\\}}=1$ (Definition of
qualitative $\mathbin{{\star}}$, $\varphi$ and $\psi$)

which proves the claim, as the last equation can only be true if for (the
only) action $a\in\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))$ we have
$C,(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$.

For allocation and for all
$a\in\text{Act}({x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{1}\dots
e_{n}\right),(s,h\mathbin{{\star}}h_{F}))$, where we have that
${x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{1}\dots
e_{n}\right),(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
\;\downarrow\;,(s,h\mathbin{{\star}}h_{a})$, we have since the action is
enabled for $h\mathbin{{\star}}h_{F}$ also that
${x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{1}\dots
e_{n}\right),(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
\;\downarrow\;,(s,h\mathbin{{\star}}h_{a}\mathbin{{\star}}h_{F})$, which
proves the claim.

Now we assume that the statement holds for arbitrary but fixed programs
$C_{1}$ and $C_{2}$.

For sequential composition we have that if $C_{1}\neq\;\downarrow\;$ and
${C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\ {C_{2}},(s^{\prime},h^{\prime})$
then also $C_{1},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})$. By induction hypothesis
$C_{1},(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$ and thus also
${C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}},(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\
{C_{2}},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$. The case that
$C_{1}=\;\downarrow\;$ is analogous.

For concurrency we have that if
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[C1,a]{1}\leavevmode\nobreak\
\left.C_{1}^{\prime}\;\middle\|\;C_{2}\right.,(s^{\prime},h^{\prime})$, then
we also have $C_{1},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C_{1}^{\prime},(s^{\prime},h^{\prime})$
and by the induction hypothesis
$C_{1},(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$ and thus also
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[C1,a]{1}\leavevmode\nobreak\
\left.C_{1}^{\prime}\;\middle\|\;C_{2}\right.,(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$.
The case where we have
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[C2,a]{1}\leavevmode\nobreak\
\left.C_{1}^{\prime}\;\middle\|\;C_{2}\right.,(s^{\prime},h^{\prime})$ is
analogous and the case where we have
$\left.\;\downarrow\;\;\middle\|\;\;\downarrow\;\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[con-end]{1}\leavevmode\nobreak\ \;\downarrow\;,(s,h)$ holds
trivially.

Thus the claim is proven.

See 4.1

See 2

######  Proof D.11.

Remark that step simplifies for non-probabilistic programs to

(30)

We will first show that $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$ satisfies all of these criteria
for non-probabilistic and framing enabled programs:

  1. 1.

For $n=0$ we have $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$, thus this criteria is
satisfied.

  2. 2.

For $n>0$ and $C=\;\downarrow\;$ we have
$\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(\varphi\mid\xi\right)(s,h)=\varphi(s,h)$,
thus $\textsf{{wrlp}}_{n}$ is $1$ if and only if $\varphi(s,h)=1$.

  3. 3.

For $n>0$ and for all $h_{\xi}$ and $h_{F}$ with $\xi(s,h_{\xi})=1$ and
$h\mathrel{\bot}h_{\xi}\mathrel{\bot}h_{F}$ and that
$\textsf{{wrlp}}_{n}\llbracket C\rrbracket\left(X\mid\xi\right)(s,h)=1$ then
for all actions $a$ we do not have
$C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ \textnormal{{abort}}$, since else  by
LABEL:eq:simple-step and $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)(s,h)=0$, which contradicts our assumption.
Finally since $C$ is framing enabled we also get that we do not have
$C,(s,h\mathbin{{\star}}h_{\xi}\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ \textnormal{{abort}}$ as well.

  4. 4.

For $n>0$ we have that if $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$, then for all $h_{\xi}$ with
$\xi(s,h_{\xi})=1$ we have  by definition of wrlp and the magic wand.
Furthermore, for all transitions
$C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s^{\prime},h^{\prime})$ we
have $h^{\prime}=h^{\prime\prime}\mathbin{{\star}}h_{\xi}^{\prime}$ with
$\xi(s^{\prime},h_{\xi}^{\prime})=1$ and $\textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(\varphi\mid\xi\right)(s^{\prime},h^{\prime\prime})=1$
due to the separating multiplication with $\xi$. Finally since $C$ is framing
enabled, we also have this argument for
$C,(s,h\mathbin{{\star}}h_{\xi}\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$, finishing this
direction.

Next we show that if all four criteria hold, then
$\textsf{{wrlp}}_{n}\llbracket C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$:

  1. 1.

if $n=0$ then $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$ holds always.

  2. 2.

if $n>0$ and $C=\;\downarrow\;$ then
$\varphi(s,h)=1=\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)$.

  3. 3.

if $n>0$ and $C\neq\;\downarrow\;$ then we especially have for all $h_{\xi}$
with $\xi(s,h_{\xi})=1$ that the transition $C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ \textnormal{{abort}}$ does not hold;
but all three $C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{\xi}^{\prime})$;
$\textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(\varphi\mid\xi\right)(s^{\prime},h^{\prime})=1$; and
$\xi(s^{\prime},h_{\xi}^{\prime})=1$ does hold. Then we have:

$\displaystyle=$
$\displaystyle\inf\left\\{0\,\middle|\,C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ \textnormal{{abort}}\right\\}$
$\displaystyle\cup\left\\{(\textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(\varphi\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime}\mathbin{{\star}}h_{\xi}^{\prime})\,\middle|\,C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{\xi}^{\prime})\right\\}$
(LABEL:eq:simple-step) $\displaystyle\geq$
$\displaystyle\inf\left\\{0\,\middle|\,C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ \textnormal{{abort}}\right\\}$
$\displaystyle\cup\left\\{\textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(\varphi\mid\xi\right)(s^{\prime},h^{\prime})\,\middle|\,C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{\xi}^{\prime})\right\\}$
(Simplifying the separating multiplication) $\displaystyle=$
$\displaystyle\inf\left\\{\textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(\varphi\mid\xi\right)(s^{\prime},h^{\prime})\,\middle|\leavevmode\nobreak\
\,C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{\xi}^{\prime})\right\\}$
(Emptyset eliminiation) $\displaystyle=$
$\displaystyle\inf\left\\{1\,\middle|\leavevmode\nobreak\
\,C,(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{\xi}^{\prime})\right\\}$
(Criteria assumption) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
1\leavevmode\nobreak\ .$

We have that for all $h_{\xi}$ with $\xi(s,h_{\xi})=1$ the above holds,
therefore we can now combine it with the magic wand and receive

$\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)=\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)(s,h)=1\leavevmode\nobreak\
.$

Lastly, we can put everything together:

$\displaystyle\psi\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(\varphi\mid\xi\right)$ iff
$\displaystyle\forall(s,h).\leavevmode\nobreak\
\psi(s,h)=1\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$ (Both
sides are qualitative) iff $\displaystyle\forall(s,h).\leavevmode\nobreak\
\psi(s,h)=1\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
\inf\\{\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)\mid n\in\mathbb{N}\\}=1$ (Lemma
B.13) iff $\displaystyle\forall(s,h).\leavevmode\nobreak\
\psi(s,h)=1\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \forall
n\in\mathbb{N}.\leavevmode\nobreak\ \textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\varphi\mid\xi\right)(s,h)=1$ (Analysis) iff
$\displaystyle\forall(s,h).\leavevmode\nobreak\
\psi(s,h)=1\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \forall
n\in\mathbb{N}.\leavevmode\nobreak\ \text{safe}_{n}(C,s,h,\xi,\varphi)$ (See
above) iff $\displaystyle\xi\models\\{\psi\\}\;C\;\\{\varphi\\}$ (Definition
4.1)

Thus finishing the proof.

##  Appendix E Soundness Proofs for all Proof Rules

######  Lemma E.1 (Monotonicity of wrlp).

If $Y\leq Z$ then $\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)\leq\textsf{{wrlp}}\llbracket
C\rrbracket\left(Z\mid\xi\right)$.

######  Proof E.2.

We prove by induction on $n$ that $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Z\mid\xi\right)$. If this holds, the inequality for their
limits hold as well.

For the base case $n=0$ we have $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mid\xi\right)=1=\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Z\mid\xi\right)$.

We now assume that the claim holds for some arbitrary but fixed $n$ as our
induction hypothesis.

For $n+1$ we have two cases. The case $C=\;\downarrow\;$ is again trivial,
since
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)=Y\leq
Z=\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Z\mid\xi\right)$.
Finally, for $C\neq\;\downarrow\;$ we have:

$\displaystyle\leavevmode\nobreak\ Y\leq Z$ implies
$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Z\mid\xi\right)$ (Induction Hypothesis) implies
$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi\leq\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Z\mid\xi\right)\mathbin{{\star}}\xi$ (Monotonicity
of $\mathbin{{\star}}$) implies (Monotonicity of step, see Lemma B.1) implies
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle\leavevmode\nobreak\
\leq\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Monotonicity of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$)
implies $\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mid\xi\right)\leq\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Z\mid\xi\right)$ (Definition of wrlp)

This concludes the proof.

######  Definition E.7.

A program $C$ is a terminating atom if for all stack heap pairs $s,h$, all
enabled actions $a\in\text{Act}(C,(s,h))$ and probabilities $p$ we have

$C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\qquad\text{or}\qquad
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}\leavevmode\nobreak\ .$

######  Lemma E.8.

For terminating atom $C$, if $X\leq\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)$ then also $X\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$.

######  Proof E.9.

We show that the statement $X\leq\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ holds for all $n$. For $n=0$ we have
$\textsf{{wrlp}}_{0}\llbracket C\rrbracket\left(Y\mid\xi\right)=1$, thus the
claim holds immediately. Since $C$ is a terminating atom, we have . With this,
we can prove the case $n=1$:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{1}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wlp}}\llbracket
C\rrbracket\left(1\mathbin{{\star}}\xi\right)$ ($C$ is a terminating atom)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wlp}}\llbracket
C\rrbracket\left(1\right)\mathbin{{\star}}\xi)$ (Lemma C.68)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)\mathbin{{\star}}\xi)$ (Monotonicity)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C\rrbracket\left(Y\right)$ (Statement 17)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ X$ (Assumption)

and $n>1$:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp, $C$ is a terminating atom and $n-1>0$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\right)$ ($C$ is a terminating atom)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)\mathbin{{\star}}\xi)$ (Lemma C.68)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}\llbracket C\rrbracket\left(Y\right)$ (Statement 17)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ X$ (Assumption)

Thus, the proof is finished.

######  Lemma E.15.

If $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)$ and $Y\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)$ then also for the sequential composition
$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket{C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)$.

######  Proof E.16.

We prove by induction on $n$ that

$\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket{C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)\leavevmode\nobreak\ .$

If this holds, the inequality also holds for their limits. Finally, we can use
monotonicity of wrlp to prove that the claim holds.

For the induction base with $n=0$, we have $\textsf{{wrlp}}_{0}\llbracket
C_{1}\rrbracket\left(\textsf{{wrlp}}_{0}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)\mid\xi\right)=1=\textsf{{wrlp}}_{0}\llbracket{C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)$.

We assume that the claim holds for some arbitrary but fixed $n$ as the
induction hypothesis.

For the induction step, we have two cases, for
$C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})$ either $C_{1}^{\prime}=\;\downarrow\;$
or $C_{1}^{\prime}\neq\;\downarrow\;$. We will only consider the case
$C_{1}^{\prime}\neq\;\downarrow\;$, since the other is analogous. Then we
have:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket{C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Monotonicity of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
and $\dagger$) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)\mid\xi\right)$ (Definition of wrlp)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)\mid\xi\right)$ (Antitonicity of wrlp
w.r.t. $n$ and monotonicity w.r.t. postexpectation)

For $\dagger$, we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\Big{|}\leavevmode\nobreak\
{C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\
{C_{2}},(s^{\prime},h^{\prime})\Big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}({C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket
C_{1}^{\prime}\rrbracket\left(\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\Big{|}\leavevmode\nobreak\
{C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\
{C_{2}},(s^{\prime},h^{\prime})\Big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}({C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h))\bigg{\\}}$
(Induction hypothesis and monotonicity) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket
C_{1}^{\prime}\rrbracket\left(\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\Big{|}\leavevmode\nobreak\
C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})\Big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C_{1},(s,h))\bigg{\\}}$ (Operational semantics of sequential
composition) $\displaystyle=$ (Definition of step)

Thus, the claim is proven.

######  Lemma E.21.

If $X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C_{1}\rrbracket\left(Y\mid\xi\right)$,
$X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$ and $X\leq\left[{b}\right]\cdot
X_{1}+\left[{\neg b}\right]\cdot X_{2}$ then also $X\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$.

######  Proof E.22.

We prove that for all $n$ we have
$\left[{b}\right]\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+\left[{\neg
b}\right]\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$,
where $\left[{b}\right](s,h)=1$ if $s\in b$ and $\left[{\neg b}\right](s,h)=0$
if $s\not\in b$. Then the inequality holds also for their limits and due to
monotonicity of all operations, we also get the claim.

For the case $n=0$, we have that
$\textsf{{wrlp}}_{0}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)=1\geq\left[{b}\right]\cdot\textsf{{wrlp}}_{0}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+\left[{\neg
b}\right]\cdot\textsf{{wrlp}}_{0}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$, thus the claim holds.

For the case $n+1$, we have two sub-cases. Either $s\in b$ or $s\not\in b$. We
will only prove the first, since the latter is analogous. There we have:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)(s,h)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)$ ($\dagger$, see
below) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket C_{1}\rrbracket\left(Y\mid\xi\right)$ (Statement
17) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket C_{1}\rrbracket\left(Y\mid\xi\right)$
(Monotonicity w.r.t $n$)

For $\dagger$, we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\Big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\},(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\Big{[}1\cdot(\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$
$\displaystyle\leavevmode\nobreak\ \qquad\Big{|}\leavevmode\nobreak\
\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{if-t}]{1}\leavevmode\nobreak\ C_{1},(s,h)\Big{]}$ ($s\in
b$) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$ (Singleton
set)

For $s\not\in b$ we similarly have

$\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)\geq\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\leavevmode\nobreak\ .$

Combining them, we have the claim from above.

######  Lemma E.25.

If $I\leq\left[{b}\right]\cdot X+\left[{\neg b}\right]\cdot Y$ and
$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(I\mid\xi\right)$ then for the loop we have
$I\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$.

######  Proof E.26.

We will now prove by induction on $n$ that if
$I\leq\left[{b}\right]\cdot\textsf{{wrlp}}\llbracket
C\rrbracket\left(I\mid\xi\right)+\left[{\neg b}\right]\cdot Y$ then
$I\leq\textsf{{wrlp}}_{n}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$.
If this holds for all $n$, then also for the limit.

For the base case $n=0$, we have $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mid\xi\right)=1\geq I$.

Now we assume that for some fixed but arbitrary $n$ the claim holds as our
induction hypothesis.

For the induction step, we have two cases. If $s\not\in b$ then:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)(s,h)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi))(s,h)$
($\dagger$, see below) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)(s,h)$
(Statement 17) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ Y(s,h)$
(Definition of wrlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
(\left[{b}\right]\cdot\textsf{{wrlp}}\llbracket
C\rrbracket\left(I\mid\xi\right)+\left[{\neg b}\right]\cdot Y)(s,h)$ (Since
$s\not\in b$) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ I(s,h)$
(Assumption)

For $\dagger$, we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\},(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\left[1\cdot(\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)\mid\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{loop-f}]{1}\leavevmode\nobreak\
\;\downarrow\;,(s,h)\right]$ (Operational semantics of loop and $s\not\in b$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$
(Sum over singleton)

Then for $s\in b$ we have:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)(s,h)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\textsf{{wrlp}}_{n}\llbracket{C}{\,;}\leavevmode\nobreak\
{\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi))(s,h)$
($\dagger\dagger$) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket{C}{\,;}\leavevmode\nobreak\
{\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}}\rrbracket\left(Y\mid\xi\right)(s,h)$
(Statement 17) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\textsf{{wrlp}}_{n}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)\mid\xi\right)(s,h)$
(Lemma E.15) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket C\rrbracket\left(I\mid\xi\right)(s,h)$
(Induction hypothesis and Monotonicity of $\textsf{{wrlp}}_{n}$ w.r.t to
postexpectation) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(I\mid\xi\right)(s,h)$ (Lemma B.13)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
(\left[{b}\right]\cdot\textsf{{wrlp}}\llbracket
C\rrbracket\left(I\mid\xi\right)+\left[{\neg b}\right]\cdot Y)(s,h)$ (Since
$s\in b$) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ I$
(Assumption)

For $\dagger\dagger$ we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\},(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\Big{[}1\cdot(\textsf{{wrlp}}_{n}\llbracket{C}{\,;}\leavevmode\nobreak\
{\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$
$\displaystyle\leavevmode\nobreak\ \qquad\Big{|}\leavevmode\nobreak\
\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{loop-t}]{1}\leavevmode\nobreak\
{C}{\,;}\leavevmode\nobreak\
{\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}},(s,h)\Big{]}$
(Operational semantics of loop and $s\in b$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket{C}{\,;}\leavevmode\nobreak\
{\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$
(Sum over singleton)

Thus, the claim is proven.

######  Lemma E.31.

If $X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C_{1}\rrbracket\left(Y\mid\xi\right)$,
$X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$ and $X\leq e_{p}\cdot
X_{1}+(1-e_{p})\cdot X_{2}$ then $X\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$.

######  Proof E.32.

We prove for all $n$ that

$e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)\leavevmode\nobreak\
.$

If this holds, then the same also holds for their limits and thus by
monotonicity of all operations the claim is proven.

For the case $n=0$ we have
$\textsf{{wrlp}}_{0}\llbracket\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)=1\geq
e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$.

For the case $n+1$ we have

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)$ ($\dagger$, see
below) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}((e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right))\mathbin{{\star}}\xi)$ (Subdist. of
$\mathbin{{\star}}$ with plus and monotonicity of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
(e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right))$ (Statement 17) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\ (e_{p}\cdot\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right))$ (Antitonicity of $\textsf{{wrlp}}_{n}$
w.r.t $n$)

Now for $\dagger$:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\},(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\left[p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[prob]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ (Operational semantics of prob.
choice) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
e_{p}(s)\cdot(\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)+(1-e_{p})(s)\cdot(\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$ (Operational
semantics of prob. choice) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$ (Pointwise
operations)

Thus, the claim is proven.

######  Lemma E.35.

If $X\mathbin{{\star}}\xi\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\left[{\textsf{{{emp}}}}\right]\right)$
then $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$.

######  Proof E.36.

We prove for all $n$ that
$X\leq\textsf{{wrlp}}_{n}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$.

For $n=0$ we have
$\textsf{{wrlp}}_{0}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)=1\geq
X$.

For $n+1>0$ and where $C$ is tame we have

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\right)$ ($\dagger$, see below)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\left[{\textsf{{{emp}}}}\right]\right)$
(Theorem B.23) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\mathbin{{\star}}\xi)$
(Assumption) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\ X$
(Statement 17)

For $\dagger$, we have:

$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\Bigg{(}\lambda(s,h).\leavevmode\nobreak\
\inf\bigg{\\{}\sum\big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\
\qquad\qquad\qquad\qquad\qquad\big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h))\bigg{\\}}\Bigg{)}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\bigg{(}\lambda(s,h).\leavevmode\nobreak\
\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\Big{]}\bigg{)}$
($\text{Act}(\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h))$ is
singleton) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\bigg{(}\lambda(s,h).\leavevmode\nobreak\
\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\Big{]}$
$\displaystyle+\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket\textnormal{{diverge}}\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s,h)\bigg{)}$
$\displaystyle\quad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}\Bigg{)}$ (Splitting reachable programs)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\Bigg{(}\lambda(s,h).\leavevmode\nobreak\
\sum\Big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\qquad\qquad\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\Big{]}$
$\displaystyle+\sum\Big{[}p\cdot(1\mathbin{{\star}}\xi)(s,h)\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}\Bigg{)}$ (Lemma C.25) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\Bigg{(}\lambda(s,h).\leavevmode\nobreak\
\sum\left[p\cdot(Y\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot(1\mathbin{{\star}}\xi)(s,h)\Big{|}\leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)\Big{]}\Bigg{)}$ (Definition of wrlp)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\Bigg{(}\lambda(s,h).\leavevmode\nobreak\
\sum\left[p\cdot(Y\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot(1\mathbin{{\star}}\xi)(s,h)\Big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\Big{]}\Bigg{)}$ (Operational semantics of
atomic regions) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\Bigg{(}\lambda(s,h).\leavevmode\nobreak\
\sum\left[p\cdot(Y\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle+\sum\Big{[}p\cdot(1)(s,h)\Big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\Big{]}\Bigg{)}$ (Since there exists
$h_{\xi}$ with $\xi(s,h_{\xi})=1$ and $h=h_{\xi}\mathbin{{\star}}h^{\prime}$
for some $h^{\prime}$ due to
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\right)$ (Definition of wlp)

The difficulty of this proof would have been far greater, if we had allowed
non-tame programs in atomic regions. Since we block when encountering non-tame
programs, we have
$\textsf{{wrlp}}_{n+1}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)=\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$.

Thus, the claim is proven.

######  Lemma E.40.

If $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\mathbin{{\star}}\pi\right)$ then
$X\mathbin{{\star}}\xi\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$.

######  Proof E.41.

To prove this, we first prove by induction on $n$ that for all programs $C$ we
have the inequality $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mid\pi\mathbin{{\star}}\xi\right)\mathbin{{\star}}\xi\leq\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$.

For the induction base $n=0$, the claim holds trivially as
$\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)=1$.

We now assume that the claim holds for some arbitrary but fixed $n$ as our
induction hypothesis.

For the induction step, we have two cases. If $C=\;\downarrow\;$ then we have
that the equality
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)=Y\mathbin{{\star}}\xi=\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y\mid\pi\mathbin{{\star}}\xi\right)\mathbin{{\star}}\xi$
holds. Thus, we assume that $C\neq\;\downarrow\;$. There we prove now

$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\left(\pi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\left(\xi\mathbin{{\star}}\pi\right)\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Statement 23) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\left(\xi\mathbin{{\star}}\pi\right)\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Induction Hypothesis) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mid\xi\mathbin{{\star}}\pi\right)$ (Definition of wrlp)

and we have

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mid\pi\mathbin{{\star}}\xi\right)\leq\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$ iff
$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mid\pi\mathbin{{\star}}\xi\right)\mathbin{{\star}}\xi\leq\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$

by adjointness (cf. Statement 15).

Lastly we now have:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\lim_{n\rightarrow\infty}\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\pi\right)$ (Definition of wrlp)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\lim_{n\rightarrow\infty}\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y\mid\pi\mathbin{{\star}}\xi\right)\mathbin{{\star}}\xi$ (See
above) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\pi\mathbin{{\star}}\xi\right)\mathbin{{\star}}\xi$
(Definition of wrlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
X\mathbin{{\star}}\xi$ (Assumption)

Thus, the claim is proven.

######  Lemma E.45.

If $X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C_{1}\rrbracket\left(Y_{1}\mid\xi\right)$,
$X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)$ and
$\text{Write}(C_{i})\cap\text{Vars}\,(C_{3-i},Y_{3-i},\xi)=\emptyset$ then
$X_{1}\mathbin{{\star}}X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket(\left.C_{1}\;\middle\|\;C_{2}\right.)\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)$.

######  Proof E.46.

We instead prove that we have

$\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket(\left.C_{1}\;\middle\|\;C_{2}\right.)\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)$

by induction on $n$. If this holds for all $n$, the same holds for the limit,
which yields the claim.

For the induction base $n=0$, we have

$\textsf{{wrlp}}_{0}\llbracket(\left.C_{1}\;\middle\|\;C_{2}\right.)\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)=1=\textsf{{wrlp}}_{0}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{0}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)\leavevmode\nobreak\ .$

We assume that the claim holds for some arbitrary but fixed $n$ as our
induction hypothesis.

For the induction step, we have four cases. If $C_{1}=C_{2}=\;\downarrow\;$ we
have:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket(\left.\;\downarrow\;\;\middle\|\;\;\downarrow\;\right.)\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\left(Y_{1}\mathbin{{\star}}Y_{2}\mathbin{{\star}}\xi\right)$
(Monotonicity of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
and $\dagger$, see below) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\ Y_{1}\mathbin{{\star}}Y_{2}$ (Statement 17)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{2}\mid\xi\right)$
(Definition of wrlp)

For $\dagger$, we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})\mid(\left.\;\downarrow\;\;\middle\|\;\;\downarrow\;\right.),(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}((\left.\;\downarrow\;\;\middle\|\;\;\downarrow\;\right.),(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sum\left[\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)\mathbin{{\star}}\xi)(s,h)\mid(\left.\;\downarrow\;\;\middle\|\;\;\downarrow\;\right.),(s,h)\leavevmode\nobreak\
\xrightarrow[\text{conc-end}]{1}\leavevmode\nobreak\
\;\downarrow\;,(s,h)\right]$ (Operational semantics of concurrency)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)\mathbin{{\star}}\xi)(s,h)$
(Sum of singleton) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
(Y_{1}\mathbin{{\star}}Y_{2}\mathbin{{\star}}\xi)(s,h)$ (Definition of wrlp)

For the case $C_{1}\neq\;\downarrow\;$ and $C_{2}\neq\;\downarrow\;$ we have:

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket(\left.C_{1}\;\middle\|\;C_{2}\right.)\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\min\bigg{\\{}$
($\dagger\dagger$, see below) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\min\bigg{\\{}$
(Induction Hypothesis and
$\text{Vars}\,(C_{i}^{\prime})\subseteq\text{Vars}\,(C_{i})$)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\min\bigg{\\{}$
(Theorem C.81 and $\text{Vars}\,(\textsf{{wrlp}}_{n}\llbracket
C_{i}\rrbracket\left(Y_{i}\mid\xi\right))\subseteq\text{Vars}\,(C_{i},Y_{i},\xi)$
by Lemma C.12) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\bigg{\\{}\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle\leavevmode\nobreak\
\quad\qquad\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
is distributiv with min) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\min\bigg{\\{}\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)\mathbin{{\star}}\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right),$ $\displaystyle\leavevmode\nobreak\
\quad\qquad\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)\mathbin{{\star}}\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\bigg{\\}}$ (Statement 24)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\bigg{\\{}\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right),$ $\displaystyle\leavevmode\nobreak\
\quad\qquad\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\bigg{\\}}$ (Definition of wrlp)
$\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\min\bigg{\\{}\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right),$ $\displaystyle\leavevmode\nobreak\
\quad\qquad\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\bigg{\\}}$ ($\textsf{{wrlp}}_{n}$ is
antitone w.r.t. $n$) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\textsf{{wrlp}}_{n+1}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)$ (Set is a singleton)

For $\dagger\dagger$ we prove:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\big{|}\leavevmode\nobreak\
(\left.C_{1}\;\middle\|\;C_{2}\right.),(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}((\left.C_{1}\;\middle\|\;C_{2}\right.),(s,h\mathbin{{\star}}h_{\xi}))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\bigg{\\{}\inf\Big{\\{}\sum\big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket\left.C_{1}^{\prime}\;\middle\|\;C_{2}\right.\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\
\quad\qquad\qquad\big{|}\leavevmode\nobreak\
C_{1},(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})\big{]}\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C_{1},(s,h\mathbin{{\star}}h_{\xi}))\Big{\\}},$
$\displaystyle\leavevmode\nobreak\
\quad\qquad\inf\Big{\\{}\sum\big{[}p\cdot(\textsf{{wrlp}}_{n}\llbracket\left.C_{1}\;\middle\|\;C_{2}^{\prime}\right.\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)\mathbin{{\star}}\xi)(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\
\quad\qquad\qquad\big{|}\leavevmode\nobreak\
C_{2},(s,h\mathbin{{\star}}h_{\xi})\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C_{2}^{\prime},(s^{\prime},h^{\prime})\big{]}\Big{|}\leavevmode\nobreak\
a\in\text{Act}(C_{2},(s,h\mathbin{{\star}}h_{\xi}))\Big{\\}}\bigg{\\}}$
(Operational Semantics of concurrency) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \min\bigg{\\{}$ (Definition of step)

The cases $C_{1}\neq\;\downarrow\;$, $C_{2}=\;\downarrow\;$ and
$C_{1}=\;\downarrow\;$, $C_{2}\neq\;\downarrow\;$ are analogous to the
previous case. We just drop the minimum, since only one thread can be
executed.

Thus, the claim is proven.

######  Definition E.63.

A program $C$ is almost surely terminating w.r.t. $S$ iff for all schedulers
$\mathfrak{s}\in S$ and all program states $(s,h)$ we have
$C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{0}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\leavevmode\nobreak\ .$

######  Lemma E.64.

If $X_{1}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y_{1}\right)$,
$X_{2}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y_{2}\right)$ and $C$
ist almost surely terminating w.r.t. $S$ then $a\cdot
X_{1}+X_{2}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(a\cdot
Y_{1}+Y_{2}\right)$.

######  Proof E.65.

We have:

$\displaystyle\leavevmode\nobreak\ \textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(a\cdot Y_{1}+Y_{2}\right)(s,h)$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\left[p\cdot(a\cdot
Y_{1}+Y_{2})(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]+p_{div}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{p_{div}}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\bigg{\\}}$ (Definition of wlp)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(a\cdot Y_{1}+Y_{2})(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ ($C$ is almost surely terminating w.r.t. $S$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(a\cdot
Y_{1}(s^{\prime},h^{\prime}))+Y_{2}(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ (Pointwise application) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\left[p\cdot a\cdot
Y_{1}(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\leavevmode\nobreak\ \quad\leavevmode\nobreak\ +\sum\left[p\cdot
Y_{2}(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ (Linearity of sum) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\ \quad\inf\bigg{\\{}\sum\left[p\cdot a\cdot
Y_{1}(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ $\displaystyle+\inf\bigg{\\{}\sum\left[p\cdot
Y_{2}(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ (Statement 7) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\ a\cdot\inf\bigg{\\{}\sum\left[p\cdot
Y_{1}(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ $\displaystyle\leavevmode\nobreak\
+\inf\bigg{\\{}\sum\left[p\cdot Y_{2}(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in S\bigg{\\}}$ (Factorisation with constant) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ a\cdot\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(Y_{1}\right)+\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(Y_{2}\right)$

######  Lemma E.66.

If $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)$ then
$X\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y\right)$.

######  Proof E.67.

Since $S\subseteq\mathbb{S}$ we have $\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)\leq\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(Y\right)$. Furthermore, by Theorem B.23 we have
$\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)=\textsf{{wlp}}\llbracket
C\rrbracket\left(Y\right)$. Thus, we also have
$X\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y\right)$.

######  Lemma E.68.

If $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ and
$\text{Write}(C)\cap\text{Vars}\,(Z)=\emptyset$ then we also have
$X\mathbin{{\star}}Z\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y\mathbin{{\star}}Z\mid\xi\right)$.

######  Proof E.69.

First, it is easy to prove that $\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}Z\mid\xi\right)=\textsf{{wrlp}}\llbracket(\left.C\;\middle\|\;\;\downarrow\;\right.)\rrbracket\left(Y\mathbin{{\star}}Z\mid\xi\right)$.
From this, we directly have the conclusion by Lemma E.45.

######  Lemma E.70.

If $C$ is a terminating atom and $X\mathbin{{\star}}\xi\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\left[{\textsf{{{emp}}}}\right]\right)$
then $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$.

######  Proof E.71.

Since $C$ is a terminating atom, we have $\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)=\textsf{{wrlp}}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$
and by Lemma E.35 together with the assumption we have
$\textsf{{wrlp}}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)\geq
X$, which proves the claim.

######  Lemma E.72.

If $X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y_{1}\mid\xi\right)$ and
$X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)$ then we have for the maximum
$\max\left\\{\,{X_{1}},\>{X_{2}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\max\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$.

######  Proof E.73.

By monotonicity (Lemma E.1) we have for both $i\in\\{1,2\\}$ that the
inequality $\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y_{i}\mid\xi\right)\leq\textsf{{wrlp}}\llbracket
C\rrbracket\left(\max\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$
holds, thus for both $i\in\\{1,2\\}$ the inequality
$X_{i}\leq\textsf{{wrlp}}\llbracket
C\rrbracket\left(\max\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$
also holds. Then we also have that the inequality
$\max\left\\{\,{X_{1}},\>{X_{2}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\max\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$
holds.

######  Lemma E.74.

If $X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y_{1}\mid\xi\right)$,
$X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)$ and $\xi$ is precise then
$\min\left\\{\,{X_{1}},\>{X_{2}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\min\left\\{\,{X_{2}},\>{Y_{2}}\,\right\\}\mid\xi\right)$.

######  Proof E.75.

We prove instead by induction on $n$ that the equality

$\min\left\\{\,{\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y_{1}\mid\xi\right)},\>{\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)}\,\right\\}=\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(\min\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$

holds. If this holds, the claim also holds.

For the induction base $n=0$, we have that $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(\min\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)=1$,
which is always equal to $\min\left\\{\,{\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y_{1}\mid\xi\right)},\>{\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)}\,\right\\}$.

Thus, we assume for some arbitrary but fixed $n$ the claim holds as our
induction hypothesis.

For the induction step, we have two cases. For $C=\;\downarrow\;$ we have

$\displaystyle\leavevmode\nobreak\
\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(\min\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\min\left\\{\,{\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{1}\mid\xi\right)},\>{\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{2}\mid\xi\right)}\,\right\\}\leavevmode\nobreak\
.$

For $C\neq\;\downarrow\;$ we have

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(\min\left\\{\,{Y_{1}},\>{Y_{2}}\,\right\\}\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Induction Hypothesis) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($\xi$ precise and Statement 25) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\min\\{$
($\dagger$, see below) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\Big{\\{}\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle\leavevmode\nobreak\ \qquad\leavevmode\nobreak\
\;\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Statement 20) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\left\\{\,{\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y_{1}\mid\xi\right)},\>{\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)}\,\right\\}$ (Definition of wrlp)

For $\dagger$ we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot\min\left\\{\,{t(C^{\prime})},\>{t^{\prime}(C^{\prime})}\,\right\\}(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Definition of step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\min\Big{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right],$ $\displaystyle\leavevmode\nobreak\
\qquad\qquad\quad\sum\left[p\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]\Big{\\}}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Distributivity with min of addition and
positive multiplication) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\min\bigg{\\{}\inf\Big{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\Big{\\}},$ $\displaystyle\leavevmode\nobreak\
\qquad\quad\inf\Big{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\Big{\\}}\bigg{\\}}$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \min\left\\{\,{\step{C}{\lambda
C^{\prime}.\leavevmode\nobreak\ \textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y_{1}\mid\xi\right)\mathbin{{\star}}\xi}},\>{\step{C}{\lambda
C^{\prime}.\leavevmode\nobreak\ \textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(Y_{2}\mid\xi\right)\mathbin{{\star}}\xi}}\,\right\\}$
(Definition of step)

######  Lemma E.86.

If $X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y_{1}\mid\xi\right)$,
$X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)$, $\xi$ is precise and
$\text{Write}(C)\cap\text{Vars}\,(e)=\emptyset$ then $e_{p}\cdot
X_{1}+(1-e_{p})\cdot X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(e_{p}\cdot Y_{1}+(1-e_{p})\cdot
Y_{2}\mid\xi\right)$.

######  Proof E.87.

We prove by induction on $n$ that $e_{p}\cdot\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y_{1}\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)\leq\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(e_{p}\cdot Y_{1}+(1-e_{p})\cdot Y_{2}\mid\xi\right)$. If this
holds, the claim also holds.

For the induction base $n=0$, we have $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(e_{p}\cdot Y_{1}+(1-e_{p})\cdot
Y_{2}\mid\xi\right)=1=e_{p}+(1-e_{p})=e_{p}\cdot\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y_{1}\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)$.

We now assume that the claim holds for some arbitrary but fixed $n$ as our
induction hypothesis.

For the induction step, we have three cases. For the case $C=\;\downarrow\;$
we have the equality
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(e_{p}\cdot
Y_{1}+(1-e_{p})\cdot Y_{2}\mid\xi\right)=e_{p}\cdot Y_{1}+(1-e_{p})\cdot
Y_{2}=e_{p}\cdot\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{1}\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{2}\mid\xi\right)$.
For the case $C\neq\;\downarrow\;$, $\text{Act}(C,(s,h))=\emptyset$ we have:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(e_{p}\cdot Y_{1}+(1-e_{p})\cdot Y_{2}\mid\xi\right)(s,h)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)(s,h)$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}1)(s,h)$
($\text{Act}(C,(s,h))=\emptyset$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ 1(s,h)$ (Definition of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\left(e_{p}+(1-e_{p})\right)(s,h)$ (Algebra) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
e_{p}\cdot\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{1}\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(Y_{2}\mid\xi\right)$
(Similar to above)

And lastly we have the case that $C\neq\;\downarrow\;$,
$\text{Act}(C,(s,h))\neq\emptyset$:

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(e_{p}\cdot Y_{1}+(1-e_{p})\cdot Y_{2}\mid\xi\right)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Definition of wrlp) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Induction Hypothesis) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($\xi$ is precise and Statements 26 and 27) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\big{(}e_{p}\cdot$
$\displaystyle\leavevmode\nobreak\ \quad\leavevmode\nobreak\ +(1-e_{p})\cdot$
(Monotoncitiy of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
and $\dagger$, see below) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
e_{p}\cdot\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)$
$\displaystyle+(1-e_{p})\cdot\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)$
(Statements 21 and 22) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
e_{p}\cdot\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y_{1}\mid\xi\right)+(1-e_{p})\cdot\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(Y_{2}\mid\xi\right)$ (Definition of wrlp)

Lastly for $\dagger$ we have:

$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot(e_{p}\cdot t(C^{\prime})+(1-e_{p})\cdot
t^{\prime}(C^{\prime}))(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right\\}$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Definition of step) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\big{[}p\cdot(e_{p}(s^{\prime})\cdot
t(C^{\prime})(s^{\prime},h^{\prime})+(1-e_{p}(s^{\prime}))\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime}))$
$\displaystyle\leavevmode\nobreak\ \qquad\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Pointwise application) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\big{[}p\cdot(e_{p}(s)\cdot
t(C^{\prime})(s^{\prime},h^{\prime})+(1-e_{p}(s))\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime}))$
$\displaystyle\leavevmode\nobreak\ \qquad\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Lemmas C.10 and C.7 and
$\text{Write}(C)\cap\text{Vars}\,(e_{p})=\emptyset$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\big{[}p\cdot
e_{p}(s)\cdot t(C^{\prime})(s^{\prime},h^{\prime})+p\cdot(1-e_{p}(s))\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime})$
$\displaystyle\leavevmode\nobreak\ \qquad\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Distributivity) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\big{[}p\cdot
e_{p}(s)\cdot t(C^{\prime})(s^{\prime},h^{\prime})\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad+\sum\big{[}p\cdot(1-e_{p}(s))\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime})\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Commutativitiy) $\displaystyle\geq$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\big{[}p\cdot e_{p}(s)\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
$\displaystyle\leavevmode\nobreak\
+\inf\bigg{\\{}\sum\big{[}p\cdot(1-e_{p}(s))\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime})\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Statement 7 and $\text{Act}(C,(s,h))\neq\emptyset$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
e_{p}(s)\cdot\inf\bigg{\\{}\sum\big{[}p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
$\displaystyle\leavevmode\nobreak\
+(1-e_{p}(s))\cdot\inf\bigg{\\{}\sum\big{[}p\cdot
t^{\prime}(C^{\prime})(s^{\prime},h^{\prime})\big{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\big{]}$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Constant factors can be shifted outside) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ e_{p}(s)\cdot$ (Definition of step)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\left(e_{p}\cdot\right)(s,h)$ (Pointwise application)

Thus, the claim is proven.

See 7

######  Proof E.101.

We prove the soundness of all inference rules.

term $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\;\downarrow\;\rrbracket\left(X\mid\xi\right)$

$Y\leq\sup_{v\in\mathbb{Z}}\left[{e\mapsto
v}\right]\mathbin{{\star}}(\left[{e\mapsto
v}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\left[{x}\coloneqq{v}\right])$
look $Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
x\mathrel{\textnormal{{:=}}}\texttt{<}\,e\,\texttt{>}\rrbracket\left(X\mid\xi\right)$

$Y\leq\inf_{v\in\mathbb{Z}}\left[{v\mapsto
e_{1},\dots,e_{n}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\left[{x}\coloneqq{v}\right]$
alloc $Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket{x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{1},\dots,e_{n}\right)\rrbracket\left(X\mid\xi\right)$

$Y\leq X\left[{x}\coloneqq{e}\right]$ assign $Y\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
x\mathrel{\textnormal{{:=}}}e\rrbracket\left(X\mid\xi\right)$

$Y\leq\left[{e\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{e\mapsto
e^{\prime}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)$
mut $Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\texttt{<}\,e\,\texttt{>}\mathrel{\textnormal{{:=}}}e^{\prime}\rrbracket\left(X\mid\xi\right)$

$Y\leq X\mathbin{{\star}}\left[{x\mapsto\,{-}\,}\right]$ disp
$Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\mathtt{free}(x)\rrbracket\left(X\mid\xi\right)$

The proof rules term, look, alloc, assign, mut and disp are sound by Lemma E.8
and the proof rules for wlp from [5].

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)$ $Y\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)$ seq $X\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket{C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)$

The proof rule seq is sound by Lemma E.15.

$X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)$ $X_{2}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$ if $\left[{b}\right]\cdot
X_{1}+\left[{\neg b}\right]\cdot X_{2}\leavevmode\nobreak\
\leq\leavevmode\nobreak\