Proof Sketch. The main ingredient of the proof is the following theorem ([28] and [30]): "For every positive self-adjoint operator \(A\), there is a corresponding densely defined, closed, symmetric, positive form \(a: \mathfrak{D}(a) \times \mathfrak{D}(a) \to \mathbb{C}\) with \(a[x,y] = \langle A^{\frac{1}{2}}x, A^{\frac{1}{2}}y\rangle\) for all \(x,y \in \mathfrak{D}(a) = \mathfrak{D}(A^{\frac{1}{2}})\) and the other way round". ◻

Proof. Follows immediately from the definitions: \[\begin{align} a \leq b \Leftrightarrow & \text{ }\forall x \in \mathfrak{D}(b): a[x] \leq b[x] \land \mathfrak{D}(b) \subseteq \mathfrak{D}(a) \\ \Leftrightarrow & \text{ }\forall \psi \in \mathfrak{D}(B_\infty^{\frac{1}{2}}): \norm{A_\infty^{\frac{1}{2}}\ket{\psi}}^2 \leq \norm{B_\infty^{\frac{1}{2}}\ket{\psi}}^2 \land \mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}}) \Leftrightarrow A \sqsubseteq B \qedhere \end{align}\] ◻

Proof Sketch. The increasing sequence of expectations \(\{A_n\}_n\) corresponds to an increasing sequence of form-expectations \(\{a_n\}_n\) by Propositions [prop:OpstoForms] and [prop:orderEquivalence]. By Kato’s theorem, the limit form \(a\) of the sequence \(\{a_n\}_n\) exists and is a form-expectation. Then we can construct the corresponding expectation \(A\) from the limit form \(a\) by Proposition [prop:OpstoForms]. Finally, we show that \(A\) is indeed the least upper bound of the sequence \(\{A_n\}_n\). ◻

Proof Sketch. For each operation, we show that the resulting form is closed, symmetric and positive, thus a form-expectation. ◻

Proof. Follows immediately from Propositions [prop:rewardFreeOriginalSem] and [prop:semanticsProperties]. ◻

Proof. \(\mathbb{E}_{C}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho)\) implies that \(C\) is a pre-expectation of \(B\) and if there was another pre-expectation \(A\) with \(C \sqsubseteq A\), it would hold that \(\mathbb{E}_{A}\left(\rho\right) > \mathbb{E}_{C}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho)\) for some \(\rho\) which contradicts that \(A\) is a pre-expectation. ◻

Proof. Follows from Theorem 3 and Lemma 6. ◻

Proof Sketch. We show by simultaneous induction on the structure of \(S\):

1. \(wp\llbracket S \rrbracket (B)\) is an expectation, and

2. \(\mathbb{E}_{wp\llbracket S \rrbracket (B)}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho)\) for all \(\rho \in \mathcal{D}(\mathcal{H})\).

 ◻

Proof. Follows immediately from the definition of \(\llbracket \boldsymbol{reward} (r) \rrbracket_D\) and we only add finite many reward statements to each statement of \(S\), i.e., we do not create non-termination by adding those reward statements. ◻

Proof. It is \(\mathbb{E}_{\boldsymbol{0}}\left(\llbracket T({S}) \rrbracket_D(\rho)\right) = 0\), thus \[\mathbb{E}_{wp\llbracket T({S}) \rrbracket (\boldsymbol{0})}\left(\rho\right) = \mathbb{E}_{\boldsymbol{0}}\left(\llbracket T({S}) \rrbracket_D(\rho)\right) + \llbracket T({S}) \rrbracket_{R}(\rho) = \llbracket T({S}) \rrbracket_{R}(\rho). \qedhere\] ◻

Proof. We use the following theorem ([28] and [30]): "For every positive self-adjoint operator \(A\), there is a corresponding densely defined, closed, symmetric, positive form \(a: \mathfrak{D}(a) \times \mathfrak{D}(a) \to \mathbb{C}\) with \(a[x,y] = \langle A^{\frac{1}{2}}x, A^{\frac{1}{2}}y\rangle\) for all \(x,y \in \mathfrak{D}(a) = \mathfrak{D}(A^{\frac{1}{2}})\) and the other way round."

We show that this theorem implies the proposition:

• \(\Rightarrow\): For every expectation \(A\) there is the positive, self-adjoint \(\infty\)-restriction \(A_\infty\). By the above theorem, there is a corresponding densely defined, closed, symmetric, positive form \(a\), thus also a form-expectation.

• \(\Leftarrow\): For every form-expectation \(a\), we can construct a densely defined form by extending \(a\) to the closure of its domain (that means \(\mathfrak{D}(a)\) is dense in \(\overline{\mathfrak{D}(a)}\)). By the above theorem, there is a corresponding positive self-adjoint operator \(A_\infty\). We obtain \(A \in \mathcal{E}(\mathcal{H})\) by extending the \(\infty\)-restriction \(A_\infty\) to \(\mathcal{H}\).

 ◻

Proof. Let \(\{A_n\}_n\) be an increasing sequence of expectations over \(\mathcal{H}\). That means every \(A_n\) is positive and \(\infty\)-self-adjoint and \(A_n \sqsubseteq A_{n+1}\) holds for all \(n\).

1. For each \(A_n\), there is the corresponding form-expectation \(a_n\) by Proposition [prop:OpstoForms].

2. \(a_n \leq a_{n+1}\) holds exactly if \(A_n \sqsubseteq A_{n+1}\) by Proposition [prop:orderEquivalence]. Thus \(\{a_n\}_n\) is a monotone non-decreasing sequence of closed, symmetric forms bounded from below.

3. We use Kato’s theorem [28]: "Let \(a_1 \leq a_2 \leq ...\) be a monotone non-decreasing sequence of closed symmetric forms bounded from below. Set \(a[x] = \lim a_n[x]\) whenever the finite limit exists. \(a\) is a closed symmetric form bounded from below." As each \(a_n\) is positive, \(a\) is positive as well. Thus \(a \in \mathcal{F}(\mathcal{H})\). Note that \(\mathfrak{D}(a)\) might not be dense in \(\mathcal{H}\), but it is dense in \(\overline{\mathfrak{D}(a)}\).

4. We use this limit form and define the corresponding expectation \(A\) according to Proposition [prop:OpstoForms].

   Then \(A_\infty\) is the self-adjoint operator that corresponds to the limit form [28] and as each \(A_n\) is positive, it is also positive.

   Then \(A\) is an expectation with \(A x = A_\infty x\) for all \(x \in \mathfrak{D}(A) = \mathfrak{D}(A_\infty)\).

Now we show that \(A\) is indeed the least upper bound of the sequence \(A_n\):

By [enum46order], we have \(A_n \sqsubseteq A\) for all \(n\) because \(a_n \leq a\) for all \(n\). That means \(A\) is an upper bound of the sequence \(A_n\).

Now it remains to show that it is the least upper bound. Let \(B: \mathfrak{D}(B) \to \mathcal{H}\) be another expectation with \(A_n \sqsubseteq B\) for all \(n\) (a possible other smaller upper bound). Then by [enum46order], it is \(a_n \leq b\) for all \(n\) where \(b\) is the form-expectation that corresponds to \(B\). Thus, by the definition of the limit form, it is \(a \leq b\). Again by [enum46order], this implies \(A \sqsubseteq B\).

Convergence on the form-level is pointwise convergence, i.e., \(a[x] = \lim_n a_n[x]\) for all \(x \in \mathfrak{D}(a)\). For the corresponding expectations, this implies convergence in WOT: \[\begin{align} &\text{ }\forall x \in \mathfrak{D}(A): a_n[x] \to a[x] \\ \Rightarrow & \text{ }\forall x,y \in \mathfrak{D}(A): a_n[x,y] \to a[x,y] \\ \Rightarrow &\text{ }\forall x,y \in \mathfrak{D}(A): \langle x, A_n y\rangle \to \langle x, A y\rangle \\ \Rightarrow &\text{ }A_n \to A \text{ in WOT} \end{align}\]

Overall, the proof steps are visualized in the diagram in Figure 2.

 ◻

Proof.

• To show: \(a+b\) is a form-expectation. Recall, \(a+b\) is defined as the form \(c: \mathfrak{D}(c) \times \mathfrak{D}(c) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(c) = \mathfrak{D}(a) \cap \mathfrak{D}(b), c[x,y] = a[x,y] + b[x,y] \end{align}\] The definition of the sum is the same as in [28] (called ‘generalized sum’). By [28] is \(c\) closed. Symmetry follows from the symmetry of \(a\) and \(b\) and positivity from the positivity of \(a\) and \(b\).

• To show: \(\alpha \cdot a\) is a form-expectation. Recall, \(\alpha \cdot a\) is defined as the form \(\alpha \cdot a: \mathfrak{D}(\alpha \cdot a) \times \mathfrak{D}(\alpha \cdot a) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(\alpha \cdot a) = \mathfrak{D}(a),(\alpha \cdot a)[x,y] = \alpha \cdot a[x,y] \end{align}\]

  • Symmetry follows from the symmetry of \(a\), as \((\alpha \cdot a)[x,y] = \alpha \cdot a[x,y] = \alpha \cdot \overline{a[y,x]} = \overline{(\alpha \cdot a)[y,x]}\) and \(\alpha\) is real.

  • Positivity follows from the positivity of \(a\), as \((\alpha \cdot a)[x] = \alpha \cdot a[x] \geq 0\) for all \(x \in \mathfrak{D}(\alpha \cdot a)\) and \(\alpha \geq 0\).

  • Closeness follows from the closeness of \(a\) as every sequence \(\{x_n\}_n\) in \(\mathfrak{D}(\alpha \cdot a)\) with \(x_n \underset{t}{\to} x\) also is a sequence in \(\mathfrak{D}(a)\) with \(x_n \underset{t}{\to} x\). Thus we have \(x\in \mathfrak{D}(\alpha \cdot a) = \mathfrak{D}(a)\) and \((\alpha \cdot a)[x_n - x_m] = \alpha \cdot a[x_n - x_m]\to 0\) for \(n,m \to \infty, \alpha\geq 0\). Thus \(\alpha \cdot a\) is closed.

• To show: \(a_M\) is a form-expectation. Recall, \(a_M\) is defined as the form \(a_M: \mathfrak{D}(a_M) \times \mathfrak{D}(a_M) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(a_M) = \{ \psi \in \mathcal{H}\mid M\psi \in \mathfrak{D}(a)\}, a_M[x,y] = a[Mx, My] \end{align}\] Note that \(\bra{\psi} M^\dagger \odot A \odot M \ket{\psi} = \bra{M\psi} A \ket{M\psi}\).

  • Symmetry follows from the symmetry of \(a\), as \(a_M[x,y] = a[Mx, My] = \overline{a[My, Mx]} = \overline{a_M[y,x]}\).

  • Positivity follows from the positivity of \(a\), as \(a_M[x] = a[Mx] \geq 0\) for all \(x \in \mathfrak{D}(a_M)\).

  • Closeness follows from the closeness of \(a\): Let \(\{x_n\}_n\) be a sequence in \(\mathfrak{D}(a_M)\) with \(x_n \underset{t}{\to} x\). That means \(x_n \in \mathfrak{D}(a_M)\), \(x_n \to x\) and \(a_M[x_n - x_m] \to 0\) for \(n,m \to \infty\). We need to show that \(x \in \mathfrak{D}(a_M)\) and \(a_M[x_n - x] \to 0\) for \(n \to \infty\). It is \(a_M[x_n - x_m]=a[M(x_n-x_m)]\), so \(a[x_n-M x_m] \to 0\) and \(Mx_n \in \mathfrak{D}(a)\) for all \(n\). As \(M\) is bounded (thus continuous), \(Mx_n \to Mx\). By the closeness of \(a\), it is \(Mx \in \mathfrak{D}(a)\) and \(a[Mx_n - Mx] \to 0\) for \(n \to \infty\). Thus \(x \in \mathfrak{D}(a_M), Mx_n \to Mx\) and \(a_M[x_n - x] \to 0\) for \(n \to \infty\). By the closeness of \(a\), we get \(Mx \in \mathfrak{D}(a)\) and thus \(x \in \mathfrak{D}(a_M)\). Thus \(a_M\) is closed.

 ◻

Proof. As \(A_n \in \mathcal{E}(\mathcal{H})\), each \(A_n\) is positive. Thus \(\{\sum_{n=0}^N A_n \}_N\) with \(\sum_{n=0}^N A_n = A_0 \oplus A_1 \oplus... \oplus A_N\) is an increasing sequence. All sums are finite and thus in \(\mathcal{E}(\mathcal{H})\) by Definition 5. By Theorem 1, this sequence has a least upper bound/limit \(\lim_{N \to \infty} \sum_{n=0}^N A_n \in \mathcal{E}(\mathcal{H})\). As convergence in WOT considers sequences of (extended) reals, this limit coincides with \(\sum_{n=0}^\infty A_n\) and as the limit is an expectation, \(\sum_{n=0}^\infty A_n \in \mathcal{E}(\mathcal{H})\). ◻

Proof. Let \(a, a_n, b, b_n\) be the corresponding form-expectations of \(A, A_n, B, B_n\).

1. \(\left(\bigvee A_n \right)\oplus B = \bigvee \left(A_n \oplus B\right)\):

   Let \(\bigvee A_n = A\). By Proposition [prop:orderEquivalence], \(a_n \leq a_{n+1}\) for all \(n\) and \(\bigvee a_n = a\) by the definition of the limit form. It is \(\mathfrak{D}(a) = \{x \in \bigcap_n \mathfrak{D}(a_n) \mid \bigvee a_n[x] < \infty\}\) and \(a[x,y] = \bigvee a_n[x,y]\). We show that both sides correspond to the same form and thus to the same operator by Proposition [prop:OpstoForms]:

   The form that corresponds to \(\left(\bigvee A_n \right)\oplus B = A \oplus B\) is \(c: \mathfrak{D}(c) \times \mathfrak{D}(c) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(c) &= \mathfrak{D}(a) \cap \mathfrak{D}(b)\\ c[x,y] &= a[x,y] + b[x,y] \end{align}\]for all \(x,y \in \mathfrak{D}(c)\).

   The form that corresponds to \(\bigvee \left(A_n \oplus B\right)\) is \(d: \mathfrak{D}(d) \times \mathfrak{D}(d) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(d) &= \{x \in \bigcap_n \mathfrak{D}(a_n) \cap \mathfrak{D}(b) \mid \bigvee a_n[x] < \infty\}\\ d[x,y] &= \bigvee a_n[x,y] + b[x,y] \end{align}\] for all \(x,y \in \mathfrak{D}(d)\). Then \[\begin{align} \mathfrak{D}(c) &= \mathfrak{D}(a) \cap \mathfrak{D}(b) = \{x \in \bigcap_n \mathfrak{D}(a_n) \cap \mathfrak{D}(b) \mid \bigvee a_n[x] < \infty\} = \mathfrak{D}(d),\\ c[x,y] &= a[x,y] + b[x,y] = \bigvee a_n[x,y] + b[x,y] = d[x,y] \end{align}\] for all \(x,y \in \mathfrak{D}(c) = \mathfrak{D}(d)\), so both sides correspond to the same form and thus to the same operator.

2. \(B \oplus\left(\bigvee A_n \right) = \bigvee \left(B \oplus A_n \right)\): Analogous to the previous case.

3. \(\left(\bigvee A_n \right)\oplus\left( \bigvee B_n \right) = \bigvee \left(A_n \oplus B_n \right)\):

   Let \(\bigvee A_n = A\) and \(\bigvee B_n = B\). It is \(\mathfrak{D}(a) = \{x \in \bigcap_n \mathfrak{D}(a_n) \mid \bigvee a_n[x] < \infty\}\), \(\mathfrak{D}(b) = \{x \in \bigcap_n \mathfrak{D}(b_n) \mid \bigvee b_n[x] < \infty\}\) and \(a[x,y] = \bigvee a_n[x,y], b[x,y] = \bigvee b_n[x,y]\). We show that both sides correspond to the same form and thus to the same operator by Proposition [prop:OpstoForms]:

   The form that corresponds to \(\left(\bigvee A_n \right)\oplus\left( \bigvee B_n \right) = A \oplus B\) is \(c: \mathfrak{D}(c) \times \mathfrak{D}(c) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(c) &= \mathfrak{D}(a) \cap \mathfrak{D}(b)\\ c[x,y] &= a[x,y] + b[x,y] \end{align}\]for all \(x,y \in \mathfrak{D}(c)\).

   The form that corresponds to \(\bigvee \left(A_n \oplus B_n \right)\) is \(d: \mathfrak{D}(d) \times \mathfrak{D}(d) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(d) &= \{x \in \bigcap_n \mathfrak{D}(a_n)\cap \mathfrak{D}(b_n) \mid \bigvee a_n[x]+ b_n[x] < \infty\} \\ d[x,y] &= \bigvee a_n[x,y] + b_n[x,y] \end{align}\] for all \(x,y \in \mathfrak{D}(d)\).

   As \(a_n\) and \(b_n\) are monotone non-decreasing sequences of forms, it is \(\bigvee a_n[x] + b_n[x] = \bigvee a_n[x] + \bigvee b_n[x]\) for all \(x \in \bigcap_n \mathfrak{D}(a_n) \cap \mathfrak{D}(b_n)\).

   Then \[\begin{align} &\mathfrak{D}(c) = \mathfrak{D}(a) \cap \mathfrak{D}(b) = \{x \in \bigcap_n \mathfrak{D}(a_n) \cap \mathfrak{D}(b_n) \mid \bigvee a_n[x] < \infty \land \bigvee b_n[x] < \infty\} = \mathfrak{D}(d),\\ & c[x,y] = a[x,y] + b[x,y] = \bigvee a_n[x,y] + \bigvee b_n[x,y] = \bigvee a_n[x,y] + b_n[x,y] = d[x,y] \end{align}\] for all \(x,y \in \mathfrak{D}(c) = \mathfrak{D}(d)\), so both sides correspond to the same form and thus to the same operator.

4. \(M^\dagger \odot \left(\bigvee A_n \right) \odot M = \bigvee \left(M^\dagger \odot A_n \odot M \right)\): Let \(\bigvee A_n = A\). By Proposition [prop:orderEquivalence], \(a_n \leq a_{n+1}\) for all \(n\) and \(\bigvee a_n = a\) by the definition of the limit form. It is \(\mathfrak{D}(a) = \{x \in \bigcap_n \mathfrak{D}(a_n) \mid \bigvee a_n[x] < \infty\}\) and \(a[x,y] = \bigvee a_n[x,y]\). We show that both sides correspond to the same form and thus to the same operator by Proposition [prop:OpstoForms]:

   The form that corresponds to \(M^\dagger \odot \left(\bigvee A_n \right) \odot M = M^\dagger \odot A \odot M\) is \(c: \mathfrak{D}(c) \times \mathfrak{D}(c) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(c) &= \{x \in \mathcal{H}\mid Mx \in \mathfrak{D}(a)\}\\ c[x,y] &= a[Mx, My] \end{align}\]for all \(x,y \in \mathfrak{D}(c)\).

   The form that corresponds to \(\bigvee \left(M^\dagger \odot A_n \odot M \right)\) is \(d: \mathfrak{D}(d) \times \mathfrak{D}(d) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(d) &= \{x \in \mathcal{H}\mid Mx \in \bigcap_n \mathfrak{D}(a_n) \text{ and } \bigvee a_n[Mx] < \infty\}\\ d[x,y] &= \bigvee a_n[Mx, My] \end{align}\] for all \(x,y \in \mathfrak{D}(d)\). Then \[\begin{align} &\mathfrak{D}(c) = \{x \in \mathcal{H}\mid Mx \in \mathfrak{D}(a)\} = \{x \in \mathcal{H}\mid Mx \in \bigcap_n \mathfrak{D}(a_n) \text{ and } \bigvee a_n[Mx] < \infty\} = \mathfrak{D}(d),\\ & c[x,y] = a[Mx, My] = \bigvee a_n[Mx, My] = d[x,y] \end{align}\] for all \(x,y \in \mathfrak{D}(c) = \mathfrak{D}(d)\), so both sides correspond to the same form and thus to the same operator.

5. \(M^\dagger \odot (A \oplus B) \odot M = M^\dagger \odot A \odot M \oplus M^\dagger \odot B \odot M\): The form that corresponds to \(M^\dagger \odot (A \oplus B) \odot M\) is \(c: \mathfrak{D}(c) \times \mathfrak{D}(c) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(c) &= \{x \in \mathcal{H}\mid Mx \in \mathfrak{D}(a) \cap \mathfrak{D}(b)\}\\ c[x,y] &= a[Mx, My] + b[Mx, My] \end{align}\]for all \(x,y \in \mathfrak{D}(c)\).

   The form that corresponds to \(M^\dagger \odot A \odot M \oplus M^\dagger \odot B \odot M\) is \(d: \mathfrak{D}(d) \times \mathfrak{D}(d) \to \mathbb{C}\) with \[\begin{align} \mathfrak{D}(d) &= \{x \in \mathcal{H}\mid Mx \in \mathfrak{D}(a) \} \cap \{x \in \mathcal{H}\mid Mx \in \mathfrak{D}(b)\}\\ d[x,y] &= a[Mx, My] + b[Mx, My] \end{align}\] for all \(x,y \in \mathfrak{D}(d)\). Then \[\begin{align} \mathfrak{D}(c) &= \{x \in \mathcal{H}\mid Mx \in \mathfrak{D}(a) \cap \mathfrak{D}(b)\} = \mathfrak{D}(d),\\ c[x,y] &= a[Mx, My] + b[Mx, My] = d[x,y] \end{align}\] for all \(x,y \in \mathfrak{D}(c) = \mathfrak{D}(d)\), so both sides correspond to the same form and thus to the same operator.

 ◻

Proof. Similar to the proof of Lemma 1, we consider finite sums first, i.e., \(\sum_{n=0}^N A_n\). By Proposition [prop:ContinuityDistributivityFormSum], it is \(M^\dagger \odot \sum_{n=0}^N A_n \odot M = \sum_{n=0}^N M^\dagger \odot A_n \odot M\) for all \(N\).

By Theorem 1, there is a least upper bound of the sequence \(\{\sum_{n=0}^N A_n\}_{N}\), which is exactly \(\sum_{n=0}^\infty A_n\). Using Proposition [prop:ContinuityDistributivityFormSum], it is \[\begin{align} M^\dagger \odot (\sum_{n=0}^\infty A_n) \odot M =& \text{ }M^\dagger \odot \left(\bigvee_{N} \sum_{n=0}^N A_n\right) \odot M \\ =& \bigvee_N M^\dagger \odot \sum_{n=0}^N A_n \odot M \\ =& \bigvee_N \sum_{n=0}^N M^\dagger \odot A_n \odot M \\ =& \sum_{n=0}^\infty M^\dagger \odot A_n \odot M\qedhere \end{align}\] ◻

Proof. Let \(A,B \in \mathcal{E}(\mathcal{H})\) be bounded expectations over \(\mathcal{H}\), \(\alpha\geq 0\) and \(M\) be a bounded operator on \(\mathcal{H}\). As \(A,B\) are bounded, their \(\infty\)-restrictions \(A_\infty, B_\infty\) are bounded and thus defined on \(\mathcal{H}\). Thus the forms \(a,b\) that correspond to \(A_\infty, B_\infty\) are defined on \(\mathcal{H}\) as well (and bounded by [28]). We have \(a[x,y] = \bra{x} A \ket{y}\) and \(b[x,y] = \bra{x} B \ket{y}\) for all \(x,y \in \mathcal{H}\). Then

• Addition: \(\mathfrak{D}(c) = \mathcal{H}\) with \(c[x,y] = a[x,y] + b[x,y] = \bra{x} A+B \ket{y}\) for all \(x,y \in \mathcal{H}\).

• Scalar multiplication: \(\mathfrak{D}(\alpha \cdot a) = \mathcal{H}\) with \((\alpha \cdot a)[x,y] = \alpha \cdot a[x,y] = \bra{x} \alpha \cdot A \ket{y}\) for all \(x,y \in \mathcal{H}\).

• Application of bounded operator: \(\mathfrak{D}(a_M) = \mathcal{H}\) with \(a_M[x,y] = a[Mx, My] = \bra{Mx} A \ket{My} = \bra{x} M^\dagger A M \ket{y}\) for all \(x,y \in \mathcal{H}\).

 ◻

Proof. Assume \(A,B,C \in \mathcal{E}(\mathcal{H})\) and \(M\) bounded.

• Antisymmetric: \(A \sqsubseteq B \land B \sqsubseteq A \Rightarrow A=B\).

  \(A \sqsubseteq B\) implies \(\mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\) and the other way round, so \(\mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(B_\infty^{\frac{1}{2}})\). Also \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 = \norm{B_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\), so \(A=B\).

  Reflexive: It is \(A \sqsubseteq A\).

  Clearly \(\mathfrak{D}(A_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\) and \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{A_\infty^{\frac{1}{2}} \psi}^2\), so \(A \sqsubseteq A\).

  Transitive: \(A \sqsubseteq B \land B \sqsubseteq C \Rightarrow A \sqsubseteq C\).

  \(A \sqsubseteq B\) means \(\mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\) and \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{B_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\). \(B \sqsubseteq C\) means \(\mathfrak{D}(C_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(B_\infty^{\frac{1}{2}})\) and \(\norm{B_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{C_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(C_\infty^{\frac{1}{2}})\).

  So we have \(\mathfrak{D}(C_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\) (in particular \(\mathfrak{D}(C_\infty^{\frac{1}{2}})\subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\)) and \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{B_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{C_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(C_\infty^{\frac{1}{2}})\). Thus \(A \sqsubseteq C\).

• Let \(a,b,c\) be the forms that correspond to \(A_\infty, B_\infty, C_\infty\) and \(A \sqsubseteq B\). Then \(\mathfrak{D}(b) = \mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(a)\) and \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{B_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\).

  It is \(\mathfrak{D}((B \oplus C)_\infty^{\frac{1}{2}}) = \mathfrak{D}(b) \cap \mathfrak{D}(c) \subseteq \mathfrak{D}(a) \cap \mathfrak{D}(c) = \mathfrak{D}((A \oplus C)_\infty^{\frac{1}{2}})\). For all \(\ket{\psi} \in \mathfrak{D}((B \oplus C)_\infty^{\frac{1}{2}})\) it is \[\begin{align} \norm{(A \oplus C)_\infty^{\frac{1}{2}} \psi}^2 &= a[\psi]+ c[\psi] \leq b[\psi] + c[\psi] = \norm{(B \oplus C)_\infty^{\frac{1}{2}} \psi}^2 \end{align}\] Thus \(A \oplus C \sqsubseteq B \oplus C\).

• Let \(a,b\) be the forms that correspond to \(A_\infty, B_\infty\) and \(A \sqsubseteq B\). That means \(a\leq b\), i.e., \(\mathfrak{D}(b) \subseteq \mathfrak{D}(a)\) and \(a[x] \leq b[x]\) for all \(x \in \mathfrak{D}(b)\) by Proposition [prop:orderEquivalence]. Then \(\mathfrak{D}(b_M) = \{ \psi \in \mathcal{H}\mid M\psi \in \mathfrak{D}(b)\} \subseteq \{ \psi \in \mathcal{H}\mid M\psi \in \mathfrak{D}(a)\} = \mathfrak{D}(a_M)\). For all \(\psi \in \mathfrak{D}(b_M)\) it is \(a_M[\psi] = a[M\psi] \leq b[M\psi] = b_M[\psi]\), thus \(a_M \leq b_M\) and thus \(M^\dagger \odot A \odot M \sqsubseteq M^\dagger \odot B \odot M\) by Proposition [prop:orderEquivalence].

 ◻

Proof. In this proof we use \(\mathbb{E}_{A}\left(\rho\right)\) to denote the expectation value defined via the spectral measure in Definition 6 and \(\mathbb{E}_{A_1}\left(\rho\right)\) and \(\mathbb{E}_{A_2}\left(\rho\right)\) to denote the two equations in this lemma.

We first show the statement for pure states \(\rho = \ket{\psi}\bra{\psi}\).

It is \(\mathfrak{D}(A_\infty^{\frac{1}{2}})=\{ \ket{\psi} \mid \int \abs{\lambda} d (tr(E_\lambda \ket{\psi}\bra{\psi})) < \infty\}\) by [30].

If \(\ket{\psi} \not \in \mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(a)\), then \(\int \abs{\lambda} d (tr(E_\lambda \ket{\psi}\bra{\psi})) = \infty\) and thus \(\mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right) = \infty\) in all cases.

If \(\ket{\psi} \in \mathfrak{D}(A_\infty^{\frac{1}{2}})\), then \(\int \abs{\lambda} d (tr(E_\lambda \ket{\psi}\bra{\psi}))= \int \abs{\lambda} d (\bra{\psi}E_\lambda \ket{\psi})< \infty\). First we show equivalence between \(\mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right)\) and \(\mathbb{E}_{A_1}\left(\ket{\psi}\bra{\psi}\right)\):

We define \(I_n(x)=\begin{cases} x & \text{if } x \leq n \\ 0 & \text{otherwise} \end{cases}\) for all \(n >0\). Then \(I_n(A_\infty),I_n(A_\infty^{\frac{1}{2}})\) is a bounded operator for all \(n >0\) and \(I_n(A_\infty) \to A_\infty, I_n(A_\infty^{\frac{1}{2}}) \to A_\infty^{\frac{1}{2}}\) strongly. \[\begin{align} & \norm{A_\infty^{\frac{1}{2}} \ket{\psi}}^2 && (I_n(A_\infty^{\frac{1}{2}}) \to A_\infty^{\frac{1}{2}}\text{ strongly})\\ =& \lim_{n\to \infty} \norm{I_n(A_\infty^{\frac{1}{2}}) \ket{\psi}}^2 \\ =& \lim_{n\to \infty} \norm{(I_{n^2}(A_\infty))^{\frac{1}{2}} \ket{\psi}}^2 && (\text{def. norm})\\ =& \lim_{n\to \infty} \bra{\psi} ((I_{n^2}(A_\infty))^{\frac{1}{2}})^2 \ket{\psi} \\ =& \lim_{n\to \infty} \bra{\psi} I_{n^2}(A_\infty) \ket{\psi} \\ =& \lim_{n\to \infty} \int I_{n^2}(\lambda) d (\bra{\psi}E_\lambda \ket{\psi}) && (\text{dominated convergence theorem})\\ =& \int \lim_{n\to \infty} I_{n^2}(\lambda) d (\bra{\psi}E_\lambda \ket{\psi}) \\ =& \int \lambda d (\bra{\psi}E_\lambda \ket{\psi}) \\ =& \int \lambda d (tr(E_\lambda \ket{\psi}\bra{\psi})) \end{align}\] The dominated convergence theorem applies as \(\abs{I_{n^2}(x)} \leq x\) for all \(n>0, x\) because \(\lim_{n \to \infty} I_{n^2}(x) = x\) for all \(x\). Also \(\int \abs{\lambda} d (\bra{\psi}E_\lambda \ket{\psi}) < \infty\) because \(\ket{\psi} \in \mathfrak{D}(A_\infty^{\frac{1}{2}})\).

The equivalence between \(\mathbb{E}_{A_1}\left(\ket{\psi}\bra{\psi}\right)\) and \(\mathbb{E}_{A_2}\left(\ket{\psi}\bra{\psi}\right)\) follows from the definition of the form \(a\) that corresponds to \(A_\infty\) as \(a[\ket{\psi}] = \norm{A_\infty^{\frac{1}{2}} \ket{\psi}}^2\) for all \(\ket{\psi} \in \mathfrak{D}(a)\).

Now we consider the case of mixed states \(\rho = \sum_i p_i \ket{\psi_i}\bra{\psi_i}\) with \(p_i > 0\). If any \(\ket{\psi_i}\) is not in \(\mathfrak{D}(A_\infty^{\frac{1}{2}})\), then \(\int \abs{\lambda} d (tr(E_\lambda \ket{\psi_i}\bra{\psi_i})) = \infty\) and thus \(\mathbb{E}_{A}\left(\rho\right) = \infty\) in all cases.

If \(\ket{\psi_i} \in \mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(a)\) for all \(i\), then by [34] \[\begin{align} \mathbb{E}_{A}\left(\rho\right) = \sum_i p_i \mathbb{E}_{A}\left(\ket{\psi_i}\bra{\psi_i}\right) = \sum_i p_i \int \lambda d (tr(E_\lambda \ket{\psi_i}\bra{\psi_i})) \end{align}\] As both \(\mathbb{E}_{A_1}\left(\rho\right)\) and \(\mathbb{E}_{A_2}\left(\rho\right)\) are defined as \(\sum_i p_i \mathbb{E}_{A_1}\left(\ket{\psi_i}\bra{\psi_i}\right)\) and \(\sum_i p_i \mathbb{E}_{A_2}\left(\ket{\psi_i}\bra{\psi_i}\right)\) respectively, and we have already shown the equivalence for pure states, we are done. ◻

Proof. \(\Rightarrow\): Assume \(A \sqsubseteq B\). Then \(\mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\) and \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{B_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\). Let \(\rho \in \mathcal{D}(\mathcal{H})\) be a density operator with decomposition \(\rho = \sum_i p_i \ket{\psi_i}\bra{\psi_i}\). If there is any \(\ket{\psi_i} \not \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\), then \(\mathbb{E}_{B}\left(\rho\right) = \infty\) and thus \(\mathbb{E}_{A}\left(\rho\right) \leq \mathbb{E}_{B}\left(\rho\right)\). Otherwise, it is \[\begin{align} \mathbb{E}_{A}\left(\rho\right) =& \sum_i p_i \mathbb{E}_{A}\left(\ket{\psi_i}\bra{\psi_i}\right) = \sum_i p_i \norm{A_\infty^{\frac{1}{2}} \ket{\psi_i}}^2 \\ \leq& \sum_i p_i \norm{B_\infty^{\frac{1}{2}} \ket{\psi_i}}^2 = \sum_i p_i \mathbb{E}_{B}\left(\ket{\psi_i}\bra{\psi_i}\right) = \mathbb{E}_{B}\left(\rho\right) \end{align}\] \(\Leftarrow\): Assume that for all \(\rho \in \mathcal{D}(\mathcal{H})\) it is \(\mathbb{E}_{A}\left(\rho\right) \leq \mathbb{E}_{B}\left(\rho\right)\). Let \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\) and consider the density operator \(\rho = \ket{\psi}\bra{\psi}\). Then it is \[\begin{align} \mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right) \leq \mathbb{E}_{B}\left(\ket{\psi}\bra{\psi}\right) \end{align}\] by assumption. As \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\), it is \(\mathbb{E}_{B}\left(\ket{\psi}\bra{\psi}\right) = \norm{B_\infty^{\frac{1}{2}} \ket{\psi}}^2 < \infty\), thus \(\mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right) < \infty\) and thus \(\ket{\psi} \in \mathfrak{D}(A_\infty^{\frac{1}{2}})\), i.e., \(\mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\). Furthermore, it is \[\begin{align} \norm{A_\infty^{\frac{1}{2}} \ket{\psi}}^2 = \mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right) \leq \mathbb{E}_{B}\left(\ket{\psi}\bra{\psi}\right) = \norm{B_\infty^{\frac{1}{2}} \ket{\psi}}^2 \end{align}\] Overall, we have \(\mathfrak{D}(B_\infty^{\frac{1}{2}}) \subseteq \mathfrak{D}(A_\infty^{\frac{1}{2}})\) and \(\norm{A_\infty^{\frac{1}{2}} \psi}^2 \leq \norm{B_\infty^{\frac{1}{2}} \psi}^2\) for all \(\ket{\psi} \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\), thus \(A \sqsubseteq B\). ◻

Proof. Linearity: First we consider the sum of two expectations. Let \(A,B \in \mathcal{E}(\mathcal{H})\) and \(\rho= \sum_i p_i \ket{\psi_i}\bra{\psi_i} \in \mathcal{D}(\mathcal{H})\). We distinguish two cases:

1. There is at least one \(\ket{\psi_i} \not \in \mathfrak{D}((A \oplus B)_\infty^{\frac{1}{2}})\). If there is any \(\ket{\psi_i} \not \in \mathfrak{D}((A \oplus B)_\infty^{\frac{1}{2}})\), then \(\mathbb{E}_{A\oplus B}\left(\rho\right) = \infty\). \(\ket{\psi_i} \not \in \mathfrak{D}((A\oplus B)_\infty^{\frac{1}{2}}) = \mathfrak{D}(A_\infty^{\frac{1}{2}})\cap \mathfrak{D}(B_\infty^{\frac{1}{2}})\) implies \(\ket{\psi_i} \not \in \mathfrak{D}(A_\infty^{\frac{1}{2}})\) or \(\ket{\psi_i} \not \in \mathfrak{D}(B_\infty^{\frac{1}{2}})\) and thus \(\mathbb{E}_{A}\left(\rho\right) = \infty\) or \(\mathbb{E}_{B}\left(\rho\right) = \infty\). Thus \(\mathbb{E}_{A}\left(\rho\right) + \mathbb{E}_{B}\left(\rho\right) = \infty\).

2. All \(\ket{\psi_i} \in \mathfrak{D}((A \oplus B)_\infty^{\frac{1}{2}})\). We consider the forms \(a,b\) that correspond to \(A_\infty, B_\infty\) and \(c\) for \((A \oplus B)_\infty\). Then it is \(\ket{\psi_i} \in \mathfrak{D}(a)\) and \(\ket{\psi_i} \in \mathfrak{D}(b)\) for all \(i\) and thus \[\begin{align} \mathbb{E}_{A\oplus B}\left(\rho\right) =& \sum_i p_i \mathbb{E}_{A\oplus B}\left(\ket{\psi_i}\bra{\psi_i}\right) = \sum_i p_i c[\psi_i] = \sum_i p_i \left( a[\psi_i] + b[\psi_i] \right) \\ =& \sum_i p_i a[\psi_i] + \sum_i p_i b[\psi_i] = \mathbb{E}_{A}\left(\rho\right) + \mathbb{E}_{B}\left(\rho\right) \end{align}\]

The linearity w.r.t. states follow from the definition (more details in the proof of Lemma 3).

Scalar multiplication: For states it follows again from the definition of the expectation value (more details in the proof of Lemma 3).

For the expectation, we distinguish two cases again. Let \(A \in \mathcal{E}(\mathcal{H})\) with corresponding form \(a\) and \(cA\) the form corresponding to \(cA\) and \(\rho= \sum_i p_i \ket{\psi_i}\bra{\psi_i} \in \mathcal{D}(\mathcal{H})\).

1. There is at least one \(\ket{\psi_i} \not \in \mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(a) = \mathfrak{D}(ca) = \mathfrak{D}(cA_\infty^{\frac{1}{2}})\). Then \(\mathbb{E}_{cA}\left(\rho\right) = \infty = \mathbb{E}_{A}\left(\rho\right)\).

2. All \(\ket{\psi_i} \in \mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(cA_\infty^{\frac{1}{2}})\). Then it is \[\begin{align} \mathbb{E}_{cA}\left(\rho\right) =& \sum_i p_i \cdot \mathbb{E}_{cA}\left(\ket{\psi_i}\bra{\psi_i}\right) = \sum_i p_i \cdot ca[\psi_i] = \sum_i p_i c\cdot a[\psi_i] \\ =& \sum_i p_i \cdot c \cdot \mathbb{E}_{A}\left(\ket{\psi_i}\bra{\psi_i}\right) \\ =& \text{ } c \cdot \sum_i p_i \cdot \mathbb{E}_{A}\left(\ket{\psi_i}\bra{\psi_i}\right) = c \cdot \mathbb{E}_{A}\left(\rho\right) \end{align}\]

Continuity: We start with the sequence of expectations: Let \(\{A_i\}_i \subseteq \mathcal{E}(\mathcal{H})\) be an increasing chain of expectations, \(\rho \in \mathcal{D}(\mathcal{H})\) and \(A = \bigvee_i A_i\) (existence follows by Theorem 1). Let \(\rho = \sum_j p_j \ket{\psi_j}\bra{\psi_j}\) be a decomposition of \(\rho\) with \(p_j > 0\). We distinguish two cases:

1. There is at least one \(\ket{\psi_j} \not \in \mathfrak{D}(A_\infty^{\frac{1}{2}}) = \mathfrak{D}(a)\). Then \(\mathbb{E}_{A}\left(\rho\right) = \infty\). It also means that \(a[\psi_j] = \lim_i a_i[\psi_j] = \infty\) as otherwise \(\ket{\psi_j} \in \mathfrak{D}(a)\). If \(\ket{\psi_j}\) not in \(\mathfrak{D}(a_i)\) for at least one \(i\), then \(\mathbb{E}_{A_i}\left(\rho\right) = \infty\) and thus \(\bigvee_i \mathbb{E}_{A_i}\left(\rho\right) = \infty\). Otherwise, it is \(\ket{\psi_j} \in \mathfrak{D}(a_i)\) for all \(i\) and thus \(\mathbb{E}_{A_i}\left(\ket{\psi_j}\bra{\psi_j}\right) = a_i[\psi_j] \not = \infty\) for all \(i\). As \(\lim_i a_i[\psi_j] = \infty\), it is \(\bigvee_i p_j \mathbb{E}_{A_i}\left(\ket{\psi_j}\bra{\psi_j}\right) = \infty\) and thus \(\bigvee_i \mathbb{E}_{A_i}\left(\rho\right) \geq \bigvee_i p_j \mathbb{E}_{A_i}\left(\ket{\psi_j}\bra{\psi_j}\right) = \infty\).

2. All \(\ket{\psi_j} \in \mathfrak{D}(A_\infty^{\frac{1}{2}})\). Then it is \[\begin{align} \mathbb{E}_{A}\left(\rho\right) \overset{Lem. \ref{lem:expectAlternativeDef}}{=}& \sum_j p_j a[\psi_j] \\ \overset{Def}{=}& \sum_j p_j \lim_i a_i[\psi_j]\\ =& \sum_j \lim_i p_j a_i[\psi_j]\\ \overset{*}{=}& \lim_i \sum_j p_j a_i[\psi_j] \\ \overset{Lem. \ref{lem:expectAlternativeDef}}{=}& \lim_i \sum_j p_j \mathbb{E}_{A_i}\left(\ket{\psi_j}\bra{\psi_j}\right) \\ \overset{Incr. Seq.}{=}& \bigvee_i \sum_j p_j \mathbb{E}_{A_i}\left(\ket{\psi_j}\bra{\psi_j}\right) \\ \overset{Lem. \ref{lem:expectAlternativeDef}}{=}& \bigvee_i \mathbb{E}_{A_i}\left(\rho\right) \end{align}\] where the step marked with \(*\) follows by the monotone convergence theorem as supremum and limit coincide here because \(a_i[\psi_j]\leq a_{i+1}[\psi_j]\) for all \(i,j\).

Now we consider the sequence of states: Let \(\{ \rho_i \}_i \subseteq \mathcal{D}(\mathcal{H})\) be an increasing chain of density operators, \(A \in \mathcal{E}(\mathcal{H})\) and \(\rho = \bigvee_i \rho_i\) (existence follows by [27]). To show: \(\mathbb{E}_{A}\left(\rho\right) = \bigvee_i \mathbb{E}_{A}\left(\rho_i\right)\).

For each \(n\), define \(A_n = \int_0^n \lambda d E_\lambda\) where \(E_\lambda\) is the spectral measure of \(A_\infty\). Then \(A_n\) is a bounded operator for all \(n\) and \(A_n \to A_\infty\) strongly. We have \(\mathbb{E}_{A_n}\left(\rho\right) = tr(A_n \rho)\) and \(\mathbb{E}_{A_n}\left(\rho_i\right) = tr(A_n \rho_i)\) for all \(i,n\). This will be denoted by (1). As \(\rho_i \to \rho\) in trace norm, it is \(tr(A_n \rho_i) \to tr(A_n \rho)\) for all \(n\), denoted by (2)

As the expectation value is continuous in the expectation, it is \(\mathbb{E}_{A}\left(\rho\right) = \bigvee_n \mathbb{E}_{A_n}\left(\rho\right)\) and \(\mathbb{E}_{A}\left(\rho_i\right) = \bigvee_n \mathbb{E}_{A_n}\left(\rho_i\right)\) for all \(i\). This will be denoted by (3). Overall we have \[\begin{align} \mathbb{E}_{A}\left(\bigvee_i \rho_i\right) \overset{(3)}{=}& \bigvee_n \mathbb{E}_{A_n}\left(\bigvee_i \rho_i\right) \\ \overset{(1)}{=}& \bigvee_n tr(A_n \bigvee_i \rho_i) \\ \overset{(2)}{=}& \bigvee_n \bigvee_i tr(A_n \rho_i) \\ =& \bigvee_i \bigvee_n tr(A_n \rho_i) \\ \overset{(1)}{=}& \bigvee_i \bigvee_n \mathbb{E}_{A_n}\left(\rho_i\right) \\ \overset{(3)}{=}& \bigvee_i \mathbb{E}_{A}\left(\rho_i\right) \end{align}\] Exchanging the suprema is possible as both sequences (fixed i, varying n and fixed n, varying i) are increasing. ◻

Proof. We show the first statement. We consider finite sums \(\sum_{n=0}^N A_n\), then \(\sum_n A_n\) is \(\bigvee_N \sum_{n=0}^N A_n\). \[\begin{align} \mathbb{E}_{\sum_n A_n}\left(\rho\right) =&\text{ } \mathbb{E}_{\bigvee_N \sum_{n=0}^N A_n}\left(\rho\right) \\ =& \bigvee_N \mathbb{E}_{\sum_{n=0}^N A_n}\left(\rho\right) && (\text{continuity of the expectation})\\ =& \bigvee_N \sum_{n=0}^N \mathbb{E}_{A_n}\left(\rho\right) && (\text{linearity of the expectation})\\ =& \sum_n \mathbb{E}_{A_n}\left(\rho\right) \end{align}\]

The second statement follows analogously with finite sums \(\sum_{n=0}^N \rho_n\). ◻

Proof. Let \(a\) be the form-expectation of \(A\) and \(a_M\) the one of \(M^\dagger \odot A \odot M\). Let \(\rho = \sum_i p_i \ket{\psi_i}\bra{\psi_i}\) be a decomposition with \(p_i > 0\).

If \(\ket{\psi_i} \not \in \mathfrak{D}(a_M)\) for at least one \(i\), then \(\mathbb{E}_{M^\dagger \odot A \odot M}\left(\rho\right) = \infty\). As \(\ket{\psi_i} \not \in \mathfrak{D}(a_M) = \{ \psi \in \mathcal{H}\mid M\psi \in \mathfrak{D}(a)\}\), it is \(M\ket{\psi_i} \not \in \mathfrak{D}(a)\) and thus \(\mathbb{E}_{A}\left(M\rho M^\dagger\right) = \infty\). Thus \(\mathbb{E}_{M^\dagger \odot A \odot M}\left(\rho\right) = \mathbb{E}_{A}\left(M\rho M^\dagger\right)\).

Otherwise, \(\mathbb{E}_{M^\dagger \odot A \odot M}\left(\rho\right) = \sum_i p_i a_M[\psi_i] = \sum_i p_i a[M\psi_i] = \mathbb{E}_{A}\left(M \rho M^\dagger\right)\). ◻

Proof. We show that each \(g_i\) corresponds to a positive, symmetric and closed form \(a_i\) and then we can write \(g\) as a least upper bound of the \(a_i\) and thus it is also a positive, symmetric and closed form by Proposition [prop:OpstoForms] and Theorem 1.

It is \(a_i[\ket{\psi}] = g_i(\ket{\psi}\bra{\psi})\) for all \(\ket{\psi} \in \mathcal{H}\) (using \(\mathfrak{D}(a_i) = \mathcal{H}\) as \(g_i\), and thus \(a\), is bounded). Positivity and symmetry follow immediately from the co-domain of \(g_i\). It remains to show that \(a_i\) is closed. Let \(\ket{\psi_n}\) be a sequence in \(\mathcal{H}\) such that \(\lim_{n \to \infty} \ket{\psi_n} = \ket{\psi}\) and \(\lim_{n,m \to \infty}a_i[\ket{\psi_n} - \ket{\psi_m}] = 0\). As \(a_i\) is bounded, \(\ket{\psi} \in \mathcal{H}= \mathfrak{D}(a_i)\). It remains to show that \(\lim_{n\to\infty} a_i[\ket{\psi_n} - \ket{\psi}] = 0\): \[\begin{align} & \lim_{n\to\infty}\ket{\psi_n} = \ket{\psi}\\ \Rightarrow & \lim_{n\to\infty} \ket{\psi_n} - \ket{\psi} = 0\\ \Rightarrow & \lim_{n\to \infty} (\ket{\psi_n} - \ket{\psi})(\ket{\psi_n} - \ket{\psi})^\dagger = 0\\ \Rightarrow & \lim_{n\to \infty} g_i((\ket{\psi_n} - \ket{\psi})(\ket{\psi_n} - \ket{\psi})^\dagger) = g_i(0)\\ \Rightarrow & \lim_{n\to \infty} a_i[\ket{\psi_n} - \ket{\psi}] = 0 \end{align}\] because \(g_i\) is continuous as it is bounded and positive. ◻

Proof.

1. See [8] as \(\boldsymbol{reward} ( c)\) behaves like \(\boldsymbol{skip}\).

2. See [8] as \(\boldsymbol{reward} ( c)\) behaves like \(\boldsymbol{skip}\).

3. We already know that \(\llbracket S \rrbracket_D\) is linear and trace non-increasing. Now we do an induction over the structure to show that it can be represented in Kraus form, which implies complete positivity.

   • For \(\boldsymbol{skip}, q:=0, \overline{q}:= U\overline{q}\) and \(\boldsymbol{reward} ( c)\), the semantics have Kraus form directly.

   • For \(S_1;S_2\), if \(\llbracket S_1 \rrbracket_D\) and \(\llbracket S_2 \rrbracket_D\) can be represented in Kraus form with operators \(E_i\) and \(F_j\) respectively, then \(\llbracket S_2 \rrbracket_D(\llbracket S_1 \rrbracket_D(\rho)) = \sum_{i,j} F_j E_i \rho E_i^\dagger F_j^\dagger\) is a Kraus representation of \(\llbracket S_1;S_2 \rrbracket\).

   • For \(\boldsymbol{measure } M[\overline{q}]:\overline{S}\), if \(\llbracket S_m \rrbracket_D\) can be represented in Kraus form with operators \(E_{m,i}\) for all \(m\), then we obtain a Kraus representation by \[\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S} \rrbracket_D(\rho) = \sum_{m,i} E_{m,i} M_m \rho M_m^\dagger E_{m,i}^\dagger.\]

   • For \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S\), we define \(\mathcal{M}_0(\rho) = M_0 \rho M_0^\dagger\) and \(\mathcal{M}_1(\rho) = M_1 \rho M_1^\dagger\) for all \(\rho \in \mathcal{D}(\mathcal{H})\). Then we define \[\begin{align} W_0 =& \text{ }\Omega = 0\\ W_{i+1} =& \text{ }\llbracket \boldsymbol{if }M[\overline{q}]=1 \boldsymbol{ then } S; W_i \rrbracket_D \\ =& \text{ }\mathcal{M}_1 \circ \llbracket S \rrbracket_D \circ W_i + \mathcal{M}_0 \end{align}\] Intuitively, \(W_i\) corresponds to the semantics of the program that executes at most \(i\) iterations of the loop and then terminates. Then we can show \(W_i = \sum_{k=0}^{i-1} (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0\) by induction over \(i\).

     • \(i=1\): \(W_1 = \mathcal{M}_1 \circ \llbracket S \rrbracket_D \circ W_0 + \mathcal{M}_0 = \mathcal{M}_0 = \sum_{k=0}^0 (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0\).

     • \(i \to i+1\): We have \[\begin{align} W_{i+1} =& \text{ }\mathcal{M}_1 \circ \llbracket S \rrbracket_D \circ W_i + \mathcal{M}_0 \\ =& \text{ }\mathcal{M}_1 \circ \llbracket S \rrbracket_D \circ \sum_{k=0}^{i-1} (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0 + \mathcal{M}_0 \\ =& \sum_{k=1}^{i} (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0 + \mathcal{M}_0 \\ =& \sum_{k=0}^{i} (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0 \end{align}\]

     As \(\mathcal{M}_1\) and \(\llbracket S \rrbracket_D\) can be represented in Kraus form, \(W_i\) can be represented in Kraus form as well by the previous cases, i.e., it is completely positive. We can show that \(W_{i+1}-W_i\) can be represented in Kraus form as well: \[\begin{align} W_{i+1} - W_i =& \sum_{k=0}^{i} (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0 - \sum_{k=0}^{i-1} (\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^k \circ \mathcal{M}_0 \\ =& \text{ }(\mathcal{M}_1 \circ \llbracket S \rrbracket_D)^i \circ \mathcal{M}_0 \end{align}\] which can be represented in Kraus form by the previous cases as it is finite concatenation of Kraus-representable maps.

     Then we have \(\bigvee_{i=0}^\infty W_i = \sum_{i=0}^{\infty} W_{i+1}-W_i\) where each summand \(W_{i+1}-W_i\) can be represented in Kraus form, which implies that \(\sum_{i=0}^\infty W_{i+1}-W_i\) can be represented in Kraus form as well by taking the union of the Kraus operators for all \(i\) [40].

4. \(\llbracket S \rrbracket_{R}(\rho)\) is linear in \(\rho\) can be shown by induction over the structure of \(S\). Let \(\rho, \sigma \in \mathcal{D}(\mathcal{H})\) and \(\alpha, \beta \in \mathbb{C}\) such that \(\alpha \rho, \beta \sigma, \alpha \rho + \beta \sigma \in \mathcal{D}(\mathcal{H})\).

   • For \(\boldsymbol{skip}, q:=0, \overline{q}:= U\overline{q}\) it follows immediately from the definition (\(=0\) always).

   • For \(\boldsymbol{reward} ( c)\), we have \[\begin{align} & \text{ }\llbracket \boldsymbol{reward} ( c) \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \text{ }c \cdot tr(\alpha \rho + \beta \sigma) \\ =& \text{ }c\cdot (\alpha tr(\rho) + \beta tr(\sigma)) \\ = & \text{ }\alpha \cdot \llbracket \boldsymbol{reward} ( c) \rrbracket_{R}(\rho) + \beta \cdot \llbracket \boldsymbol{reward} ( c) \rrbracket_{R}(\sigma) \end{align}\] as the trace is linear.

   • For \(S_1;S_2\), we have \[\begin{align} &\text{ }\llbracket S_1;S_2 \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \text{ }\llbracket S_2 \rrbracket_{R}(\llbracket S_1 \rrbracket_D(\alpha \rho + \beta \sigma)) + \llbracket S_1 \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \text{ }\llbracket S_2 \rrbracket_{R}(\alpha \llbracket S_1 \rrbracket_D(\rho) + \beta \llbracket S_1 \rrbracket_D( \sigma)) + \llbracket S_1 \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \text{ }\alpha\llbracket S_2 \rrbracket_{R}( \llbracket S_1 \rrbracket_D(\rho)) + \beta \llbracket S_2 \rrbracket_{R}(\llbracket S_1 \rrbracket_D( \sigma)) + \alpha \llbracket S_1 \rrbracket_{R}(\rho) + \beta \llbracket S_1 \rrbracket_{R}(\sigma) \\ =& \text{ }\alpha \cdot \llbracket S_2 \rrbracket_{R}(\llbracket S_1 \rrbracket_D(\rho),\llbracket S_1 \rrbracket_{R}(\rho)) + \beta \cdot \llbracket S_2 \rrbracket_{R}(\llbracket S_1 \rrbracket_D( \sigma),\llbracket S_1 \rrbracket_{R}(\sigma)) \\ =& \text{ }\alpha \cdot \llbracket S_1;S_2 \rrbracket_{R}(\rho) + \beta \cdot \llbracket S_1;S_2 \rrbracket_{R}(\sigma) \end{align}\]

   • For \(\boldsymbol{measure } M[\overline{q}]:\overline{S}\), we have \[\begin{align} &\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S} \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \sum_m \llbracket S_m \rrbracket_{R}(M_m (\alpha \rho + \beta \sigma) M_m^\dagger) \\ =& \sum_m \llbracket S_m \rrbracket_{R}(\alpha M_m \rho M_m^\dagger + \beta M_m \sigma M_m^\dagger) \\ =& \sum_m [\alpha\llbracket S_m \rrbracket_{R}(M_m \rho M_m^\dagger) + \beta\llbracket S_m \rrbracket_{R}(M_m \sigma M_m^\dagger)]\\ =&\text{ } \alpha\sum_m\llbracket S_m \rrbracket_{R}(M_m \rho M_m^\dagger) + \beta\sum_m\llbracket S_m \rrbracket_{R}(M_m \sigma M_m^\dagger)\\ =& \text{ } \alpha\cdot\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S} \rrbracket_{R}(\rho) + \beta\cdot\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S} \rrbracket_{R}(\sigma) \end{align}\]

   • For \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S\), we have \[\begin{align} &\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \lim_{i \to \infty} \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^i \rrbracket_{R}(\alpha \rho + \beta \sigma) \\ =& \lim_{i \to \infty} \alpha\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^i \rrbracket_{R}(\rho) + \beta\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^i \rrbracket_{R}(\sigma) \\ =& \text{ }\alpha\cdot\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket_{R}(\rho) + \beta\cdot\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket_{R}(\sigma) \end{align}\] by induction hypothesis (for \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^i\)) and the fact that limits preserve linearity for positive sequences.

5. \(a[\ket{\psi}] := \llbracket S \rrbracket_{R}(\ket{\psi} \bra{\psi})\) for all \(\ket{\psi} \in \mathfrak{D}(a) = \{\ket{\psi} \in \mathcal{H}\mid \llbracket S \rrbracket_{R}(\ket{\psi} \bra{\psi}) < \infty \}\) is a symmetric, positive and closed form. Positivity follows immediately from the previous points and symmetry follows from the co-domain of \(\llbracket S \rrbracket_{R}\). We show closeness by induction over the structure of \(S\):

   • For \(\boldsymbol{skip}, q:=0\) and \(\overline{q}:= U\overline{q}\) is \(a\) exactly the zero form, which is closed.

   • For \(\boldsymbol{reward} ( c)\), we distinguish between \(c < \infty\) and \(c = \infty\). If \(c < \infty\), then \(a\) is defined on \(\mathcal{H}\) and is closed (e.g., by Proposition [prop:OpstoForms]as it corresponds to the self-adjoint operator \(c\boldsymbol{I}\)). If \(c = \infty\), then \(a\) is the infinity form that is zero on the zero vector and \(\infty\) everywhere else, which is also closed.

   • For \(S_1;S_2\), let \(a_1\) and \(a_2\) be the (closed, positive, symmetric) forms corresponding to \(S_1\) and \(S_2\) respectively. We know that \(\llbracket S_1 \rrbracket_D\) has a Kraus representation by the previous points and thus we can write \(\llbracket S_1 \rrbracket_D(\ket{\psi}\bra{\psi}) = \sum_i E_i \ket{\psi}\bra{\psi} E_i^\dagger\). Then we have \(a[\ket{\psi}] = \llbracket S_1 \rrbracket_{R}(\ket{\psi}\bra{\psi}) + \llbracket S_2 \rrbracket_{R}(\llbracket S_1 \rrbracket_D(\ket{\psi}\bra{\psi})) = a_1[\ket{\psi}] + \sum_i a_2[E_i \ket{\psi}]\). Then \(a\) is closed by Proposition [prop:FormAddMult] and Lemma 1.

   • For \(\boldsymbol{measure } M[\overline{q}]:\overline{S}\), let \(a_m\) be the (closed, positive, symmetric) form corresponding to \(S_m\) for all \(m\). We have \(a[\ket{\psi}] = \sum_m a_m[M_m \ket{\psi}]\). Then \(a\) is closed by Proposition [prop:FormAddMult] and Lemma 1.

   • For \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S\), we have \(a[\ket{\psi}] = \lim_{i \to \infty} a_i[\ket{\psi}]\) where \(a_i\) is the form corresponding to \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^i\). We can write \(a_i\) as a sum of forms corresponding to sequences of program statements (by induction hypothesis)without loops and thus we can write \(a_i\) as a least upper bound of an increasing sequence of closed forms by Proposition [prop:OpstoForms] and Theorem 1.

 ◻

Proof.

1. By definition and because \(\llbracket S \rrbracket_D\) is trace non-increasing (thus the term in square brackets is non-negative) and for reward-free programs is \(\llbracket S \rrbracket_{R}(\rho)= 0\).

2. \(\mathbb{E}_{\boldsymbol{0}}\left(\rho\right) = 0 \leq \mathbb{E}_{A}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho)\) for all \(\rho\).

3. \[\begin{align} &\mathbb{E}_{A}\left(\rho\right) \leq \mathbb{E}_{\boldsymbol{I}}\left(\rho\right) = tr(\rho) \\ \Rightarrow \text{ }&\mathbb{E}_{A}\left(\rho\right) \leq tr(\rho) = tr(\llbracket S \rrbracket_D(\rho)) + [tr(\rho) - tr(\llbracket S \rrbracket_D(\rho))] \\ \Rightarrow \text{ }&\mathbb{E}_{A}\left(\rho\right) \leq \mathbb{E}_{\boldsymbol{I}}\left(\llbracket S \rrbracket_D(\rho)\right) + [tr(\rho) - tr(\llbracket S \rrbracket_D(\rho))]\qedhere \end{align}\]

 ◻

Proof.

• It is \(\mathbb{E}_{\boldsymbol{0}_{\mathcal{H}}}\left(\llbracket S \rrbracket_D(\rho)\right) = 0 = \mathbb{E}_{wp\llbracket S \rrbracket (\boldsymbol{0}_{\mathcal{H}})}\left(\rho\right)\) for all \(\rho\), so \(wp\llbracket S \rrbracket (\boldsymbol{0}_{\mathcal{H}}) = \boldsymbol{0}_{\mathcal{H}}\) as \(\llbracket S \rrbracket_{R}(\rho) = 0\) for reward-free programs.

• Follows by the linearity of expectation values (Proposition [prop:expectationProperties]): \[\begin{align} \mathbb{E}_{wp\llbracket S \rrbracket (c B)}\left(\rho\right) &= \mathbb{E}_{c B}\left(\llbracket S \rrbracket_D(\rho)\right) = c \cdot \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) \\ &= c \cdot \mathbb{E}_{wp\llbracket S \rrbracket (B)}\left(\rho\right) = \mathbb{E}_{c \cdot wp\llbracket S \rrbracket (B)}\left(\rho\right) \\ \mathbb{E}_{wp\llbracket S \rrbracket (B_1 \oplus B_2)}\left(\rho\right) &= \mathbb{E}_{B_1 \oplus B_2}\left(\llbracket S \rrbracket_D(\rho)\right) = \mathbb{E}_{B_1}\left(\llbracket S \rrbracket_D(\rho)\right) + \mathbb{E}_{B_2}\left(\llbracket S \rrbracket_D(\rho)\right) \\ &= \mathbb{E}_{wp\llbracket S \rrbracket (B_1)}\left(\rho\right) + \mathbb{E}_{wp\llbracket S \rrbracket (B_2)}\left(\rho\right) \\ & = \mathbb{E}_{wp\llbracket S \rrbracket (B_1) \oplus wp\llbracket S \rrbracket (B_2)}\left(\rho\right) \end{align}\] This holds for all \(\rho \in \mathcal{D}(\mathcal{H})\) and we conclude that \(wp\llbracket S \rrbracket (c B) = c \cdot wp\llbracket S \rrbracket (B)\) and \(wp\llbracket S \rrbracket (B_1 \oplus B_2) = wp\llbracket S \rrbracket (B_1) \oplus wp\llbracket S \rrbracket (B_2)\) by Lemma 4 and because \(\sqsubseteq\) is a partial order and thus in particular antisymmetric. Note that this property does not hold for programs with rewards as the reward term \(\llbracket S \rrbracket_{R}(\rho)\) is not \(0\) then.

• Follows by Lemma 4: \[\begin{align} &B_1 \sqsubseteq B_2 \\ \Rightarrow &\text{ } \forall \rho \in \mathcal{D}(\mathcal{H}) : \mathbb{E}_{B_1}\left(\llbracket S \rrbracket_D(\rho)\right) \leq \mathbb{E}_{B_2}\left(\llbracket S \rrbracket_D(\rho)\right) \\ \Rightarrow & \text{ }\forall \rho \in \mathcal{D}(\mathcal{H}) : \mathbb{E}_{wp\llbracket S \rrbracket (B_1)}\left(\rho\right) + \llbracket S \rrbracket_{R}(\rho) \leq \mathbb{E}_{wp\llbracket S \rrbracket (B_2)}\left(\rho\right) + \llbracket S \rrbracket_{R}(\rho)\\ \Rightarrow & \text{ }\forall \rho \in \mathcal{D}(\mathcal{H}) : \mathbb{E}_{wp\llbracket S \rrbracket (B_1)}\left(\rho\right) \leq \mathbb{E}_{wp\llbracket S \rrbracket (B_2)}\left(\rho\right)\\ \Rightarrow & \text{ }wp\llbracket S \rrbracket (B_1) \sqsubseteq wp\llbracket S \rrbracket (B_2) \end{align}\]

• The existence of both suprema follows by Theorem 1 and the monotonicity. The equivalence follows by continuity of expectation values (Proposition [prop:expectationProperties]): \[\begin{align} \mathbb{E}_{wp\llbracket S \rrbracket (\bigvee_n B_n)}\left(\rho\right) &= \mathbb{E}_{\bigvee_n B_n}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho) \\ &= \bigvee_n \mathbb{E}_{B_n}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho) \\ &= \bigvee_n \mathbb{E}_{wp\llbracket S \rrbracket (B_n)}\left(\rho\right) = \mathbb{E}_{\bigvee_n wp\llbracket S \rrbracket (B_n)}\left(\rho\right) \end{align}\] and the same argument as given in the proof of linearity.

 ◻

Proof. In the following we will use \(a\) (and later \(A\)) for the precondition and \(b\) (and \(B\)) for the postcondition.

By Definition 7, we can use the Kraus representation of \(\llbracket S \rrbracket_D\) and write \(\llbracket S \rrbracket_D(\rho) = \sum_i E_i \rho E_i^\dagger\) as a sum for some bounded operators \(E_i\). They are not unique, but for now we fix one family \(E_i\) (later we will show that it does not matter which representation we choose). Then we define \[\begin{align} a_i &= \lambda \psi. b_{E_i}[\ket{\psi}]+ \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\\ \hat{a_j} &= \sum_{i\leq j} a_i\\ a &= \bigvee_j \hat{a_j} \end{align}\] As \(b\in \mathcal{F}(\mathcal{H})\), \(b_{E_i} \in \mathcal{F}(\mathcal{H})\) by Proposition [prop:FormAddMult] as it is just applying a bounded operator \(E_i\). \(\llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\) corresponds also to a form-expectation by Definition 7. Thus \(a_i\) (as the sum of two form-expectations) is a form-expectation by Proposition [prop:FormAddMult].

\(\hat{a_j}\) is a finite sum, we can apply Proposition [prop:FormAddMult] again and obtain that \(\hat{a_j} \in \mathcal{F}(\mathcal{H})\) for all \(j\) again. As \(a_i\) is positive for all \(i\) , \(\hat{a_j}\) is increasing in \(j\).

Then we can also consider the corresponding expectations \(\hat{A}_j\) for each \(j\). They form an increasing chain of expectations by Proposition[prop:orderEquivalence], thus the corresponding least upper bound \(\bigvee_j \hat{A}_j\) exists by Theorem 1 and is an expectation and \(a\) is its corresponding form, so \(a \in \mathcal{F}(\mathcal{H})\).

Now we show that \(wp\llbracket S \rrbracket (B)\) is the corresponding expectation of \(a = wp_f\llbracket S \rrbracket (b)\). By the above part, we know that there exists a corresponding expectation \(A\) to \(a\).

First we show that \(\mathbb{E}_{B}\left(\llbracket S \rrbracket(\ket{\psi}\bra{\psi})\right) + \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})= \mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right)\) holds for all \(\ket{\psi}\). Let \(\ket{\psi}\in \mathcal{H}\). Then \(\llbracket S \rrbracket(\ket{\psi}\bra{\psi}) = \sum_i E_i \ket{\psi}\bra{\psi} E_i^\dagger\).

If there is at least one \(E_i \ket{\psi} \not \in \mathfrak{D}(B)\) then \(\ket{\psi} \not \in \mathfrak{D}(a)\) and both sides are \(\infty\).

If all \(E_i \ket{\psi} \in \mathfrak{D}(B)\), then \[\begin{align} &\text{ } \mathbb{E}_{B}\left(\llbracket S \rrbracket(\ket{\psi}\bra{\psi})\right) + \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\\ =& \text{ }\mathbb{E}_{B}\left(\sum_i E_i \ket{\psi} \bra{\psi}E_i^\dagger\right) + \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\\ =& \sum_i \mathbb{E}_{B}\left(E_i \ket{\psi} \bra{\psi}E_i^\dagger\right) + \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\\ =& \sum_i b[E_i \ket{\psi}]+ \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\\ & = \sum_i a_i[\ket{\psi}] = a[\ket{\psi}] =\mathbb{E}_{A}\left(\ket{\psi}\bra{\psi}\right) \end{align}\]

We can conclude that \(\mathbb{E}_{A}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho)\) for all \(\rho = \sum_i p_i \ket{\psi_i}\bra{\psi_i}\): \[\begin{align} \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho) &= \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\sum_i p_i \ket{\psi_i}\bra{\psi_i})\right) + \llbracket S \rrbracket_{R}(\sum_i p_i\ket{\psi_i}\bra{\psi_i})\\ &= \mathbb{E}_{B}\left(\sum_i p_i \llbracket S \rrbracket_D(\ket{\psi_i}\bra{\psi_i})\right)+ \sum_i p_i \llbracket S \rrbracket_{R}(\ket{\psi_i}\bra{\psi_i})\\ &= \sum_i p_i \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\ket{\psi_i}\bra{\psi_i})\right) + \sum_i p_i \llbracket S \rrbracket_{R}(\ket{\psi_i}\bra{\psi_i})\\ &= \sum_i p_i \left(\mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\ket{\psi_i}\bra{\psi_i})\right) + \llbracket S \rrbracket_{R}(\ket{\psi_i}\bra{\psi_i})\right)\\ &= \sum_i p_i \mathbb{E}_{A}\left(\ket{\psi_i}\bra{\psi_i}\right) = \mathbb{E}_{A}\left(\sum_i p_i \ket{\psi_i}\bra{\psi_i}\right) \\ &= \mathbb{E}_{A}\left(\rho\right) \end{align}\] as \(\llbracket S \rrbracket_D, \llbracket S \rrbracket_{R}\) and \(\mathbb{E}\) are linear.

In the beginning, we fixed one Kraus representation \(E_i\). Now lets assume there is another one \(F_j\) with \(\llbracket S \rrbracket_D^F(\rho) := \sum_j F_j \rho F_j^\dagger =\llbracket S \rrbracket_D(\rho)= \sum_i E_i \rho E_i^\dagger =: \llbracket S \rrbracket_D^E(\rho)\) for all \(\rho\). Let \(A_F\) and \(A_E\) be the corresponding expectations to \(wp_f\llbracket S_F \rrbracket (a)\) and \(wp_f\llbracket S_E \rrbracket (a)\) respectively. Then for all \(\rho\) \[\begin{align} \mathbb{E}_{A_F}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D^F(\rho)\right) + \llbracket S \rrbracket_{R}(\rho) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D^E(\rho)\right) + \llbracket S \rrbracket_{R}(\rho) = \mathbb{E}_{A_E}\left(\rho\right). \end{align}\] Together with the fact that \(\sqsubseteq\) is a partial order and thus antisymmetric by Proposition [prop:orderproperties] and Lemma 4, we conclude \(wp_f\llbracket S_F \rrbracket (a) = wp_f\llbracket S_E \rrbracket (a)\) and thus the definition does not depend on the choice of Kraus operators. ◻

Proof. We have to check two things:

1. \(wp\llbracket S \rrbracket (B)\) is an expectation, and

2. \(\mathbb{E}_{wp\llbracket S \rrbracket (B)}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket S \rrbracket_D(\rho)\right) + \llbracket S \rrbracket_{R}(\rho)\) for all \(\rho \in \mathcal{D}(\mathcal{H})\).

We show both statements together by an induction on the structure of \(S\). Let \(\rho = \sum_i p_i \ket{\psi_i}\bra{\psi_i} \in \mathcal{D}(\mathcal{H})\) with \(p_i>0\) and \(B\in \mathcal{E}(\mathcal{H})\) with corresponding form \(b \in \mathcal{F}(\mathcal{H})\).

• \(S = \boldsymbol{skip}\): Trivial as \(wp\llbracket \boldsymbol{skip} \rrbracket (B) = B\) and \(\llbracket \boldsymbol{skip} \rrbracket_D(\rho)=\rho\), \(\llbracket \boldsymbol{skip} \rrbracket_{R}(\rho) = 0\) for all \(\rho \in \mathcal{D}(\mathcal{H})\).

• \(S = q:=0\):

  1. \(wp\llbracket q:=0 \rrbracket (B) \in \mathcal{E}(\mathcal{H})\) by Definition 5 as \(\ket{n}\bra{0}\) are bounded operators. The sum is infinite and by Lemma 1 in \(\mathcal{E}(\mathcal{H})\).

  2. It is \[\begin{align} \mathbb{E}_{wp\llbracket q:=0 \rrbracket (B)}\left(\rho\right) =& \text{ }\mathbb{E}_{\sum_n \ket{n}\bra{0} \odot B \odot \ket{0}\bra{n}}\left(\rho\right) \\ =& \sum_n \mathbb{E}_{\ket{n}\bra{0} \odot B \odot \ket{0}\bra{n}}\left(\rho\right) \\ =& \sum_n \mathbb{E}_{B}\left(\ket{0}\bra{n} \rho \ket{n}\bra{0}\right) \\ =& \text{ }\mathbb{E}_{B}\left(\sum_n \ket{0}\bra{n} \rho \ket{n}\bra{0}\right) \\ =& \text{ }\mathbb{E}_{B}\left(\llbracket q:=0 \rrbracket_D(\rho)\right) \end{align}\] as \(\mathbb{E}\) is linear in both the state and the expectation (Lemma 5) and we can move bounded operators from the expectation to the density operator by Proposition [prop:boundedOpinExpectation]. As \(\llbracket q:=0 \rrbracket_{R}(\rho) = 0\) for all \(\rho\), we have \(\mathbb{E}_{wp\llbracket q:=0 \rrbracket (B)}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket q:=0 \rrbracket_D(\rho)\right) + \llbracket q:=0 \rrbracket_{R}(\rho)\).

• \(S = \overline{q}:= U\overline{q}\):

  1. \(wp\llbracket \overline{q}:= U\overline{q} \rrbracket (B)\in \mathcal{E}(\mathcal{H})\) by Definition 5 as \(U\) is a bounded operator.

  2. Let \(wp\) the corresponding form of \(wp\llbracket \overline{q}:= U\overline{q} \rrbracket (B)_\infty\). It is \(\mathfrak{D}(wp) = \{\ket{\psi} \in \mathcal{H}\mid U\ket{\psi} \in \mathfrak{D}(b)\}\).

     1. If there is (at least) one \(\ket{\psi_i}\not \in \mathfrak{D}(wp)\), then \(\mathbb{E}_{wp\llbracket S \rrbracket (B)}\left(\rho\right) = \infty\). By the definition of \(\mathfrak{D}(wp)\), we have \(\mathbb{E}_{B}\left(\llbracket \overline{q}:= U\overline{q} \rrbracket_D(\ket{\psi_i}\bra{\psi_i})\right) = \infty\). Overall it is \(\mathbb{E}_{wp\llbracket \overline{q}:= U\overline{q} \rrbracket (B)}\left(\rho\right) =\infty = \mathbb{E}_{B}\left(\llbracket \overline{q}:= U\overline{q} \rrbracket_D(\rho)\right)\) by linearity.

     2. If \(\ket{\psi_i} \in \mathfrak{D}(wp)\) for all \(i\), then \[\begin{align} \mathbb{E}_{wp\llbracket \overline{q}:= U\overline{q} \rrbracket (B)}\left(\rho\right) & = \sum_i p_i wp[\ket{\psi_i}]\\ &= \sum_i p_i b[U\ket{\psi_i}] \\ &= \sum_i p_i \mathbb{E}_{B}\left(\llbracket \overline{q}:= U\overline{q} \rrbracket_D(\ket{\psi_i}\bra{\psi_i})\right) \\ &= \mathbb{E}_{B}\left(\llbracket \overline{q}:= U\overline{q} \rrbracket_D(\rho)\right) \end{align}\]

     Overall we have \(\mathbb{E}_{wp\llbracket \overline{q}:= U\overline{q} \rrbracket (B)}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket \overline{q}:= U\overline{q} \rrbracket_D(\rho)\right) + \llbracket \overline{q}:= U\overline{q} \rrbracket_{R}(\rho)\) as \(\llbracket \overline{q}:= U\overline{q} \rrbracket_{R}(\rho) = 0\) for all \(\rho\).

• \(S = \boldsymbol{reward} ( c)\):

  1. \(wp\llbracket \boldsymbol{reward} ( c) \rrbracket (B) = B \oplus c \cdot \boldsymbol{I}\) is in \(\mathcal{E}(\mathcal{H})\) by Definition 5.

  2. It is \(\mathbb{E}_{wp\llbracket \boldsymbol{reward} ( c) \rrbracket (B)}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket \boldsymbol{reward} ( c) \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{reward} ( c) \rrbracket_{R}(\rho)\) as \[\begin{align} \mathbb{E}_{wp\llbracket \boldsymbol{reward} ( c) \rrbracket (B)}\left(\rho\right) &= \mathbb{E}_{B \oplus c \cdot \boldsymbol{I}}\left(\rho\right) \\ & = \mathbb{E}_{B}\left(\llbracket \boldsymbol{reward} ( c) \rrbracket_D(\rho)\right) + \mathbb{E}_{c \cdot \boldsymbol{I}}\left(\rho\right) \\ &= \mathbb{E}_{B}\left(\llbracket \boldsymbol{reward} ( c) \rrbracket_D(\rho)\right) + c \cdot tr(\rho) \\ &= \mathbb{E}_{B}\left(\llbracket \boldsymbol{reward} ( c) \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{reward} ( c) \rrbracket_{R}(\rho) \end{align}\] by linearity of expectation values (Proposition [prop:expectationProperties]).

• \(S = S_1;S_2\):

  1. \(wp\llbracket S_1 \rrbracket (wp\llbracket S_2 \rrbracket (B)) \in \mathcal{E}(\mathcal{H})\) follows immediately from the induction hypothesis.

  2. \[\begin{align} \mathbb{E}_{wp\llbracket S_1;S_2 \rrbracket (B)}\left(\rho\right) & = \mathbb{E}_{wp\llbracket S_1 \rrbracket (wp\llbracket S_2 \rrbracket (B))}\left(\rho\right) \\ &\overset{IH}{=} \mathbb{E}_{wp\llbracket S_2 \rrbracket (B)}\left(\llbracket S_1 \rrbracket_D(\rho)\right) + \llbracket S_1 \rrbracket_{R}(\rho) \\ &\overset{IH}{=} \mathbb{E}_{B}\left(\llbracket S_2 \rrbracket_D(\llbracket S_1 \rrbracket_D(\rho))\right) + \llbracket S_2 \rrbracket_{R}(\llbracket S_1 \rrbracket_D(\rho)) + \llbracket S_1 \rrbracket_{R}(\rho) \\ &= \mathbb{E}_{B}\left(\llbracket S_1;S_2 \rrbracket_D(\rho)\right) + \llbracket S_1;S_2 \rrbracket_{R}(\rho) \end{align}\]

• \(S = \boldsymbol{measure } M[\overline{q}]:\overline{S'}\):

  1. By induction hypothesis, \(wp\llbracket S_m' \rrbracket (B) \in \mathcal{E}(\mathcal{H})\) for all \(m\). Then by Definition 5, \(M_m^\dagger \odot wp\llbracket S_m' \rrbracket (B) \odot M_m \in \mathcal{E}(\mathcal{H})\) for all \(m\) as \(M_m\) are bounded operators. We can define \(\hat{f}_n = \sum_{m\leq n} M_m^\dagger \odot wp\llbracket S_m' \rrbracket (B) \odot M_m\). As each \(M_m^\dagger \odot wp\llbracket S_m' \rrbracket (B) \odot M_m \in \mathcal{E}(\mathcal{H})\), \(\hat{f}_n \in \mathcal{E}(\mathcal{H})\) for all \(n\) as it is a finite sum by Definition 5. As \(\hat{f}_n\) is an increasing chain (each \(M_m^\dagger \odot wp\llbracket S_m' \rrbracket (B) \odot M_m\) is positive), by Theorem 1, the least upper bound \(\bigvee_n \hat{A}_n\) exists and corresponds to \(\sum_m M_m^\dagger \odot wp\llbracket S_m' \rrbracket (B) \odot M_m\).

  2. Let \(wp\) be the form-expectation of \(wp\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (B)\) and \(wp_m\) the one of \(wp\llbracket S_m' \rrbracket (B)\). It is \(\mathfrak{D}(wp) = \bigcap_m \{\ket{\psi}\mid M_m \ket{\psi} \in \mathfrak{D}(wp_m)\}\).

     1. If there is an \(i\) such that \(\ket{\psi_i}\not \in \mathfrak{D}(wp)\), then there must be a \(j\) such that \(M_j \ket{\psi_i} \not \in \mathfrak{D}(wp_j)\) and thus \[\begin{align} \infty =& \mathbb{E}_{wp\llbracket S_j' \rrbracket (B)}\left(\ket{M_j \psi_i}\bra{M_j \psi_i}\right) \\ \overset{IH}{=}&\mathbb{E}_{B}\left(\llbracket S_j' \rrbracket_D(\ket{M_j \psi_i}\bra{M_j \psi_i})\right) + \llbracket S_j' \rrbracket_{R}(\ket{M_j \psi_i}\bra{M_j \psi_i}) \end{align}\] By linearity of semantics (Proposition [prop:semanticsProperties]) and expectation values (Proposition [prop:expectationProperties], Lemma 5): \[\begin{align} &\mathbb{E}_{B}\left(\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_{R}(\rho)\\ =& \infty = \mathbb{E}_{wp\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S} \rrbracket (B)}\left(\rho\right). \end{align}\]

     2. Assume \(\ket{\psi_i} \in \mathfrak{D}(wp)\) for all \(i\), then \(M_m \ket{\psi_i} \in \mathfrak{D}(wp_m)\) for all \(i,m\). Then \[\begin{align} &\mathbb{E}_{wp\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S} \rrbracket (B)}\left(\rho\right) \\ =& \sum_{m} \mathbb{E}_{M_m^\dagger \odot wp\llbracket S_m' \rrbracket (B) \odot M_m}\left(\rho\right) \\ = & \sum_{m} \sum_i p_i wp_m[M_m \ket{\psi_i}] \\ \overset{IH}{=} &\sum_{m} \sum_i p_i \mathbb{E}_{B}\left(\llbracket S_m' \rrbracket_D(\ket{M_m \psi_i}\bra{M_m \psi_i})\right) + \llbracket S_m' \rrbracket_{R}(\ket{M_j \psi_i}\bra{M_j \psi_i}) \\ = &\sum_i p_i \sum_{m} \mathbb{E}_{B}\left(\llbracket S_m' \rrbracket_D(\ket{M_m \psi_i}\bra{M_m \psi_i})\right) + \llbracket S_m' \rrbracket_{R}(\ket{M_j \psi_i}\bra{M_j \psi_i})\\ =& \sum_i p_i \mathbb{E}_{B}\left(\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_D(\ket{\psi_i}\bra{\psi_i})\right) \\ & +\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_{R}(\ket{\psi_i}\bra{\psi_i}) \\ =& \mathbb{E}_{B}\left(\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_{R}(\rho) \end{align}\] As \(\mathbb{E}_{B}\left(\ket{\psi}\bra{\psi}\right), \llbracket S \rrbracket_{R}(\ket{\psi}\bra{\psi})\) and \(p_i\) are non-negative for all \(\ket{\psi}, S\), we can switch the sums in the forth step due to Fubini’s theorem for infinite series. We also use linearity of semantics (Proposition [prop:semanticsProperties]) and expectation values (Proposition [prop:expectationProperties], Lemma 5).

• \(S = \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'\): In this case we prove both parts together. First of all, we show \(wp\llbracket S' \rrbracket (A_n) \in \mathcal{E}(\mathcal{H})\) for all \(n\). Each \(A_n \in \mathcal{E}(\mathcal{H})\) because it is defined via sums and applications of bounded operators on expectations (see Definition 5). Now it reminds to show that \(\{A_n\}_n\) is an increasing chain, then the least upper bound \(\bigvee_n A_n\) exists by Theorem 1 and is in \(\mathcal{E}(\mathcal{H})\).

  First we show \[\begin{align} \label{align:expectAn} \mathbb{E}_{A_n}\left(\rho\right) = \mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\rho) \end{align}\tag{1}\] by induction on \(n\):

  • \(n=0\): \[\begin{align} \mathbb{E}_{A_0}\left(\rho\right) =& \text{ }\mathbb{E}_{\boldsymbol{0}}\left(\rho\right) = 0 \\ =& \text{ }\mathbb{E}_{B}\left(\llbracket \Omega \rrbracket_D(\rho)\right) + \llbracket \Omega \rrbracket_{R}(\rho) \\ =& \text{ }\mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^0 \rrbracket(\rho)\right) + \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^0 \rrbracket_{R}(\rho) \end{align}\]

  • \(n \to n+1\): Let \(wp_n\) be the form corresponding to \(wp\llbracket S' \rrbracket (A_n)\), \(b\) to \(B_\infty\) and \(a_{n}\) the form corresponding to \({A_n}_\infty\). Then \(\mathfrak{D}(a_{n+1}) = \{\psi \mid M_0 \psi \in \mathfrak{D}(b)\} \cap \{\psi \mid M_1 \psi \in \mathfrak{D}(wp_n)\}\). Let \(\rho = \sum_i p_i \ket{\psi_i}\bra{\psi_i}\) be a decomposition of \(\rho\) into pure states. We show the statement for each \(\ket{\psi_i}\bra{\psi_i}\), then we can conclude it for \(\rho\) by linearity of expectation values and the semantics (Proposition [prop:expectationProperties], Lemma 5 and Proposition [prop:semanticsProperties]). We distinguish two cases:

    1. Assume there is an \(i\) such that \(\ket{\psi_i} \not \in \mathfrak{D}(a_{n+1})\), then \(\mathbb{E}_{A_{n+1}}\left(\rho\right) = \infty\).

       If \(M_0 \ket{\psi_i} \not \in \mathfrak{D}(b)\), then \(\mathbb{E}_{B}\left(M_0 \ket{\psi_i}\bra{\psi_i} M_0^\dagger\right) = \infty\) and thus by linearity of expectation values and semantics (Proposition [prop:expectationProperties], Lemma 5, Proposition [prop:semanticsProperties]), we get \(\mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^{n+1} \rrbracket_D(\rho)\right) = \infty\), thus the sum with \(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^{n+1} \rrbracket_{R}(\rho)\) is \(\infty\) as well.

       If \(M_1 \ket{\psi_i} \not \in \mathfrak{D}(wp_n)\), then \[\begin{align} \infty &= \mathbb{E}_{wp\llbracket S' \rrbracket (A_n)}\left(\ket{M_1 \psi_i}\bra{M_1 \psi_i}\right) \\ & = \mathbb{E}_{A_n}\left(\llbracket S' \rrbracket_D(\ket{M_1 \psi_i}\bra{M_1 \psi_i})\right) \\ &= \mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\llbracket S' \rrbracket_D(\ket{M_1 \psi_i}\bra{M_1 \psi_i}))\right) \end{align}\] By linearity (Proposition [prop:expectationProperties], Lemma 5 and Proposition [prop:semanticsProperties]), we have
       \(\mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^{n+1} \rrbracket_D(\rho)\right) = \infty\) and thus the same for the addition with \(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^{n+1} \rrbracket_{R}(\rho)\).

    2. Assume \(\ket{\psi_i} \in \mathfrak{D}(a_{n+1})\) for all \(i\). \[\begin{align} \mathbb{E}_{A_{n+1}}\left(\ket{\psi_i}\bra{\psi_i}\right) =& \text{ } \mathbb{E}_{M_0^\dagger \odot B \odot M_0}\left(\ket{\psi_i}\bra{\psi_i}\right) + \mathbb{E}_{M_1^\dagger \odot wp\llbracket S' \rrbracket (A_n) \odot M_1}\left(\ket{\psi_i}\bra{\psi_i}\right) \\ =&\text{ } b[M_0 \ket{\psi_i}] + wp_n[M_1 \ket{\psi_i}] \\ =&\text{ } \mathbb{E}_{B}\left(\ket{M_0 \psi_i}\bra{M_0 \psi_i}\right) + \mathbb{E}_{wp\llbracket S' \rrbracket (A_n)}\left(\ket{M_1 \psi_i}\bra{M_1 \psi_i}\right) \\ =&\text{ } \mathbb{E}_{B}\left(\ket{M_0 \psi_i}\bra{M_0 \psi_i}\right) \\ &+ \mathbb{E}_{A_n}\left(\llbracket S' \rrbracket_D(\ket{M_1 \psi_i}\bra{M_1 \psi_i})\right) + \llbracket S' \rrbracket_{R}(\ket{M_1 \psi_i} \bra{M_1 \psi_i})\\ =&\text{ } \mathbb{E}_{B}\left(\ket{M_0 \psi_i}\bra{M_0 \psi_i}\right) \\ &+ \mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\llbracket S' \rrbracket_D(\ket{M_1 \psi_i}\bra{M_1 \psi_i}))\right) \\ &+ \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\llbracket S' \rrbracket_D(\ket{M_1 \psi_i}\bra{M_1 \psi_i})) \\ & + \llbracket S' \rrbracket_{R}(\ket{M_1 \psi_i} \bra{M_1 \psi_i}) \\ =&\text{ } \mathbb{E}_{B}\left(\llbracket \boldsymbol{skip} \rrbracket_D(\ket{M_0 \psi_i}\bra{M_0 \psi_i})\right) \\ &+ \mathbb{E}_{B}\left(\llbracket S'; \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\ket{M_1 \psi_i}\bra{M_1 \psi_i})\right) \\ &+ \llbracket \boldsymbol{skip} \rrbracket_{R}(\ket{M_0 \psi_i}\bra{M_0 \psi_i}) \\ &+ \llbracket S'; \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\ket{M_1 \psi_i}\bra{M_1 \psi_i}) \\ =&\text{ } \mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\ket{\psi_i}\bra{ \psi_i})\right) \\ &+ \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\ket{ \psi_i}\bra{ \psi_i}) \end{align}\]

    Now we can show that \(\{A_n\}_n\) is an increasing chain:

    • \(n=0\): \(A_0 = \boldsymbol{0}\sqsubseteq A_1\) and \(\mathfrak{D}(A_1) \subseteq \mathcal{H}=\mathfrak{D}(\boldsymbol{0})\)

    • \(n \to n+1\): \(A_{n+1} = M_0^\dagger \odot B \odot M_0 + M_1^\dagger \odot wp\llbracket S' \rrbracket (A_n) \odot M_1\) \[\begin{align} & \text{ }A_{n-1} \sqsubseteq A_n \\ \Rightarrow & \text{ }wp\llbracket S' \rrbracket (A_{n-1}) \sqsubseteq wp\llbracket S' \rrbracket (A_n) \\ \Rightarrow & \text{ } M_1^\dagger \odot wp\llbracket S' \rrbracket (A_{n-1}) \odot M_1 \sqsubseteq M_1^\dagger \odot wp\llbracket S' \rrbracket (A_n) \odot M_1 \\ \Rightarrow & \text{ } M_0^\dagger \odot B \odot M_0 + M_1^\dagger \odot wp\llbracket S' \rrbracket (A_{n-1}) \odot M_1\\ & \sqsubseteq M_0^\dagger \odot B \odot M_0 + M_1^\dagger \odot wp\llbracket S' \rrbracket (A_n) \odot M_1 \\ \Rightarrow & \text{ } A_n \sqsubseteq A_{n+1} \end{align}\]

    The first step holds by the monotonicity of \(wp\) (shown in Proposition [prop:wpProperties]). The next two steps hold by Proposition [prop:orderproperties]. Thus we have shown \(\bigvee_n A_n \in \mathcal{E}(\mathcal{H})\).

    Finally, we can conclude the second part of the proof based on the previous results: \[\begin{align} & \mathbb{E}_{wp\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B)}\left(\rho\right) \\ & = \mathbb{E}_{\bigvee_n A_n}\left(\rho\right)\\ &= \bigvee_n \mathbb{E}_{A_n}\left(\rho\right) \\ &\overset{Eq. \ref{align:expectAn}}{=} \bigvee_n [\mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\rho)]\\ & = \bigvee_n \mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\rho)\right) + \lim_n \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\rho)\\ &= \mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket_D(\rho)\right) + \llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket_{R}(\rho) \end{align}\] because both \(\mathbb{E}_{B}\left(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_D(\rho)\right)\) and \(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S^n \rrbracket_{R}(\rho)\) are increasing in \(n\).

 ◻

Proof.

• First of all note that if \(A \sqsubseteq\boldsymbol{I}\) is bounded, then \(\mathbb{E}_{A}\left(\rho\right) = tr(A\rho)\) for all partial density operators \(\rho \in \mathcal{D}(\mathcal{H})\) as \(\mathfrak{D}(A) = \mathcal{H}\) for bounded operators.

• Then the definition of total and partial correctness are exactly the same as in [8] for reward-free programs \(S\) as \(\llbracket S \rrbracket_{R}(\rho) = 0\) for all \(\rho\).

• The definition of weakest pre-expectation is also the same as in [1].

• Finally, the concrete representation of the weakest pre-expectation transformer \(wp\) differs only by the addition and multiplication but for bounded operators they coincide by Proposition [prop:BoundedAddition].

 ◻

Proof. As a technical result, we can show that the weakest pre-expectation of a loop is equivalent to the least upper bound of its characteristic function: Let \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S\) be a loop in qrWhile and \(B \in \mathcal{E}(\mathcal{H})\) be a post-expectation. Then \(wp\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B) = \bigvee_n \psi_B^n(0)\).

To show this equivalence, we show \(\psi_B^n(0) = A_n\) for all \(n\) where \(A_n\) is defined as in Table 1:

• \(n=0\): \(\psi_B^0(0) = 0 = A_0\)

• \(n \to n+1\):
  \[\begin{align} \psi_B^{n+1}(0) &= \psi_B(\psi_B^n(0)) \\ &= M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot wp\llbracket S \rrbracket (\psi_B^n(0)) \odot M_1 \\ &= M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot wp\llbracket S \rrbracket (A_n) \odot M_1 \\ &= A_{n+1} \end{align}\]

Now we continue by showing that \(\psi_B\) is monotone: Let \(A_1, A_2 \in \mathcal{E}(\mathcal{H})\) with \(A_1 \sqsubseteq A_2\), then \[\begin{align} A_1 &\sqsubseteq A_2 \\ \overset{Prop. \ref{prop:wpProperties}}{\Rightarrow} wp\llbracket S \rrbracket (A_1) &\sqsubseteq wp\llbracket S \rrbracket (A_2) \\ \overset{Prop. \ref{prop:orderproperties}}{\Rightarrow} M_1^\dagger \odot wp\llbracket S \rrbracket (A_1) \odot M_1 &\sqsubseteq M_1^\dagger \odot wp\llbracket S \rrbracket (A_2) \odot M_1 \\ \overset{Prop. \ref{prop:orderproperties}}{\Rightarrow} M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot wp\llbracket S \rrbracket (A_1) \odot M_1 &\sqsubseteq M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot wp\llbracket S \rrbracket (A_2) \odot M_1 \\ \Rightarrow \psi_B(A_1) &\sqsubseteq\psi_B(A_2) \end{align}\]

We can show that \(\psi_B(A)\sqsubseteq A\) implies \(\psi^n_B(0) \sqsubseteq A\) for all \(n\in \mathbb{N}\) by induction over \(n\):

• \(n=0\): \(\psi^0_B(0) = 0 \sqsubseteq A\) as \(A\) is positive.

• \(n \to n+1\): \[\begin{align} \psi_B(A) &\sqsubseteq A \\ \overset{IH}{\Rightarrow} \psi^n_B(0) &\sqsubseteq A \\ \Rightarrow \psi_B(\psi^n_B(0)) &\sqsubseteq\psi_B(A) \\ \Rightarrow \psi^{n+1}_B(0) &\sqsubseteq\psi_B(A) \\ \Rightarrow \psi^{n+1}_B(0) &\sqsubseteq A \end{align}\] where the second step holds by monotonicity of \(\psi_B\) and the last step holds by the assumption \(\psi_B(A) \sqsubseteq A\) and the transitivity of \(\sqsubseteq\) (Proposition [prop:orderproperties]).

Finally, we can show that whole statement: \[\begin{align} \psi_B(A)\sqsubseteq A &\Rightarrow \forall n\in \mathbb{N}: \psi^n_B(0) \sqsubseteq A \\ & \Rightarrow \bigvee_n \psi^n_B(0) \sqsubseteq A \\ & \Rightarrow wp\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B) \sqsubseteq A \end{align}\] where the first step holds by the above induction, the second one by the definition of \(\bigvee\) and the last one by the technical result at the beginning of the proof. ◻

Proof.

• \(\forall \rho \in \mathcal{D}(\mathcal{H})\) is \(\llbracket S \rrbracket_{R}(\rho) = 0\), thus \[\begin{align} tr(\llbracket S \rrbracket_D(\rho)) = tr(\boldsymbol{I}\llbracket S \rrbracket_D(\rho)) = tr(wp\llbracket S \rrbracket (\boldsymbol{I}) \rho) = tr(\boldsymbol{I}\rho) = tr(\rho). \end{align}\]

• \(\mathfrak{D}(wp\llbracket T({S}) \rrbracket (\boldsymbol{0})) = \mathcal{H}\) means that \(\mathbb{E}_{wp\llbracket T({S}) \rrbracket (\boldsymbol{0})}\left(\rho\right) < \infty\) for all \(\rho \in \mathcal{D}(\mathcal{H})\), thus it is \(\llbracket T({S}) \rrbracket_{R}(\rho) < \infty\) for all \(\rho \in \mathcal{D}(\mathcal{H})\) and thus \(S\) is PAST. Conversely, if \(S\) is PAST, then \(\llbracket T({S}) \rrbracket_{R}(\rho) < \infty\) for all \(\rho \in \mathcal{D}(\mathcal{H})\), thus \(\mathbb{E}_{wp\llbracket T({S}) \rrbracket (\boldsymbol{0})}\left(\rho\right) < \infty\) for all \(\rho \in \mathcal{D}(\mathcal{H})\) and thus \(\mathfrak{D}(wp\llbracket T({S}) \rrbracket (\boldsymbol{0})) = \mathcal{H}\).

 ◻

Proof. Let \(S\) be a reward-free qrWhile program, \(A,B \in \mathcal{E}(\mathcal{H})\) and \(c\geq 0\).

1. Well-definedness & Connection to wp & Monotonicity: We show this together by induction over the structure of \(S\). The connection to wp is shown by induction over the structure of \(S\) as well, and monotonicity follows immediately from the connection to wp and the monotonicity of wp: Let \(A \sqsubseteq B\). We show \(ert\llbracket S \rrbracket (A) \sqsubseteq ert\llbracket S \rrbracket (B)\) based on 2. and the monotonicity of wp (Proposition [prop:wpProperties]): \[\begin{align} &ert\llbracket S \rrbracket (A) \\ &\overset{2.}{=} wp\llbracket S \rrbracket (A) \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \\ &\sqsubseteq wp\llbracket S \rrbracket (B) \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \\ &\overset{2.}{=} ert\llbracket S \rrbracket (B) \end{align}\] Induction over the structure of \(S\):

   • \(S = \boldsymbol{skip}\): Clearly \(ert\llbracket \boldsymbol{skip} \rrbracket (A) \in \mathcal{E}(\mathcal{H})\). \[\begin{align} ert\llbracket \boldsymbol{skip} \rrbracket (A) = A = A + \boldsymbol{0}= wp\llbracket \boldsymbol{skip} \rrbracket (A) \oplus ert\llbracket \boldsymbol{skip} \rrbracket (\boldsymbol{0}) \end{align}\]

   • \(S = q:=0\): It is \(ert\llbracket q:=0 \rrbracket (A) \in \mathcal{E}(\mathcal{H})\) by Definition 5 as \(\ket{n}\bra{0}\) are bounded operators. The sum is infinite and by Lemma 1 in \(\mathcal{E}(\mathcal{H})\). \[\begin{align} &ert\llbracket q:=0 \rrbracket (A) \\ &= \boldsymbol{I}\oplus\sum_{n=0}^\infty \ket{n}\bra{0} \odot A \odot \ket{0}\bra{n} \\ &= \boldsymbol{I}\oplus wp\llbracket q:=0 \rrbracket (A) \\ &= wp\llbracket q:=0 \rrbracket (A) \oplus ert\llbracket q:=0 \rrbracket (\boldsymbol{0}) \end{align}\]

   • \(S = \overline{q}:= U\overline{q}\): It is \(ert\llbracket \overline{q}:= U\overline{q} \rrbracket (A) \in \mathcal{E}(\mathcal{H})\) as \(\mathcal{E}(\mathcal{H})\) is closed under \(\oplus\) and bounded-operator application. \[\begin{align} ert\llbracket \overline{q}:= U\overline{q} \rrbracket (A) = U^\dagger \odot A \odot U \oplus\boldsymbol{I}= wp\llbracket \overline{q}:= U\overline{q} \rrbracket (A) \oplus ert\llbracket \overline{q}:= U\overline{q} \rrbracket (\boldsymbol{0}) \end{align}\]

   • \(S = S_1;S_2\): It is \(ert\llbracket S_1;S_2 \rrbracket (A)\in \mathcal{E}(\mathcal{H})\) by induction hypothesis. \[\begin{align} ert\llbracket S_1;S_2 \rrbracket (A) &= ert\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (A)) \\ &\overset{IH}{=} ert\llbracket S_1 \rrbracket (wp\llbracket S_2 \rrbracket (A) \oplus ert\llbracket S_2 \rrbracket (\boldsymbol{0})) \\ &\overset{IH}{=} wp\llbracket S_1 \rrbracket (wp\llbracket S_2 \rrbracket (A) \oplus ert\llbracket S_2 \rrbracket (\boldsymbol{0})) \oplus ert\llbracket S_1 \rrbracket (\boldsymbol{0}) \\ &= wp\llbracket S_1 \rrbracket (wp\llbracket S_2 \rrbracket (A)) \oplus wp\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (\boldsymbol{0})) \oplus ert\llbracket S_1 \rrbracket (\boldsymbol{0}) \\ &\overset{IH}{=}wp\llbracket S_1 \rrbracket (wp\llbracket S_2 \rrbracket (A)) \oplus ert\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (\boldsymbol{0}))\\ &= wp\llbracket S_1;S_2 \rrbracket (A) \oplus ert\llbracket S_1;S_2 \rrbracket (\boldsymbol{0}) \end{align}\]

   • \(S = \boldsymbol{measure } M[\overline{q}]:\overline{S'}\):

     To show \(ert\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (A) \in \mathcal{E}(\mathcal{H})\): It is \(M_m^\dagger \odot ert\llbracket S_m' \rrbracket (A) \odot M_m \in \mathcal{E}(\mathcal{H})\) for all \(m\) as \(\mathcal{E}(\mathcal{H})\) is closed under bounded-operator application and \(ert\llbracket S_m' \rrbracket (A) \in \mathcal{E}(\mathcal{H})\) by induction hypothesis. The sum is infinite and in \(\mathcal{E}(\mathcal{H})\) by Lemma 1. Adding \(\boldsymbol{I}\) is also fine as \(\mathcal{E}(\mathcal{H})\) is closed under \(\oplus\). \[\begin{align} &ert\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (A) \\ &= \boldsymbol{I}\oplus\left(\sum_{m} M_m^\dagger \odot ert\llbracket S_m' \rrbracket (A) \odot M_m \right) \\ &\overset{IH}{=} \boldsymbol{I}\oplus\left(\sum_{m} M_m^\dagger \odot \left(wp\llbracket S_m' \rrbracket (A) \oplus ert\llbracket S_m' \rrbracket (\boldsymbol{0})\right) \odot M_m \right) \\ &= \boldsymbol{I}\oplus\left(\sum_{m} M_m^\dagger \odot wp\llbracket S_m' \rrbracket (A) \odot M_m \right) \oplus\left(\sum_{m} M_m^\dagger \odot ert\llbracket S_m' \rrbracket (\boldsymbol{0}) \odot M_m \right) \\ &= wp\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (A) \oplus ert\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (\boldsymbol{0}) \end{align}\] Distributivity for infinite sums holds by Lemma 2 (and for finite ones by Proposition [prop:ContinuityDistributivityFormSum]).

   • \(S = \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'\): We consider three different chains: \[\begin{align} ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (A) &= \bigvee_n F_n \quad \text{where }\\ F_0 &= \boldsymbol{0},\\ F_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_n) \odot M_1 \oplus\boldsymbol{I}\\ ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (\boldsymbol{0}) &= \bigvee_n G_n \quad \text{where }\\ G_0 &= \boldsymbol{0},\\ G_{n+1} &= M_0^\dagger \odot \boldsymbol{0} \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (G_n) \odot M_1 \oplus\boldsymbol{I}\\ &= M_1^\dagger \odot ert\llbracket S' \rrbracket (G_n) \odot M_1 \oplus\boldsymbol{I}\\ wp\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (A) &= \bigvee_n H_n \quad \text{where }\\ H_0 &= \boldsymbol{0},\\ H_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot wp\llbracket S' \rrbracket (H_n) \odot M_1 \end{align}\] First of all, each \(F_n\in \mathcal{E}(\mathcal{H})\) by induction over \(n\) as \(\mathcal{E}(\mathcal{H})\) is closed under \(\oplus\) and \(M^\dagger \odot \cdot \odot M\) for any \(M\). We can also show that \(F_n\) is increasing in \(n\) by induction over \(n\) as well:

     • \(n=0\): \(F_0 = \boldsymbol{0}\sqsubseteq F_1\).

     • \(n \to n+1\): \[\begin{align} F_{n} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_{n-1}) \odot M_1 \oplus\boldsymbol{I}\\ &\sqsubseteq M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_{n}) \odot M_1 \oplus\boldsymbol{I}= F_{n+1} \end{align}\] by Proposition [prop:orderproperties] and because \(ert\llbracket S' \rrbracket (F_{n-1}) \sqsubseteq ert\llbracket S' \rrbracket (F_{n})\) holds by the monotonicity of \(ert\llbracket S' \rrbracket (\cdot)\) which follows by induction hypothesis.

     Thus \(F_n\) is an increasing sequence in \(n\) and thus \(\bigvee_n F_n\) is well-defined. (Analogously, we can show the same for \(G_n\) and \(H_n\).)

     We show by induction over \(n\) that \(F_n = H_n \oplus G_n\) for all \(n\):

     • \(n=0\): \(F_0 = \boldsymbol{0}= H_0 \oplus G_0\).

     • \(n \to n+1\): \[\begin{align} F_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_n) \odot M_1 \oplus\boldsymbol{I}\\ &\overset{IH}{=} M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (H_n \oplus G_n) \odot M_1 \oplus\boldsymbol{I}\\ &\overset{IH}{=} M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot \left(wp\llbracket S' \rrbracket (H_n \oplus G_n) \oplus ert\llbracket S' \rrbracket (\boldsymbol{0})\right) \odot M_1 \oplus\boldsymbol{I}\\ &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot \left(wp\llbracket S' \rrbracket (H_n) \oplus wp\llbracket S' \rrbracket (G_n) \oplus ert\llbracket S' \rrbracket (\boldsymbol{0})\right) \odot M_1 \oplus\boldsymbol{I}\\ &\overset{IH}{=} M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot \left(wp\llbracket S' \rrbracket (H_n) \oplus ert\llbracket S' \rrbracket (G_n)\right) \odot M_1 \oplus\boldsymbol{I}\\ &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot wp\llbracket S' \rrbracket (H_n) \odot M_1 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (G_n) \odot M_1 \oplus\boldsymbol{I}\\ &= H_{n+1} \oplus G_{n+1} \end{align}\]

     Thus we have \(F_n = H_n \oplus G_n\) for all \(n\). Finally, we can show the connection to wp: \[\begin{align} &ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (A) = \bigvee_n F_n \\ =& \bigvee_n (H_n \oplus G_n) = \bigvee_n H_n \oplus\bigvee_n G_n \\ =& \text{ }wp\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (A) \oplus ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (\boldsymbol{0}) \end{align}\]

2. Continuity: Let \(\{A_i\}_i\) be an increasing chain of expectations. We show \(ert\llbracket S \rrbracket (\bigvee_i A_i) = \bigvee_i ert\llbracket S \rrbracket (A_i)\): \[\begin{align} &\text{ } ert\llbracket S \rrbracket (\bigvee_i A_i)\\ =& \text{ }wp\llbracket S \rrbracket (\bigvee_i A_i) \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \\ =& \bigvee_i wp\llbracket S \rrbracket (A_i) \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \\ =& \bigvee_i \left(wp\llbracket S \rrbracket (A_i) \oplus ert\llbracket S \rrbracket (\boldsymbol{0})\right) \\ =& \bigvee_i ert\llbracket S \rrbracket (A_i) \end{align}\] where the first step holds by 2., the second one by the continuity of \(wp\llbracket S \rrbracket (\cdot)\) (Proposition [prop:wpProperties]) and the third one by the continuity of \(\oplus\) (Proposition [prop:ContinuityDistributivityFormSum]).

3. Constant propagation: We show \(ert\llbracket S \rrbracket (c\cdot A) = c\cdot A \oplus ert\llbracket S \rrbracket (\boldsymbol{0})\) \[\begin{align} &ert\llbracket S \rrbracket (c\cdot A) \\ &\overset{2.}{=} wp\llbracket S \rrbracket (c\cdot A) \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \\ &= c\cdot wp\llbracket S \rrbracket (A) \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \\ &\overset{2.}{=} c\cdot A \oplus ert\llbracket S \rrbracket (\boldsymbol{0}) \end{align}\] where the second step holds as wp is linear by Proposition [prop:wpProperties].

4. Preservation of infinity: It is \(ert\llbracket S \rrbracket (\boldsymbol{\infty}) = \boldsymbol{\infty}\) because \(M^\dagger \odot \boldsymbol{\infty} \odot M = \boldsymbol{\infty}\) for any (linear bounded) \(M\neq \boldsymbol{0}\), \(\boldsymbol{\infty}\oplus A = \boldsymbol{\infty}\) for any (linear) \(A\) and \(\bigvee \boldsymbol{\infty}= \boldsymbol{\infty}\), thus it follows by induction over the structure of \(S\) that \(ert\llbracket S \rrbracket (\boldsymbol{\infty}) = \boldsymbol{\infty}\).

 ◻

Proof. We show the statement by induction over the structure of \(S\):

• \(S = \boldsymbol{skip}\): \[\begin{align} ert\llbracket \boldsymbol{skip} \rrbracket (A) = A = wp\llbracket \boldsymbol{skip} \rrbracket (A) = wp\llbracket T({\boldsymbol{skip}}) \rrbracket (A) \end{align}\]

• \(S = q:=0\): \[\begin{align} &\text{ }ert\llbracket q:=0 \rrbracket (A) \\ =& \text{ }\boldsymbol{I}\oplus\sum_{n=0}^\infty \ket{n}\bra{0} \odot A \odot \ket{0}\bra{n} \\ =& \text{ }\boldsymbol{I}\oplus wp\llbracket q:=0 \rrbracket (A) \\ =& \text{ }wp\llbracket \boldsymbol{reward} (1) \rrbracket (wp\llbracket q:=0 \rrbracket (A))\\ =& \text{ }wp\llbracket \boldsymbol{reward} (1); q:=0 \rrbracket (A)\\ =& \text{ }wp\llbracket T({q:=0}) \rrbracket (A) \end{align}\]

• \(S = \overline{q}:= U\overline{q}\): \[\begin{align} &\text{ } ert\llbracket \overline{q}:= U\overline{q} \rrbracket (A) = \boldsymbol{I}\oplus U^\dagger \odot A \odot U \\ =& \text{ }\boldsymbol{I}\oplus wp\llbracket \overline{q}:= U\overline{q} \rrbracket (A) = wp\llbracket \boldsymbol{reward} (1) \rrbracket (wp\llbracket \overline{q}:= U\overline{q} \rrbracket (A)) \\ =& \text{ }wp\llbracket T({\overline{q}:= U\overline{q}}) \rrbracket (A) \end{align}\]

• \(S = S_1;S_2\): \[\begin{align} &ert\llbracket S_1;S_2 \rrbracket (A) = ert\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (A)) \\ \overset{IH}{=} &wp\llbracket T({S_1}) \rrbracket (wp\llbracket T({S_2}) \rrbracket (A)) = wp\llbracket T({S_1;S_2}) \rrbracket (A) \end{align}\]

• \(S = \boldsymbol{measure } M[\overline{q}]:\overline{S'}\): \[\begin{align} &\text{ }ert\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (A) \\ =& \text{ }\boldsymbol{I}\oplus\left(\sum_{m} M_m^\dagger \odot ert\llbracket S_m' \rrbracket (A) \odot M_m \right) \\ \overset{IH}{=} &\boldsymbol{I}\oplus\left(\sum_{m} M_m^\dagger \odot wp\llbracket T({S_m'}) \rrbracket (A) \odot M_m \right) \\ =& \text{ }\boldsymbol{I}\oplus wp\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (A) \\ =& \text{ }wp\llbracket \boldsymbol{reward} (1) \rrbracket (wp\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (A)) \\ =& \text{ }wp\llbracket T({\boldsymbol{measure } M[\overline{q}]:\overline{S'}}) \rrbracket (A) \end{align}\]

• \(S = \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'\): For this case, we need an auxiliary result:

  Lemma 10. Let \(S\) be a reward-free qrWhile program and \(A \in \mathcal{E}(\mathcal{H})\). Then \(ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (A) = \bigvee F'_n\) where \[\begin{align} F'_0 &= \boldsymbol{I}\\ F'_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S \rrbracket (F'_n) \odot M_1 \oplus\boldsymbol{I}. \end{align}\]

  Proof. We have to show that \(\bigvee F'_n\) and \(\bigvee F_n\) are equal where \(F_n\) is defined as in Table 3 for \(\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'\), i.e. \[\begin{align} F_0 &= \boldsymbol{0}\\ F_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_n) \odot M_1 \oplus\boldsymbol{I} \end{align}\] The only difference is the definition of \(F_0\).

  Clearly \(F'_n\) is an increasing sequence as well, so we show by induction over \(n\) that \(F'_n \sqsubseteq F_{n+1}\) and \(F_n \sqsubseteq F'_{n}\) using the induction hypothesis, monotonicity of \(ert\llbracket S' \rrbracket (\cdot)\) and Proposition [prop:orderproperties]. This implies \(\bigvee_n F'_n = \bigvee_n F_n\).

  • \(F'_n \sqsubseteq F_{n+1}\): \[\begin{align} F'_0 =& \text{ }\boldsymbol{I}\sqsubseteq\boldsymbol{I}\oplus M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (\boldsymbol{0}) \odot M_1 = F_1\\ F'_{n+1} =& \text{ }M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F'_n) \odot M_1 \oplus\boldsymbol{I}\\ \sqsubseteq& \text{ }M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_{n+1}) \odot M_1 \oplus\boldsymbol{I}= F_{n+2} \end{align}\]

  • \(F_n \sqsubseteq F'_{n}\) \[\begin{align} F_0 = &\text{ } \boldsymbol{0}\sqsubseteq\boldsymbol{I}= F'_0\\ F_{n+1} =& \text{ }M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_n) \odot M_1 \oplus\boldsymbol{I}\\ \sqsubseteq& \text{ }M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F'_n) \odot M_1 \oplus\boldsymbol{I}= F'_{n+1} \qedhere \end{align}\]

   ◻

  Using the auxiliary result, we can now show the statement for the while case. Recall that \(wp\llbracket T({\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'}) \rrbracket (A) = \bigvee A_n\) where \[\begin{align} A_0 &= \boldsymbol{0},\\ A_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot wp\llbracket T({S'});\boldsymbol{reward} (1) \rrbracket (A_n) \odot M_1 \end{align}\] We show by induction over \(n\) that \(F'_n = A_n \oplus\boldsymbol{I}\) for all \(n\) which implies \(\bigvee_n F'_n = \boldsymbol{I}\oplus\bigvee_n A_n\).

  • \(n = 0\): \[\begin{align} F'_0 &= \boldsymbol{I}\\ A_0 &= \boldsymbol{0}\\ F'_0 &= A_0 \oplus\boldsymbol{I} \end{align}\]

  • \(n \to n+1\): \[\begin{align} F'_{n+1} &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F'_n) \odot M_1 \oplus\boldsymbol{I}\\ &\overset{IH}{=} M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (A_n \oplus\boldsymbol{I}) \odot M_1 \oplus\boldsymbol{I}\\ &\overset{IH}{=} M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot wp\llbracket T({S'}) \rrbracket (A_n \oplus\boldsymbol{I}) \odot M_1 \oplus\boldsymbol{I}\\ &= M_0^\dagger \odot A \odot M_0 \oplus M_1^\dagger \odot wp\llbracket T({S'});\boldsymbol{reward} (1) \rrbracket (A_n) \odot M_1 \oplus\boldsymbol{I}\\ &= A_{n+1} \oplus\boldsymbol{I}\qedhere \end{align}\]

 ◻

Proof. We show this by induction:

• \(S = \boldsymbol{skip}\): \(\mathbb{E}_{ert\llbracket \boldsymbol{skip} \rrbracket (\boldsymbol{0})}\left(\rho\right) = \mathbb{E}_{\boldsymbol{0}}\left(\rho\right) = 0 = ERT\llbracket \boldsymbol{skip} \rrbracket (\rho)\).

• \(S = q:=0\): \[\begin{align} \text{ }\mathbb{E}_{ert\llbracket q:=0 \rrbracket (\boldsymbol{0})}\left(\rho\right) =& \text{ }\mathbb{E}_{\boldsymbol{I}\oplus\sum_{n=0}^\infty \ket{n}\bra{0} \odot \boldsymbol{0}\odot \ket{0}\bra{n}}\left(\rho\right) \\ =& \text{ }\mathbb{E}_{\boldsymbol{I}}\left(\rho\right) + \mathbb{E}_{\sum_{n=0}^\infty \ket{n}\bra{0} \odot \boldsymbol{0}\odot \ket{0}\bra{n}}\left(\rho\right) \\ =& \text{ }tr(\rho) + \mathbb{E}_{\boldsymbol{0}}\left(\rho\right) = tr(\rho) = ERT\llbracket q:=0 \rrbracket (\rho) \end{align}\]

• \(S = \overline{q}:= U\overline{q}\): \(\mathbb{E}_{ert\llbracket \overline{q}:= U\overline{q} \rrbracket (\boldsymbol{0})}\left(\rho\right) = \mathbb{E}_{U^\dagger \odot \boldsymbol{0} \odot U \oplus\boldsymbol{I}}\left(\rho\right) = \mathbb{E}_{\boldsymbol{I}}\left(\rho\right)= tr(\rho) = ERT\llbracket \overline{q}:= U\overline{q} \rrbracket (\rho)\).

• \(S = S_1;S_2\): We use the connection to \(wp\) (Proposition [prop:ERTProperties]) \[\begin{align} \mathbb{E}_{ert\llbracket S_1;S_2 \rrbracket (\boldsymbol{0})}\left(\rho\right) =&\text{ }\mathbb{E}_{ert\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (\boldsymbol{0}))}\left(\rho\right) \\ =& \text{ }\mathbb{E}_{wp\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (\boldsymbol{0})) \oplus ert\llbracket S_1 \rrbracket (\boldsymbol{0})}\left(\rho\right) \\ =& \text{ }\mathbb{E}_{wp\llbracket S_1 \rrbracket (ert\llbracket S_2 \rrbracket (\boldsymbol{0}))}\left(\rho\right) + \mathbb{E}_{ert\llbracket S_1 \rrbracket (\boldsymbol{0})}\left(\rho\right) \\ =& \text{ }\mathbb{E}_{ert\llbracket S_2 \rrbracket (\boldsymbol{0})}\left(\llbracket S_1 \rrbracket(\rho)\right) + \mathbb{E}_{ert\llbracket S_1 \rrbracket (\boldsymbol{0})}\left(\rho\right) \\ =& \text{ }ERT\llbracket S_2 \rrbracket (\llbracket S_1 \rrbracket(\rho)) + ERT\llbracket S_1 \rrbracket (\rho) \\ =& \text{ }ERT\llbracket S_1;S_2 \rrbracket (\rho) \end{align}\]

• \(S = \boldsymbol{measure } M[\overline{q}]:\overline{S'}\): \[\begin{align} &\text{ }\mathbb{E}_{ert\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (\boldsymbol{0})}\left(\rho\right)\\ = &\text{ }\mathbb{E}_{\boldsymbol{I}\oplus\left(\sum_{m} M_m^\dagger \odot ert\llbracket S_m' \rrbracket (\boldsymbol{0}) \odot M_m \right)}\left(\rho\right) \\ =& \text{ }\mathbb{E}_{\boldsymbol{I}}\left(\rho\right) + \mathbb{E}_{\sum_{m} M_m^\dagger \odot ert\llbracket S_m' \rrbracket (\boldsymbol{0}) \odot M_m}\left(\rho\right) \\ =& \text{ }tr(\rho) + \sum_{m} \mathbb{E}_{M_m^\dagger \odot ert\llbracket S_m' \rrbracket (\boldsymbol{0}) \odot M_m}\left(\rho\right) \\ =& \text{ }tr(\rho) + \sum_{m} \mathbb{E}_{ert\llbracket S_m' \rrbracket (\boldsymbol{0})}\left(M_m{\rho} M_m^\dagger\right) \\ =& \text{ }tr(\rho) + \sum_{m} ERT\llbracket S_m' \rrbracket (M_m \rho M_m^\dagger) \\ =& \text{ }ERT\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket (\rho) \end{align}\]

• \(S= \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'\): We show \(\mathbb{E}_{F_n}\left(\rho\right) = ERT\llbracket while^{[n]} \rrbracket (\rho)\) \[\begin{align} \mathbb{E}_{F_0}\left(\rho\right) =& \text{ }\mathbb{E}_{\boldsymbol{0}}\left(\rho\right) = 0 = ERT\llbracket while^{[0]} \rrbracket (\rho) \\ \mathbb{E}_{F_{n+1}}\left(\rho\right) =&\text{ } \mathbb{E}_{M_0^\dagger \odot \boldsymbol{0} \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S' \rrbracket (F_n) \odot M_1 \oplus\boldsymbol{I}}\left(\rho\right) \\ =& \text{ } \mathbb{E}_{\boldsymbol{0}}\left(\rho\right) + \mathbb{E}_{M_1^\dagger \odot ert\llbracket S' \rrbracket (F_n) \odot M_1}\left(\rho\right) + \mathbb{E}_{\boldsymbol{I}}\left(\rho\right) \\ =& \text{ } 0 + \mathbb{E}_{ert\llbracket S' \rrbracket (F_n)}\left(M_1 \rho M_1^\dagger\right) + tr(\rho) \\ =& \text{ }\mathbb{E}_{wp\llbracket S' \rrbracket (F_n) + ert\llbracket S' \rrbracket (\boldsymbol{0}) }\left(M_1 \rho M_1^\dagger\right) + tr(\rho) \\ =& \text{ }\mathbb{E}_{wp\llbracket S' \rrbracket (F_n)}\left(M_1 \rho M_1^\dagger\right) + \mathbb{E}_{ert\llbracket S' \rrbracket (\boldsymbol{0})}\left(M_1 \rho M_1^\dagger\right) + tr(\rho) \\ =& \text{ }\mathbb{E}_{F_n}\left(\llbracket S' \rrbracket(M_1 \rho M_1^\dagger)\right) + \mathbb{E}_{ert\llbracket S' \rrbracket (\boldsymbol{0})}\left(M_1 \rho M_1^\dagger\right) + tr(\rho) \\ =& \text{ }0 + ERT\llbracket while^{[n]} \rrbracket (\llbracket S' \rrbracket(M_1 \rho M_1^\dagger)) + ERT\llbracket S' \rrbracket (M_1 \rho M_1^\dagger) + tr(\rho) \\ =& \text{ }ERT\llbracket \boldsymbol{skip} \rrbracket (M_0 \rho M_0^\dagger) + ERT\llbracket S';while^{[n]} \rrbracket (M_1 \rho M_1^\dagger) + tr(\rho)\\ =& \text{ }ERT\llbracket while^{[n+1]} \rrbracket (\rho) \end{align}\] Then \[\begin{align} &\text{ } \mathbb{E}_{ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (\boldsymbol{0})}\left(\rho\right) \\ =& \text{ }\mathbb{E}_{\bigvee_n F_n}\left(\rho\right) = \sup_n \mathbb{E}_{F_n}\left(\rho\right) \\ =& \sup_n ERT\llbracket while^{[n]} \rrbracket (\rho) \\ =& \lim_n ERT\llbracket while^{[n]} \rrbracket (\rho) \\ =& \text{ } ERT\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (\rho) \end{align}\] where supremum and limit coincide since we have increasing sequences.

 ◻

Proof. Let \(S\) be reward-free and \(\rho \in \mathcal{D}(\mathcal{H})\). Assume \(S\) is PAST on \(\rho\), that means \(\llbracket T({S}) \rrbracket_{R}(\rho) < \infty\) by definition. We show by induction that \(tr(\llbracket S \rrbracket_D(\rho)) = tr(\rho)\), that means \(S\) is AST on \(\rho\).

• \(S = \boldsymbol{skip}\): \(tr(\llbracket \boldsymbol{skip} \rrbracket_D(\rho)) = tr(\rho)\) by definition.

• \(S = q:=0\): \[\begin{align} &tr(\llbracket q:=0 \rrbracket_D(\rho)) = tr(\sum_n \ket{0}\bra{n} \rho \ket{n}\bra{0}) \\ =& \sum_n tr( \ket{n}\bra{0} \ket{0}\bra{n} \rho ) = tr(\sum_n \ket{n}\bra{n} \rho ) = tr(\rho). \end{align}\]

• \(S = \overline{q}:= U\overline{q}\): \(tr(\llbracket \overline{q}:= U\overline{q} \rrbracket_D(\rho)) = tr(U \rho U^\dagger) =tr(U^\dagger U \rho )= tr(\rho)\) as \(U\) is unitary.

• \(S = S_1;S_2\): By \(\llbracket T({S_1;S_2}) \rrbracket_{R}(\rho) = \llbracket T({S_1}) \rrbracket_{R}(\rho) + \llbracket T({S_2}) \rrbracket_{R}(\llbracket S_1 \rrbracket_D(\rho)) < \infty\), we have \[\begin{align} \llbracket T({S_1}) \rrbracket_{R}(\rho) < \infty \quad \text{and} \quad \llbracket T({S_2}) \rrbracket_{R}(\llbracket S_1 \rrbracket_D(\rho)) < \infty. \end{align}\] Thus \(tr(\llbracket S_1 \rrbracket_D(\rho)) = tr(\rho)\) and \(tr(\llbracket S_2 \rrbracket_D(\llbracket S_1 \rrbracket_D(\rho))) = tr(\llbracket S_1 \rrbracket_D(\rho))\) by induction hypothesis. Overall it is \(tr(\llbracket S_1;S_2 \rrbracket_D(\rho)) = tr(\llbracket S_2 \rrbracket_D(\llbracket S_1 \rrbracket_D(\rho))) = tr(\llbracket S_1 \rrbracket_D(\rho)) = tr(\rho)\).

• \(S = \boldsymbol{measure } M[\overline{q}]:\overline{S'}\): It is \(\llbracket T({\boldsymbol{measure } M[\overline{q}]:\overline{S'}}) \rrbracket_{R}(\rho) = \sum_m \llbracket T({S_m'}) \rrbracket_{R}(M_m \rho M_m^\dagger) < \infty\), thus \(\llbracket T({S_m'}) \rrbracket_{R}(M_m \rho M_m^\dagger) < \infty\) for all \(m\). Then \(tr(\llbracket S_m' \rrbracket_D(M_m \rho M_m^\dagger)) = tr(M_m \rho M_m^\dagger)\) for all \(m\) by induction hypothesis. Overall it is \[\begin{align} tr(\llbracket \boldsymbol{measure } M[\overline{q}]:\overline{S'} \rrbracket_D(\rho)) &= tr(\sum_m \llbracket S_m' \rrbracket_D(M_m \rho M_m^\dagger)) \\ &= \sum_m tr(\llbracket S_m' \rrbracket_D(M_m \rho M_m^\dagger)) \\ &\overset{IH}{=} \sum_m tr(M_m \rho M_m^\dagger) \\ &= tr(\sum_m M_m^\dagger M_m \rho) \\ &= tr(\rho) \end{align}\]

• \(S = \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S'\): By \(ERT\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (\rho)< \infty\), we have \[\begin{align} \forall n:&\text{ } ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n]} \rrbracket (\rho)\\ \leq &\lim_{n \to \infty} ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n]} \rrbracket (\rho) \\ = & \text{ } ERT\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket (\rho) < \infty \end{align}\] and thus by induction hypothesis, it is \(tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n]} \rrbracket_D (\rho)) = tr(\rho)\) for all \(n\).

  We define \(\sigma_0 = \rho\) and \(\sigma_{n+1} = \llbracket S' \rrbracket_D(M_1 \sigma_n M_1^\dagger)\) for all \(n\). Intuitively, \(\sigma_n\) is the state entering the \(n\)-th iteration of the loop. We have \[\begin{align} \infty > & \text{ }ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n]} \rrbracket (\rho) \\ = & \text{ } tr(\rho) + ERT\llbracket \boldsymbol{skip} \rrbracket (M_0 \rho M_0^\dagger) + ERT\llbracket S'; (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n-1]} \rrbracket (M_1 \rho M_1^\dagger) \\ =& \text{ }tr(\rho) + ERT\llbracket S' \rrbracket (M_1 \rho M_1^\dagger) + ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n-1]} \rrbracket (\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger))\\ \geq & \text{ }tr(\sigma_0) + ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n-1]} \rrbracket (\sigma_1)\\ \geq &\text{ } tr(\sigma_0) + tr(\sigma_1) + ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[n-2]} \rrbracket (\sigma_2) \\ \geq & \dots \\ \geq & \text{ } tr(\sigma_0) + tr(\sigma_1) + \ldots + ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[1]} \rrbracket (\sigma_{n-1}) \geq \sum_{i=0}^{{n-1}} tr(\sigma_i) \end{align}\] Since \(\sum_{i=0}^{n} tr(\sigma_i) < \infty\) for all \(n\), \(\lim_{n \to \infty} tr(\sigma_n) = 0\).

  From the equation above we get \(ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[1]} \rrbracket (\sigma_n) < \infty\) for all \(n\), thus \[\begin{align} \infty > & \text{ }ERT\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{[1]} \rrbracket (\sigma_n) \\ =& \text{ }tr(\sigma_n) + ERT\llbracket S'; \boldsymbol{skip} \rrbracket (M_1 \sigma_n M_1^\dagger) + ERT\llbracket \boldsymbol{skip} \rrbracket (M_0 \sigma_n M_0^\dagger) \\ \geq &\text{ } ERT\llbracket S' \rrbracket (M_1 \sigma_n M_1^\dagger) \end{align}\] That means \(S'\) is PAST on \(M_1 \sigma_n M_1^\dagger\) for all \(n\). By induction hypothesis for \(S'\), we have \(tr(\llbracket S' \rrbracket_D(M_1 \sigma_n M_1^\dagger)) = tr(M_1 \sigma_n M_1^\dagger)\) for all \(n\).

  Then we show that \(tr(\rho) - tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D (\rho)) = tr(\sigma_n)\) by induction over \(n\):

  • \(n=0\): \(tr(\rho) - tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{0} \rrbracket_D (\rho)) = tr(\rho) - tr(0) = tr(\rho) = tr(\sigma_0)\)

  • \(n \to n+1\): It is \[\begin{align} &\text{ } tr(\rho) - tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n+1} \rrbracket_D (\rho)) \\ = & \text{ } tr(\rho) - tr(\llbracket \boldsymbol{skip} \rrbracket_D(M_0 \rho M_0^\dagger) + \llbracket S'; (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D(M_1 \rho M_1^\dagger)) \\ = & \text{ } tr(\rho) - tr(\llbracket \boldsymbol{skip} \rrbracket_D(M_0 \rho M_0^\dagger)) - tr(\llbracket S'; (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D(M_1 \rho M_1^\dagger)) \\ = & \text{ } tr(\rho) - tr(M_0 \rho M_0^\dagger) - tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D(\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger))) \\ & + tr(\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger)) - tr(\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger))\\ =& \text{ } tr(\rho) - tr(M_0 \rho M_0^\dagger) - tr(M_1 \rho M_1^\dagger) + \\ & \left(tr(\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger)) - tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D(\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger)))\right) \\ \overset{I.H.}{=}& 0+ tr(\sigma_{n+1}) \end{align}\] because \(\rho = \sigma_0\), thus \(tr(\llbracket S' \rrbracket_D(M_1 \rho M_1^\dagger)) = tr(M_1 \rho M_1^\dagger)\) by induction hypothesis for \(S'\). Also \(tr(\rho) - tr(M_0 \rho M_0^\dagger) - tr(M_1 \rho M_1^\dagger) = 0\) because \(M_0^\dagger M_0 + M_1^\dagger M_1 = \boldsymbol{I}\).

  Overall we have shown that \(tr(\rho) - tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D (\rho)) = tr(\sigma_n)\) for all \(n\) and as \(\lim_{n \to \infty} tr(\sigma_n) = 0\), \(\lim_{n \to \infty} tr(\llbracket (\boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S')^{n} \rrbracket_D (\rho)) = tr(\rho)\) and thus \(tr(\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S' \rrbracket_D (\rho)) = tr(\rho)\) (limit and \(\bigvee\) coincide as we have an increasing sequence of real numbers) and \(S\) is AST on \(\rho\).

 ◻

Proof. First we show an auxiliary result that \(ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B) = \bigvee_n \Psi_B^n(0)\) where \(\Psi_B^n\) is the \(n\)-fold composition of \(\Psi_B\):

We show by induction over \(n\) that \(\Psi_B^n(0) = F_n\) where \(F_n\) is defined as in the definition of \(ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B)\) in Table 3:

• \(n=0\): \(\Psi_B^0(0) = 0 = F_0\).

• \(n \to n+1\): \[\begin{align} \Psi_B^{n+1}(0) =&\text{ } \Psi_B(\Psi_B^n(0)) \\ =& \text{ } \boldsymbol{I}\oplus M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S \rrbracket (\Psi_B^n(0)) \odot M_1 \\ =& \text{ } \boldsymbol{I}\oplus M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S \rrbracket (F_n) \odot M_1 \\ =& \text{ } F_{n+1} \end{align}\]

Thus we have \(\Psi_B^n(0) = F_n\) for all \(n\) and thus \(\bigvee_n \Psi_B^n(0) = \bigvee_n F_n = ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B)\).

The rest of the proof is now completely analogous to the proof of Park induction for wp (Proposition [prop:park]) and thus we only give a sketch here: \(\Psi_B\) is monotonous (\(A_1 \sqsubseteq A_2 \Rightarrow \Psi_B(A_1) \sqsubseteq\Psi_B(A_2)\)) by the monotonicity of ert and by Proposition [prop:orderproperties]: \[\begin{align} A_1 \sqsubseteq A_2 &\Rightarrow M_1^\dagger \odot ert\llbracket S \rrbracket (A_1) \odot M_1 \sqsubseteq M_1^\dagger \odot ert\llbracket S \rrbracket (A_2) \odot M_1 \\ &\Rightarrow \boldsymbol{I}\oplus M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S \rrbracket (A_1) \odot M_1 \\ & \sqsubseteq\boldsymbol{I}\oplus M_0^\dagger \odot B \odot M_0 \oplus M_1^\dagger \odot ert\llbracket S \rrbracket (A_2) \odot M_1 \\ &\Rightarrow \Psi_B(A_1) \sqsubseteq\Psi_B(A_2) \end{align}\] Then \(\Psi_B(A) \sqsubseteq A\) implies \(\Psi_B^n(0) \sqsubseteq A\) completely analogous as we have the same needed properties of \(\Psi_B\) as in the wp case. Finally, we have \(ert\llbracket \boldsymbol{while } M[\overline{q}]=1 \boldsymbol{ do } S \rrbracket (B) = \bigvee_n \Psi_B^n(0) \sqsubseteq A\). ◻