We also assume that for any $\sigma \in \Mem[\DetVar]$, any $\mu_1 \in \DMem{T_1}, \mu_2 \in \DMem{T_2}$ where $T_1, T_2 \subseteq \RanVar$, the first component of
$\Sem{c}(\sigma, \mu_1)$ and $\Sem{c}(\sigma, \mu_2)$ are the same.
For any $(\sigma, \mu) \in \Config$, let

\begin{align*}
\Sem{\Skip}(\sigma, \mu)	&\triangleq (\sigma, \mu) \\
\Sem{\Assn{x_d}{e_d}}(\sigma, \mu)	&\triangleq (\sigma[x_d \mapsto \Sem{e_d} (\sigma, \mu)], \mu) \\
\Sem{\Assn{x_r}{e_r}}(\sigma, \mu)	&\triangleq (\sigma, \dbind(\mu, m \mapsto \dunit(m[x_r \mapsto \Sem{e_r}(\sigma, m)]))) \\
\Sem{\Rand{x_r}{\Unif{S}}}(\sigma, \mu)	&\triangleq (\sigma, \dbind(\mu, m \mapsto \dbind(\text{Unif}_S, v \mapsto \dunit(m[x_r \mapsto v]))))  \\
\Sem{\Seq{c}{c'}}(\sigma, \mu)	&\triangleq \Sem{c'}(\Sem{c} (\sigma, \mu)) \\
\Sem{\RCond{b}{c}{c'}(\sigma, \mu)} &\triangleq
\begin{cases}
\Sem{c}(\sigma, \mu) & \text{ if } \Sem{b}(\sigma, \mu) = \delta(\ktt)\\
\Sem{c'}(\sigma, \mu) & \text{ if } \Sem{b}(\sigma, \mu) = \delta(\kff)\\
(\sigma, \mu_1 \comb_{\rho} \mu_2) & \text{otherwise, where } (\sigma, \mu_1) =  \Sem{c}(\sigma, \mu \mid \Sem{b} \sigma = \ktt), \\
\qquad																																			& \rho = \mu(\Sem{b} \sigma = \ktt),
\text{ and } (\sigma, \mu_2) =  \Sem{c'}(\sigma, \mu \mid \Sem{b} \sigma = \kff).
\end{cases}\\
\Sem{\RWhile{b}{c}} (\sigma, \mu) &\triangleq
\lim_{n \to \infty} \Sem{(\RCondt{b}{c})^n; \RCondt{b}{\mathbf{abort}}} (\sigma, \mu)
\end{align*}

In the last case of the conditional, we write $\Sem{b} \sigma$ for the partial
evaluation of $b$ on the deterministic memory and think of it as another
expression.  So $\mu \mid \Sem{b} \sigma = \ktt$ and  $\mu \mid \Sem{b} \sigma
= \kff$ are both conditional distribution.  We assume that there is no update
to the deterministic memory when branching on randomized expressions, so the
deterministic memory of both $\Sem{c} (\sigma, \mu \mid \Sem{b} \sigma = \ktt)$
and $\Sem{c} (\sigma, \mu \mid \Sem{b} \sigma = \kff)$ remains to be $\sigma$.

In the semantics for the while loop, we can see $\mathbf{abort}$ as a command
that programmers does not have access to: for any $\sigma, \mu$,
$\Sem{\mathbf{abort}} (\sigma, \mu)$ returns the zero sub-distribution.  The
limit, taken with the point-wise order, exists because the sub-distribution's
mass monotonically increases as $n$ increases and is upper bounded by 1.  In
practice, because we assumed that all loops terminates in finite steps, the
limit is always a full distribution, so all commands in can still be
interpreted as transformers from configurations to configurations.

§.§ The atomic propositions and axioms

For any operation $\odot \in \{ \land, \lor, \negand, \indand\}$, we use the
corresponding big-operation $\bigodot \in \left \{ \bigwedge, \bigvee, \bigneg, \bigind \right \}$.

* For any constant or logical variable $N \geq 1$, let $\bigodot_{i
= 0}^{N} P_i = P_0$ abbreviate $((P_{0} \odot P_{1}) \odot \cdots ) \odot
P_{N-1}$. Formally, let $\bigodot_{i = 0}^{N} P_i = P_0$ if $N = 1$, and
let $\bigodot_{i = 0}^{N} P_i \triangleq \left(\bigodot_{i =
0}^{N - 1} P_i \right) \odot P_{N-1}$ for $N > 1$.

* For a finite multi- set of formula $\{P_i\}_{i \in S}$, let $\bigodot_{s \in S}
P_s$ abbreviate $((P_{s_0} \odot P_{s_1}) \odot \cdots ) \odot P_{s_{k}}$,
where $s_0, \dots, s_{k}$ is an arbitrary ordering of $S$.  The satisfaction
is not ambiguous since $\odot$ is associative and commutative.

* For any program variable $v \in \DetVar \cup \RanVar$, for any state
$(\sigma, \mu) \models \apEq{v}{N}$, we want $\bigodot_{i = 0}^{v} P_i$ to be equivalent to
$\bigodot_{i = 0}^{N} P_i$.  Formally,  $\bigodot_{i = 0}^{v} P_i$
abbreviates $\bigvee_{N \in \Val} ( \apEq{v}{N} \land \bigodot_{i = 0}^{N} P_i )$.

Forward direction: we fix $\sigma \in \Mem[\DetVar]$.
Let $Y_j = \{y_i \mid 0 \leq i \leq j\}$
we prove by induction on $j$ that
$(\sigma, \pi_{Y_{j} } \mu)\models  \bigneg_{i=0}^{j + 1} \apIn{y_i}  $.

If $j = 0$: then $y_1 \in \dom(\mu)$, and $(\sigma, \pi_{\{y_1\}} \mu) \models \apIn{y_1}$.

If $j \geq 1$: Assuming $(\sigma, \pi_{Y_{j - 1} } \mu)\models  \bigneg_{i=0}^{j 1} \apIn{y_i}  $.
Since $Y$ satisfies NA in $\mu$, by <Ref>, $\mu$ is $\mathcal{T}$-for any partition $\mathcal{T}$ of $Y$.
In particular, for any partition $\mathcal{T}_1$ on $Y_{j-1}$ and any partition $\mathcal{T}_2$ on $\{y_j\}$,
$\mu$ must be $\mathcal{T}_1 \cup \mathcal{T}_2$-.
$\pi_{Y_j} \mu \in \pi_{Y_{j - 1}} \mu \oplus \pi_{\{y_j\}} \mu$.
Since $(\sigma, \pi_{Y_{j - 1} } \mu)\models  \bigneg_{i=0}^{j } \apIn{y_i}  $
and $(\sigma, \pi_{\{y_j\} } \mu)\models  \apIn{y_j}  $,
that implies $(\sigma, \pi_{Y_{j} } \mu)\models  \bigneg_{i=0}^{j + 1} \apIn{y_i}  $.

Thus, $(\sigma, \pi_{Y_{j} } \mu)\models  \bigneg_{i=0}^{j + 1} \apIn{y_i}  $.
Take $j = K$, we have $(\sigma, \pi_{Y} \mu) \models  \bigneg_{i=0}^{K} \apIn{y_i}$.
By persistence, $(\sigma, \mu) \models  \bigneg_{i=0}^{K} \apIn{y_i}$.

Backward direction: for any $A, B$ being  disjoint subsets of $Y$,
by commutativity and associativity of $\negand$, we can
reorder formula and get
$(\sigma, \mu) \models \left( \bigneg_{y_i \in A} \apIn{y_i} \negand \bigneg_{y_i \in B} \apIn{y_i} \right) \negand \bigneg_{y_i \in (T \setminus (A \cup B))} \apIn{y_i}  $.
By satisfaction rules and the definition of $\oplus$, there exists $\mu' \sqsubseteq \mu$ such that
$(\sigma,  \mu') \models  \bigneg_{y_i \in A} \apIn{y_i} \negand \bigneg_{y_i \in B} \apIn{y_i}$.
By satisfaction rules again,
there exists $\mu_1, \mu_2, \mu''$ such that

$ \mu' \sqsupseteq  \mu'' \in  \mu_1 \oplus \mu_2$,
and $(\sigma, \mu_1) \models  \bigneg_{y_i \in A} \apIn{y_i} $,
and $(\sigma, \mu_2) \models  \bigneg_{y_i \in B} \apIn{y_i} $.
Note that $\mu_1$ is trivially $\{ A \}$-,
and $\mu_2$ is trivially $\{ B \}$-.
Thus, $\mu''$ satisfies $\{A, B \}$-.

Therefore, $\mu$ satisfies $(A, B)$-NA for any $A, B$ being disjoint subsets of $Y$,
i.e., $\mu$ satisfies NA on $Y$.

For any state $(\sigma, \mu)$ satisfying $\apOnehot{[x_1, \dots, x_{N-1}]}{N}$,
by <Ref>,
$\{x_1, \dots, x_N\}$ satisfies	NA in $\mu$,
and by <Ref>,
$(\sigma, \mu) \models \bigneg_{\gamma = 1}^N \apIn{x_{\gamma}} $.
by <Ref>,
$\{x_1, \dots, x_N\}$ satisfies	NA in $\mu$,
and by <Ref>,
$(\sigma, \mu) \models \bigneg_{\gamma = 1}^N \apIn{x_{\gamma}} $.

Given a distribution $\mu$ with domain $S$.
Let $\mathcal{S} = \{S_1, \dots, S_N \}$ be a partition of $S$,
$\{f_i: \Mem[S_i] \to \Mem[T_i]\}_{\mathcal{S}_i \in \mathcal{S}}$ be a family of non-decreasing functions (or a family of non-increasing functions),
and $\mathcal{T} = \{ T_1, \dots, T_N\}$ be a partition of another set $T$.

\[\mu' = 	\dbind\Big(\mu, m \mapsto  \bigoplus_{S_i \in \mathcal{S}} \dunit(f_i(\p_{S_i} m))  \Big). \]

If $\mu$ satisfies $\mathcal{S}$-, then $\mu'$ satisfies

It suffices to show that for any $\mathcal{R} = \{ R_1, \dots, R_m\}$ that coarsens $\mathcal{T}$,
for any family of non-negative non-increasing (or non-decreasing) functions $\{g_i: \Mem[R_i] \to \mathbb{R}^+\}_{R_i \in \mathcal{R}}$,

\[
\mathbb{E}_{m' \sim \mu'}\left[ \prod_{i} g_i(\p_{R_i} m')\right] \leq \prod_i \mathbb{E}_{m' \sim \mu' } \left[  g_i(\p_{R_i} m') \right].
\]

Our first step is to show that if we can obtain a distribution on $\mathcal{R}$ by first applying monotone map and then coarsening, then we can also obtaining that by first coarsening and then applying monotone map:

For any $\mathcal{R}$ that coarsens $\mathcal{T} = \{T_1, \dots, T_n \}$, there exists some coarsening function $g$ such that

\begin{align*}
\mathcal{R} = \{ \cup\{T_j \mid j \in g(i)\} \mid i \in [n] \}.
\end{align*}

Let $R_i =\cup \{T_j \mid j \in g(i)\} $.
Since $g$ is a coarsening function,
for each $i \in [n]$,
there exists exactly one $k_i$ (i.e., the index for the component in the coarsened function) such that $g(k_i) \ni i$.

$T_i \subseteq \cup \{T_j \mid j \in g(k_i)\} = R_{k_i}$.

Let $R'_i =\cup \{S_j \mid j \in g(i)\} $,
and $\mathcal{R}' = \{ R'_i \mid i \in [n]\}$.
Then $\mathcal{R}'$ coarsens $\mathcal{S}$.
Define $h_i: \Mem[R'_i] \to  \Mem[R_i]$ by having
$h_i(m) = \bowtie_{j \in g(i)} f_j(\p_{S_j} m)$.
Since each $f_i$ is monotone, then each $h_i$ also monotone in the point-wise order. Then,

\begin{align*}
\mu' =	\dbind\Big(\mu,   m \mapsto \bigoplus_{i \in [n]} \dunit(f_i(\p_{S_i} m)) \Big)
&= 	\dbind\Big(\mu, m \mapsto \bigoplus_{R'_i \in \mathcal{R}'} \dunit(h_i(\p_{R'_i} m))  \Big),
\end{align*}

so $\mu'$ is equivalent to applying $h_i$ on each component of $\mathcal{R}'$.

Also, since $\mu$ is  $\mathcal{S}$-and $\mathcal{R}'$ coarsens $\mathcal{S}$,
for any family of non-negative non-increasing (or non-decreasing) functions $\{g_i: \Mem[R'_i] \to \mathbb{R}^+\}_{R'_i \in \mathcal{R}'}$,

\begin{align} \label{eq:oldPNAreq}
\mathbb{E}_{m \sim \mu} \left[ \prod_{i} g_i(\p_{R'_i} m)\right] \leq \prod_i \mathbb{E}_{m \sim \mu}   g_i(\p_{R'_i} m) .
\end{align}

Our second step is to show that this inequality is preserved under monotone maps.

* If every $h_i$ is non-increasing and $\{g_i: \Mem[R_i] \to \mathbb{R}^+\}_{R_i \in \mathcal{R}}$ are non-decreasing,
is non-increasing,

\begin{align*}
& \mathbb{E}_{m' \sim \mu'}[ \prod_{R_i \in \mathcal{R}} g_i(\p_{R_i} m')]\\
&= \sum_{m' \in \Mem[T]} \mu'(m') \cdot \prod_{R_i \in \mathcal{R}}  g_i(\p_{R_i} m') \\
&=\sum_{m' \in \Mem[T]} \sum_{m \in \Mem[S]} \mu(m) \cdot (\prod_{R'_i \in \mathcal{R}'} \dunit(h_i(\p_{R'_i} m))(\p_{R_i} m')) \cdot \prod_{R_i \in \mathcal{R}}  g_i(\p_{R_i} m') \\
&=\sum_{m \in \Mem[S]} \mu(m) \cdot \prod_{R'_i \in \mathcal{R}'}  g_i(h_i(\p_{R'_i} m)) \\
&= \mathbb{E}_{m \sim \mu} [ \prod_{R'_i \in \mathcal{R}'} g_i(h_i(\p_{R'_i} m))] .
\end{align*}

Note that $g_i \circ f$ is non-negative non-decreasing,
then since $\mu$ satisfies <Ref>, we have

\begin{align*}
\mathbb{E}_{m \sim \mu} [\prod_{R'_i \in \mathcal{R}'} g_i(h_i(\p_{R'_i} m))]
\prod_{R'_i \in \mathcal{R}'} \mathbb{E}_{m \sim \mu} [g_i(h_i(\p_{R'_i} m))]\\
&= \prod_{R'_i \in \mathcal{R}'} \sum_{m \in \Mem[S] } \mu(m) \cdot g_i(h_i(\p_{R'_i} m)) \\
&= \prod_{R_i \in \mathcal{R}} \mathbb{E}_{m' \sim \mu' }  g_i(\p_{R_i} m') .
\end{align*}

Combined, we have $ \mathbb{E}_{m' \sim \mu'}[ \prod_{i} g_i(\p_{R_i} m')] \leq \prod_i \mathbb{E}_{m' \sim \mu' }   g_i(\p_{R_i} m')$.

* When $f_i$ is non-increasing and $\{g_i\}$ are non-negative non-decreasing,
or when $f_i$ is non-decreasing and $\{g_i\}$ are non-negative non-decreasing/non-increasing,
the proof is analogous.

Abbreviate $ \{ \bigcup_{\alpha = 0}^{K_{\gamma} + 1} \{x_{\gamma, \alpha}\} \mid 1 \leq \gamma < M\}$ as $X_M$.

For any state $(\sigma, \mu)$ satisfying $\bigneg_{\gamma = 0}^N (\bigwedge_{\alpha = 0}^{K_{\gamma} + 1} \apIn{x_{\gamma, \alpha}}) $,

we show by induction on $M$ that: for $1 \leq M \leq N$,

* $(\sigma, \mu) \models \bigneg_{\gamma = 0}^M (\bigwedge_{\alpha = 0}^{K_{\gamma}} \apIn{x_{\gamma, \alpha}}) $;

* And $\mu$ satisfies $X_M$-implies
$\mu$ satisfies $X_N$-.

Assuming that it is true for $M$, we show that for $M-1$.
By assumption, $(\sigma, \mu) \models \bigneg_{\gamma = 0}^M (\bigwedge_{\alpha = 0}^{K_{\gamma} + 1} \apIn{x_{\gamma, \alpha}}) $,
so there exists $\mu', \mu_1, \mu_2$ such that $\mu \sqsupseteq \mu' \in \mu_1 \oplus \mu_2$,
$(\sigma, \mu_1) \models \bigneg_{\gamma = 0}^{M-1} (\bigwedge_{\alpha = 0}^{K_{\gamma} + 1} \apIn{x_{\gamma, \alpha}})$ and $(\sigma, \mu_2) \models \bigwedge_{\alpha = 0}^{K_M + 1} \apIn{x_{M, \alpha}}$. Thus, $\mu'$ is $X_M$-if $\mu_1$ is $X_{M-1}$-and $\mu_2$ is $\cup_{\alpha = 0}^{K_M + 1} \{ x_{M, \alpha} \}$-. Thus,

* By the definition of $\oplus$, we have $\mu \sqsupseteq \mu_1$,
and by persistence $(\sigma, \mu) \models \bigneg_{\gamma = 0}^{M-1} (\bigwedge_{\alpha = 0}^{K_{\gamma} + 1} \apIn{x_{\gamma, \alpha}}) $;

* Since 	$(\sigma, \mu_1) \models \bigneg_{\gamma = 0}^{M-1} (\bigwedge_{\alpha = 0}^{K_{\gamma} + 1} \apIn{x_{\gamma, \alpha}})$, we have  $\cup X_{M-1}$ is inside $\dom(\sigma) \cup \dom(\mu_1)$. Thus,
if $\mu$ satisfies $X_{M-1}$-, then $\mu_1 \sqsubseteq \mu$  satisfies $X_{M-1}$-.
Trivially, $\mu_2$ is $\cup_{\alpha = 0}^{K_M} \{ x_{M, \alpha} \}$-.
Thus, $\mu'$ is $X_M$-, and $\mu$ is $X_M$-.
By inductive assumption, $\mu$ is $X_N$-.

Then, letting $M =1$ would give us: $\mu$ satisfies $X_1$-implies
$\mu$ satisfies $X_N$-.
$X_1$ is a partition of one component, so $\mu$ satisfying $X_1$-is trivial.
Therefore, $\mu$ satisfies $X_N$-.

Since $ \bigwedge_{\gamma = 0}^N y_{\gamma} = f_{\gamma}(x_{\gamma, 1}, \dots, x_{\gamma, K_{\gamma}})$ and $f_{\gamma}$ are all antitone or monotone,
by <Ref>,
$\mu$ satisfies $\{ \{ y_{\gamma} \} \mid 1 \leq \gamma < N\}$-.
Then we can show $(\sigma, \mu) \models \bigneg_{\gamma=1}^N \apIn{y_{\gamma}}$
through another simple induction or by applying the existing theorems.
If we do that by applying the theorems,
<Ref> implies that
if $\mu$ satisfies $\{ \{ y_{\gamma} \} \mid 1 \leq \gamma \leq N\}$-,
then $\{ \{ y_{\gamma} \} \mid 1 \leq \gamma \leq N\}$ satisfies NA in $\mu$.
Then, by <Ref>, $(\sigma, \mu) \models \bigneg_{\gamma=1}^N \apIn{y_{\gamma}}$.

§.§ The restriction property

We prove the restriction on deterministic memories and on randomized memories
by separate induction, and then combine them.

Let $(\sigma, \mu)$ be any configuration in $\Config$,
and let $\phi$ be a formula interpreted on $\CombModel$,
Then, for any $m \in \Mem[\DetVar \setminus \FV(\phi)]$,

\[(\sigma, \mu) \models \phi \iff (\p_{\FV(\phi)}\sigma \bowtie m, \mu) \models \phi. \]

Note that the two directions are symmetric, so we only prove the forward direction.

We prove it by induction on the syntax of formula.
Most cases are straightforward, so we only show three cases.

$\phi = P \to Q$:   Assuming $(\sigma, \mu) \models P \to Q$,
that says for any $(\sigma', \mu') \sqsupseteq (\sigma, \mu)$,
if $(\sigma', \mu') \models P$, then $(\sigma', \mu') \models Q$.

For any $(\widehat{\sigma}, \widehat{\mu}) \sqsupseteq (\p_{\FV(\phi)}\sigma \bowtie m, \mu)$,
it must $\widehat{\sigma} = \p_{\FV(\phi)}\sigma \bowtie m$ and $\widehat{\mu} \sqsupseteq \mu$.
If $ (\widehat{\sigma}, \widehat{\mu} ) \models P$,
then by $\widehat{\sigma} = \p_{\FV(\phi)}\sigma \bowtie m$
and the inductive hypothesis, $ (\sigma, \widehat{\mu}) \models P $;
since $(\sigma, \mu) \models P \to Q$ and $\widehat{\mu} \sqsupseteq \mu$,
$ (\sigma, \widehat{\mu}) \models P $ implies $ (\sigma, \widehat{\mu}) \models Q$;
and by inductive hypothesis again, $ (\p_{\FV(\phi)}\sigma \bowtie m, \widehat{mu}) \models Q $,
Thus, $ (\p_{\FV(\phi)}\sigma \bowtie m, \mu) \models P \to Q$.

$\phi = P \negand Q$:
Assuming $(\sigma, \mu) \models P \negand Q$,
then there exists
$(\widehat{\sigma}, \widehat{\mu}), (\sigma_1, \mu_1), (\sigma_2, \sigma_2)$ such that
$(\sigma, \mu) \sqsupseteq (\widehat{\sigma}, \widehat{\mu}) \in (\sigma_1, \mu_1) \oplus (\sigma_2, \mu_2)$,
$(\sigma_1, \mu_1) \models P$,
and $(\sigma_2, \mu_2) \models Q$.
By the definition of the pre-order and $\oplus$,
it must $\sigma = \widehat{\sigma} = \sigma_1 = \sigma_2$,
$\mu \sqsupseteq \widehat{\mu} \in \mu_1 \oplus \mu_2$.

By inductive hypothesis,
$(\p_{\FV(\phi)}\sigma_1 \bowtie m, \mu_1) = (\p_{\FV(\phi)}\sigma \bowtie m, \mu_1) \models P$,
and $(\p_{\FV(\phi)}\sigma_2 \bowtie m, \mu_2) = (\p_{\FV(\phi)}\sigma \bowtie m, \mu_2) \models Q$.

\[(\p_{\FV(\phi)}\sigma \bowtie m, \mu) \sqsupseteq (\p_{\FV(\phi)}\sigma \bowtie m, \widehat{\mu}) \in  (\p_{\FV(\phi)}\sigma \bowtie m, \mu_1)  \oplus (\p_{\FV(\phi)}\sigma \bowtie m, \mu_2)  . \]

So $(\p_{\FV(\phi)}\sigma \bowtie m, \mu) \models P \negand Q$.

$\phi = P \indand Q$
Analogous as the case for $P \negand Q$.

$\phi = P \indimp Q$:
Assuming $(\sigma, \mu) \models P \indimp Q$,
that says for any
$(\sigma'', \mu'') \in (\sigma, \mu) \otimes (\sigma', \mu')$,
if $(\sigma', \mu') \models P$,
then $(\sigma'', \mu'') \models Q$.

For any $(\sigma'', \mu'') \in (\p_{\FV(\phi)}\sigma \bowtie m, \mu) \otimes (\sigma', \mu')$,
it must $\sigma'' = \sigma' = \p_{\FV(\phi)}\sigma \bowtie m $, $\mu'' \in \mu \otimes \mu'$.
Thus, $(\sigma', \mu') \models P$ is equivalent to $( \p_{\FV(\phi)}\sigma \bowtie m , \mu') \models P$, and by inductive hypothesis,
that is equivalent to $(\sigma, \mu') \models P$.
It also follows that $(\sigma, \mu'') \in (\sigma, \mu) \otimes (\sigma, \mu')$.
Since $(\sigma, \mu) \models P \indimp Q$ and $(\sigma, \mu') \models P$,
we have $(\sigma, \mu'') \models Q$.
By inductive hypothesis, $ (\p_{\FV(\phi)}\sigma \bowtie m, \mu'') \models Q $,
and equivalently $(\sigma'', \mu'') \models Q$.

Thus, $(\p_{\FV(\phi)}\sigma \bowtie m, \mu) \models P \indimp Q$.

Let $(\sigma, \mu)$ be any configuration in $\Config$,
and let $\phi$ be a formula interpreted on $\CombModel$,

\[(\sigma, \mu) \models \phi \iff (\sigma, \pi_{\FV(\phi)}\mu) \models \phi. \]

The reverse direction follows by the Kripke monotonicity,
and the forward direction follows by induction on $\phi$.
The proof for most of the inductive cases is very similar to the proof that
the probabilistic model in <cit.> satisfies restriction.
The new inductive case is:

* $\phi \equiv  P \negand Q$.
Then, $\mu \models \phi$ iff there exists  $\mu', \mu_1, \mu_2$ s.t. $\mu \sqsupseteq \mu' \in \mu_1 \oplus \mu_2$, $\mu_1 \models P$ and  $\mu_2 \models Q$.
By induction, $\pi_{FV(P)} \mu_1 \models P$ and  $\pi_{FV(Q)} \mu_2 \models Q$.
Note that $\pi_{FV(P)} \mu_1 \sqsubseteq \mu_1$ and  $\pi_{FV(Q)} \mu_2 \sqsubseteq \mu_2$.
By Down-closure, there exists $\mu'' \sqsubseteq  \mu'$  such that
$\mu'' \in \pi_{FV(P)} \mu_1 \oplus \pi_{FV(Q)} \mu_2$.
This $\mu''$ satisfies $P \negand Q$.
By definition of $\oplus$ in the model,

\[dom(\mu'') = dom(\pi_{FV(P)} \mu_1) \cup dom(\pi_{FV(Q)} \mu_2 ) = FV(P) \cup FV(Q) = FV(P \negand Q) .\]

Also, by the definition of the pre-order, $\mu'' \sqsubseteq \mu' \sqsubseteq \mu$
implies that $\mu'' = \pi_{dom(\mu'')} \mu = \pi_{FV(\phi)} \mu$.
Thus, $\pi_{FV(\phi)} \mu = \mu'' \models \phi$.

Based on <Ref> and <Ref>,

\[(\sigma, \mu) \models \phi \iff (\sigma, \pi_{\phi} \mu) \models \phi  \iff (\p_{\FV(\phi)}\sigma \bowtie m, \pi_{\FV(\phi)}\mu) \models \phi. \]

For the counterexample of the restriction property, we prove a lemma.

Let $\sigma \in \Mem[\DetVar]$ be “empty” – let every deterministic variable be undefined,
$\mu $ be the uniform distribution over one hot vectors on $A, B$,
and $\phi = (\apUnif{C}{\{0, 1\}}) \negimp (\apIn{B} \indand \apIn{C})$.
Then, $(\sigma, \mu) \models \phi$.

Fix any $\mu_C$ such that $ (\sigma, \mu_C) \models \apUnif{C}{\{0, 1\}}$,
which implies that $\pi_C \mu_C (0) = 0.5$ and $\pi_C \mu_C(1) = 0.5$.

Fix $\mu_e \in \mu \oplus \mu_C$.

Since $B \in \dom(\mu)$, $\mu$ is trivially $\{\{B\}\}$-.
Similarly, $\mu_C$ is trivially $\{\{C\}\}$-.
Thus, $\mu_e \in \mu \oplus \mu_C$ must be $\{\{B\}, \{C\}\}$-.
Then for any two both monotone or antitone functions $f: \Mem[B] \to \mathbb{R}^+,
g: \Mem[C] \to \mathbb{R}^+$,

\begin{align*}
\mathbb{E}_{m \sim \mu_e}[f(\p_B m) \cdot g(\p_C m)] \leq \mathbb{E}_{m \sim \mu_e}[f(\p_B m)] \cdot \mathbb{E}_{m \sim \mu_e}[g(\p_C m)].
\end{align*}

Similarly, 	$\mu_e \in \mu \oplus \mu_C$ must be $\{\{A\}, \{C\}\}$-,
and for any two both monotone or antitone functions $f: \Mem[A] \to \mathbb{R}^+,
g: \Mem[C] \to \mathbb{R}^+$,

\begin{align}
\label{eq:AC-NA}
\mathbb{E}_{m \sim \mu_e}[f(\p_A m) \cdot g(\p_C m)] \leq \mathbb{E}_{m \sim \mu_e}[f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu_e}[g(\p_C m)].
\end{align}

Suppose variables $B$ and $C$ are not independent in $\mu_e$,
then by <Ref>,
there must exists some both monotone or both antitone functions $f: \Mem[B] \to \mathbb{R}^+,
g: \Mem[C] \to \mathbb{R}^+$ such that

\begin{align*}
& \mathbb{E}_{m \sim \mu_e}[f(\p_B m) \cdot g(\p_C m)] < \mathbb{E}_{m \sim \mu_e}[f(\p_B m)] \cdot \mathbb{E}_{m \sim \mu_e}[g(\p_C m)] \\
\iff & 0.5 \cdot f(0) \cdot \left( g(1) \cdot P(C = 1 \mid B = 0) + g(0) \cdot P(C = 0 \mid B = 0) \right) \\
&+  0.5 \cdot f(1) \cdot \left( g(1) \cdot P(C = 1 \mid B = 1) + g(0) \cdot P(C = 0, B = 1) \right) \\
<& (0.5 \cdot f(0) + 0.5 \cdot f(1) )  \cdot ( 0.5 \cdot g(1) + 0.5 \cdot g(0)) ,
\end{align*}

where $ P(\dots)$ denotes the respective probability that in $\mu_e$.
Since $\mu_e \in \mu \oplus \mu_C$,
we have $\mu_e \sqsupseteq \mu$,
and $\mu$ being a uniform distribution over one-hot vectors on $A, B$ indicates that
for any $m$ in the support of $\mu_e$, $A = 1$ iff $B = 0$, and $A = 0$ iff $B = 1$.
$P(C = v \mid B = 0) = P(C = v \mid A = 1)$ and $P(C = v \mid B = 1) = P(C = v \mid A = 0). $
Also, by Bayes theorem, we have

\begin{align*}
&P(C = v \mid A = 0) \cdot P(A = 0) + P(C = v \mid A = 1) \cdot P(A = 1) = P(C = v)  \\
\implies & P(C = v \mid A = 0) \cdot 0.5 + P(C = v \mid A = 1) \cdot 0.5 = 0.5 \\
\iff & P(C = v \mid A = 0) = 1 - P(C = v \mid A = 1) .
\end{align*}

Let $X = P(C = 1 \mid A = 1)$, $Y = P(C = 0 \mid A = 1)$, then we have

\begin{align*}
& 0.5 \cdot f(0) \cdot \left( g(1) \cdot X + g(0) \cdot Y \right)
+  0.5 \cdot f(1) \cdot \left( g(1) \cdot (1-X) + g(0) \cdot (1 - Y) \right) \\
<& (0.5 \cdot f(0) + 0.5 \cdot f(1) )  \cdot ( 0.5 \cdot g(1) + 0.5 \cdot g(0)) \\
\iff & f(0) \cdot  g(1) \cdot (X - 0.5) + f(0) \cdot  g(0) \cdot (Y - 0.5)
+ f(1) \cdot g(1) \cdot (0.5-X) + f(1) \cdot  g(0) \cdot (0.5 - Y) < 0 \\
\iff & (f(0) - f(1)) \cdot  g(1) \cdot (X - 0.5) + (f(0) - f(1)) \cdot  g(0) \cdot (Y - 0.5) < 0 \\
\iff 			& 0.5 \cdot f(1) \cdot \left( g(1) \cdot X + g(0) \cdot Y \right)
+  0.5 \cdot f(0) \cdot \left( g(1) \cdot (1-X) + g(0) \cdot (1 - Y) \right) \\
<& (0.5 \cdot f(0) + 0.5 \cdot f(1) )  \cdot ( 0.5 \cdot g(1) + 0.5 \cdot g(0)) .
\end{align*}

Viewing $f$ as a function from $\Mem[A]$ to $\mathbb{R}^+$,
this is equivalent to

\begin{align*}
\mathbb{E}_{m \sim \mu_e}[f(\p_A m) \cdot g(\p_C m)] < \mathbb{E}_{m \sim \mu_e}[f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu_e}[g(\p_C m)] .
\end{align*}

The last inequality contradicts <Ref>.

Therefore, $B$ and $C$ must be independent in $\mu_e$.
Hence, $\mu_e \models \apIn{B} \sepand \apIn{C}$, and $\mu \models \phi$.

Let $A, B, C$ be three variables in $\RanVar$.
Let $\phi = (\apUnif{C}{\{0, 1\}}) \negimp (\apIn{B} \indand \apIn{C})$.
Let $\sigma$ be a deterministic memory where every deterministic variable is undefined,
and $\mu $ be the uniform distribution over one hot vectors on $A, B$.
Then, we claim $(\sigma, \mu) \models \phi$
but $(\sigma, \pi_{\{B,C\}} \mu ) \not\models \phi$.
For $(\sigma, \mu) \models \phi$, it suffices to show that for any $\mu_C$
where $C$'s value is the uniform distribution on $\{0, 1\}$, for any $\mu'
\sqsupseteq \mu$, and $\mu_e \in \mu' \oplus \mu_C$, $B$ and $C$ are
independent in $\mu_e$ according to <Ref>.
The intuition is that $\mu_e$ must satisfies $\{B, C\}$-and $\{A, C\}$-,
and since $A$'s value is always the opposite of $B$'s value,
$(B, C)$ has to satisfy pairwise independence in $\mu_e$.
To show $(\sigma, \pi_{\{B,C\}} \mu) \not\models \phi$,
we first note that $\pi_{\{B,C\}} \mu = \pi_{\{B\}} \mu$ is a uniform distribution of $0$ and $1$ on $B$.
Let  $\mu_C' \in \DMem{\{C\}}$ be the uniform distribution on $\{0, 1\}$,
$\mu' \in \DMem{\{B, C\}}$ be the uniform distribution over one-hot vectors on $B,C$.
Clearly, $B, C$ are not independent in $\mu'$, so $\mu' \not\models \apIn{B} \indand \apIn{C}$.
Also, $\mu'$ is in $\pi_{\{B, C\}} \mu \oplus \mu_C'$. So $\pi_{B,C} \mu \not\models \apUnif{C}{\{0, 1\}}  \negimp (\apIn{A} \indand \apIn{C})$.

§.§ The proof system of the program logic

The proof for the soundness of the frame rule relies on the following corollary of

Let $S, T \subseteq \Var$ be two disjoint sets of variables, and $\mathcal{T}$
is sub-partition of $T$.  Suppose that $f : \Mem[S] \to \Mem[S']$ is a
monotonically non-decreasing non-negative function, and $S'$ disjoint from
$T$.  If $\mu$ with domain $S \cup T$ satisfies $\{S\} \cup
\mathcal{T}$-, then $\dbind(\mu, m \mapsto \dunit(f(\pi_S m)) \oplus
\dunit(\pi_T m)) \in \DMem{S' \cup T}$ satisfies $\{S'\} \cup
\mathcal{T}$-.

We can reduce to <Ref>:
Let $S_1 = S$, $T_1 = S'$,
and $\{S_2, \dots, S_n\} = \{T_2, \dots, T_n\} = \mathcal{T}$.
Let $f_1 = f$ and the rest of $f_i$ to be the identity map.
Note that we have assumed to only work with non-negative values, so identity maps are also monotonically non-decreasing non-negative function.

We only prove the cases not already in <cit.>.

Rule: Cond.

For any configuration $(\sigma, \mu) \models \phi$,
by side-condition that $\models \phi \rightarrow \apDetm{b}$,
$(\sigma, \mu) \models \apDetm{b}$.
Thus, $\Sem{b} (\sigma, \mu)$ must be a Dirac distribution.
Since the commands are well-typed, $\Sem{b} (\sigma, \mu)$ is a distribution over booleans.
So $\Sem{b} (\sigma, \mu)$ is either a Dirac distribution of truthful value $\ktt$
or a Dirac distribution of false value $\kff$.

If $\Sem{b} (\sigma, \mu)$ is a Dirac distribution of truthful value $\ktt$,
then for any $m$ in the support of $\mu$, $\Sem{b}(\sigma, m) = \ktt$,
and thus, $(\sigma, \mu) \models \phi \land \apEq{b}{\ktt}$.
By the side-condition $\vdash \hoare{\phi \land \apEq{b}{\ktt} }{c}{\psi}$
and inductive hypothesis that this judgement is sound,
$\Sem{c} (\sigma, \mu) \models \psi$.
When $\Sem{b} (\sigma, \mu) = \delta(\ktt)$, the semantics say that $ \Sem{\RCond{b}{c}{c'}} (\sigma, \mu) = \Sem{c} (\sigma, \mu) \models \psi$.

Symmetrically, when $\Sem{b} (\sigma, \mu) = \delta(\kff)$,
$ \Sem{\RCond{b}{c}{c'}} (\sigma, \mu) = \Sem{c'} (\sigma, \mu) \models \psi$.

Rule: Loop.
For any $(\sigma, \mu) \models \phi$, the side condition implies $(\sigma, \mu) \models \apDetm{b}$. We show by induction that for any $n$,
$\Sem{(\RCondt{b}{c})^n} (\sigma, \mu) \models \phi \land \apDetm{b}$,
$\Sem{(\RCondt{b}{c})^n} (\sigma, \mu) \models \phi \land \apEq{b}{\kff}$ implies
$\Sem{(\RCondt{b}{c})^{n + 1}} (\sigma, \mu) \models \phi \land \apEq{b}{\kff}$.

Say $(\sigma', \mu') = \Sem{(\RCondt{b}{c})^n} (\sigma, \mu)$. Assuming 	$(\sigma', \mu') \models \phi \land \apDetm{b}$, there are two possibilities:

* $(\sigma', \mu') \models \phi \land \apEq{b}{\kff}$, then

\[ \Sem{(\RCondt{b}{c})^{n+1} } (\sigma, \mu) = \Sem{\RCondt{b}{c} }
(\sigma', \mu') = (\sigma', \mu') \models \phi \land \apEq{b}{\kff}. \]

* $(\sigma', \mu') \models \phi \land \apEq{b}{\ktt}$, then

\[ \Sem{(\RCondt{b}{c})^{n+1} } (\sigma, \mu) = \Sem{\RCondt{b}{c} } (\sigma', \mu')
= \Sem{c}  (\sigma', \mu') \models \phi, \]

where the last satisfaction is guaranteed by $\vdash \hoare{\phi \land \apEq{b}{\ktt}}{c}{\phi}$.
Since $\models \phi \to \apDetm{b}$, so $\Sem{\RCondt{b}{c} } (\sigma', \mu') \models \phi \land \apDetm{b}$.

Since we assumed that the loop ends in finite step,
there exists a finite number $N$ such that
$\Sem{(\RCondt{b}{c})^N} (\sigma, \mu) \models \phi \land \apEq{b}{\kff}$ and
also $\Sem{(\RCondt{b}{c})^{N -1}} (\sigma, \mu) \models \phi \land \apEq{b}{\ktt}$
if $N > 1$.

$\Sem{\RWhile{b}{c}} (\sigma, \mu) = \Sem{(\RCondt{b}{c})^{N}} (\sigma, \mu)
\models \phi \land \apEq{b}{\kff}$.

Rule: RCase.
For any $(\sigma, \mu) \models \phi \indand \eta$,
there exists $\mu', \mu_1, \mu_2$ such that $\mu \sqsupseteq \mu' \in \mu_1 \oplus \mu_2$
and $(\sigma, \mu_1) \models \phi$, $(\sigma, \mu_2) \models \eta$.

Say $\mu_2$ is in $\DMem{T}$, then for any $m$ in the support of $\mu_2$,
the conditional distribution $\mu_2 \mid T = m$ is a Dirac distribution of $m$,
i.e., $\delta(m)$.
Since $\eta \in \CCond$ (closed under conditioning),
so $(\sigma, \delta(m)) \models \eta$,
and thus $(\sigma, \delta(m)) \models \bigvee_{\alpha \in S} \eta_\alpha$.
Then, there exists $\alpha$ such that $(\sigma, \delta(m)) \models \eta_\alpha$.
Since $\dom(\mu_1)$ and $\dom(\mu_2)$ are independent in $\mu'$,
the conditional distribution $\mu' \mid T = m$ is in $\mu_1 \oplus \delta(m)$.
So $\mu' \mid T = m \models \phi \indand \eta_\alpha$.
By the side-condition $\vdash \phi \indand \eta_{\alpha}$ and inductive hypothesis that
it is sound, we have $\Sem{c} (\sigma,\mu' \mid T = m) \models \psi$.

For any command $c$, any condition $b$,
let $(\sigma_b, \mu_b) = \Sem{c} (\sigma, \mu' \mid b)$ and $ (\sigma_b, \mu_{\neg b}) = \Sem{c}(\sigma, \mu' \mid \neg b)$.
We can show by induction on the semantics of commands that
$\Sem{c} (\sigma, \mu') $ is a convex combination of $(\sigma, \mu' \mid b)$
and $(\sigma, \mu' \mid \neg b) $:
$\Sem{c} (\sigma, \mu') = (\sigma, (\mu' \mid b) \comb_{\mu'(b = \ktt)} (\mu' \mid \neg b) ) $.
Thus, $\Sem{c} (\sigma,\mu')$ is a convex combination of
all $\Sem{c} (\sigma,\mu' \mid T = m) $, where $m$ in the support of $\mu'$.
Since each of $\Sem{c} (\sigma,\mu' \mid T = m)$ satisfies $\psi$ and $\psi$ is
closed under mixture,
we have  $\Sem{c} (\sigma,\mu') \models \psi$.
We can also show  by induction on the semantics of commands that
$\Sem{c}(\sigma, \mu) \sqsupseteq \Sem{c}(\sigma, \mu')$ if $\mu \sqsupseteq \mu'$.
So by persistence $\Sem{c}(\sigma, \mu) \models \psi$.

Rule: ProbBound.
For any program state $(\sigma, \mu) \models \Pr[ev_1] \geq 1 - \epsilon$,
let event $ev_1^{\sigma}: \Mem[\dom(\mu)] \to \{0, 1\}$ be the result of partially
interpreting $ev_1$ on $\sigma$, i.e.,
$ev_1^{\sigma} = \text{curry}(\Sem{ev_1}) (\sigma)$,
and denote the function $\lambda x. 1 - ev_1^{\sigma}(x)$ as $\neg ev_1^{\sigma}$.
We also write $\Pr_{\mu}[ev_1^{\sigma}]$ for
$\sum_{m \in \DMem{\dom(\mu)}} \mu(m) \cdot ev_1^{\sigma}(m)$.

We can express $\mu$ as the convex combination of two conditional distributions,

\[
\mu = \Pr_{\mu}[ev_1^{\sigma}] \cdot (\mu \mid ev_1^{\sigma})
+ \Pr_{\mu}[\neg ev_1^{\sigma}] \cdot (\mu \mid \neg ev_1^{\sigma}).
\]

Let $(\sigma', \mu_{ev_1^{\sigma}}) = \Sem{c}(\sigma, (\mu \mid ev_1^{\sigma}))$.
Since assignments to deterministic memories can only use variables in the
deterministic memories, there exists probabilistic memories $\mu_{\neg ev_1^{\sigma}}$
such that
$(\sigma', \mu_{\neg ev_1^{\sigma}}) = \Sem{c}(\sigma, (\mu \mid \neg ev_1^{\sigma}))$.
Then, by induction on the denotational semantics,
we can prove that
$\Sem{c} (\sigma, \mu) = (\sigma', \mu_{ev_1^{\sigma}} \circ_{\Pr_{\mu}[ev_1^{\sigma}]} \mu_{\neg ev_1^{\sigma}})$.

By construction, $\Sem{ev_1} (\sigma, (\mu \mid ev_1^{\sigma})) = 1$,
so $ (\sigma, (\mu \mid ev_1^{\sigma})) \models ev_1$.
Also, by the assumption and inductive hypothesis, we have
$\models \hoare{ev_1}{c}{\Pr[ev_2] \geq 1- \delta}$,
which implies

\[\Sem{c}(\sigma, (\mu \mid ev_1^{\sigma})) = (\sigma', \mu_{ev_1^{\sigma}}) \models \Pr[ev_2] \geq 1 - \delta.\]

By definition, that means
$\Pr_{(\sigma', \mu_{ev_1^{\sigma}})}[ev_2] \geq 1 - \delta $.
Then, by the law of total probability,

\begin{align*}
\Pr_{(\sigma', \mu_{ev_1^{\sigma}} \circ_{\Pr_{\mu}[ev_1^{\sigma}]} \mu_{\neg ev})} [ev_1^{\sigma}]
&\leq \Pr_{(\sigma', \mu_{ev_1^{\sigma}})} [ev_2] + \Pr_{\mu}[\neg ev_1^{\sigma}] \\
&\leq \delta +  \Pr_{\sigma, \mu}[\neg ev_1] \tag{because $\Pr_{\mu}[\neg ev_1^{\sigma}] = \Pr_{\sigma, \mu}[\neg ev_1]$}\\
&\leq \delta +  \epsilon  \tag{because $(\sigma, \mu) \models \Pr[ev_1] \geq 1 - \epsilon$,}
\end{align*}

$\Sem{c} (\sigma, \mu)\models \Pr[ev_2] \leq \delta + \epsilon$.

Rule: NegFrame.  For any $(\sigma, \mu) \models ev_1 \sepand \eta$,
there exists $k_1, k_2, \mu'$ such that $\mu \sqsupseteq \mu' \in k_1 \oplus k_2$, and
$(\sigma, k_1)	\models \phi$ and $(\sigma, k_2) \models \eta$.

Let $S_1 \triangleq \dom(k_1)$,
and note that $(\sigma, k_1) \models \phi$ and $\models \phi \rightarrow \apIn{\RV(c)}$
implies $(\sigma, k_1) \models \apIn{\RV(c)}$,
and thus $\RV(c) \cap \RanVar \subseteq S_1$.
Let $S_2 \triangleq \dom(k_2) \cap \FV(\eta)$.
Then, $\MV(c)$  is disjoint from $S_2$ because $S_2 \subseteq \FV(\eta)$ and $\FV(\eta) \cap \MV(c) = \emptyset$;
also, by restriction,  $(\sigma, \pi_{S_2} k_2) \models \eta$.

Since $k_1 \oplus k_2$ is non-empty, $dom(k_1), dom(k_2)$ are disjoint;
since $S_1 = dom(k_1), S_2 \subseteq dom(k_2)$, $S_1, S_2$ are disjoint.

Let $(\sigma_e, \mu_e) = \denot{c} (\sigma, \mu)$.
Denote $\RV(c) \cap \DetVar$ as $R_1$, $\MV(C) \cap \DetVar$ as $M_1$,
$\RV(c) \cap \RanVar$ as $R_2$, $\MV(C) \cap \RanVar$ as $M_2$.
By the soundness of $\RV, \WV$, and $\MV$,
there exists $G: \Mem[R_1] \to \Mem[M_1]$,
$F : \Mem[\RV(c)]	\to \DMem{M_2}$ such that:

\begin{align*}
\sigma_e &= G(\p_{R_1} \sigma) \bowtie \p_{\DetVar \setminus M_1} \sigma \\
\mu_e &= \dbind(\mu, m \mapsto F(\p_{R_1} \sigma \bowtie \p_{R_2} m) \otimes  \dunit(\p_{\dom(\mu) \setminus M_2} m) ) .
\end{align*}

Since $R_2 \subseteq S_1$, and $S_2$ is disjoint of $S_1$ and $\MV(c)$,
we have

\begin{align}
\pi_{M_2 \cup S_1 \cup S_2} \mu_e
&= \dbind(\pi_{S_1 \cup S_2}  \mu, (m_1, m_2) \mapsto F(\p_{R_1} \sigma \bowtie \p_{R_2} m_1) \otimes \dunit(\p_{S_1 \setminus M_2} m_1) \otimes \dunit(m_2)) . \label{eq:Fmap}
\end{align}

One implication is that $(\sigma_e, \pi_{S_2} \mu_e) \models \eta$:
<Ref>  implies that $\pi_{S_2} \mu_e = \pi_{S_2} \mu$.
We $(\sigma, \pi_{S_2} \mu ) \models \eta$, so  $(\sigma, \pi_{S_2} \mu_e ) \models \eta$.
By restriction, for any $m \in \Mem[\DetVar \setminus \FV(\eta)]$,
$(\p_{\FV(\eta)} \sigma \bowtie m, \pi_{S_2} \mu_e) \models \eta$.
Since $	\sigma_e = G(\p_{R_1} \sigma) \bowtie \p_{\DetVar \setminus M_1} \sigma $,
and $\FV(\eta) \cap \MV(c) = \emptyset$ implies that $\FV(\eta) \cap \DetVar \subseteq \DetVar \setminus M_1$,
and $(\sigma_e, \pi_{S_2} \mu_e) \models \eta$.

If $y \in \DetVar$, then $ \Sem{y} (\sigma_e, m_F \bowtie \p_{X \cap \RanVar} m ) = \sigma_e (y)$.
Thus, $(\sigma_e, t) \models \apIn{y}$ where $t$ is the trivial distribution in $\DMem{\emptyset}$.
Also, $(\sigma_e, \mu_e) \in (\sigma_e, t) \circ (\sigma_e, \mu_e)$,
where $ (\sigma_e, \mu_e) \sqsupseteq (\sigma_e, \pi_{S_2} \mu_e) \models \eta$.
So $(\sigma_e, \mu_e) \models \eta$.

If $y \notin \MV(c)$, then $\{y\} \cup S_2 \subseteq \dom(\mu) \setminus \MV(c)$,
and thus $\pi_{\{y\} \cup S_2}  \mu_e = \pi_{\{y\} \cup S_2} \mu$.

* Since $\vdash \hoare{\phi}{c}{\apEq{y}{f(X)}}$, by inductive assumption we have $\denot{c} (\sigma, k_1) \models \apEq{y}{f(X)}$.
Updates to deterministic variables only depend on deterministic program state, so $\denot{c} (\sigma, k_1)  = (\sigma_e, \mu_k)$ for some $\mu_k$.
And $y \notin \MV(c)$ implies that $ \pi_{\{y \}} \mu_k =  \pi_{\{y \}} \mu = \pi_{\{y\}} k_1$.
The restriction property and $\denot{c} (\sigma, k_1) \models \apEq{y}{f(X)}$ implies $(\sigma_e, \pi_{\{y\}} k_1) = (\sigma_e, \pi_{\{y\}} \mu_k) \models \apIn{y}$.

* $(\sigma_e, \pi_{S_2} \mu) \models \eta$.

* $\mu \sqsupseteq \mu' \in k_1 \oplus k_2$, so $\pi_{\{y\} \cup S_2} \mu \in \pi_{\{ y \}}k_1 \oplus \pi_{S_2} k_2$ too.

Therefore, $(\sigma_e, \pi_{\{y\} \cup S_2} \mu) \models \apIn{y} \negand \eta $.
Since $ (\sigma_e, \mu_e)  \sqsupseteq (\sigma_e,  \pi_{\{y\} \cup S_2} \mu_e)  = (\sigma_e,  \pi_{\{y\} \cup S_2} \mu)$,
by persistence, $  (\sigma_e, \mu_e) \models \apIn{y} \negand \eta$.

If $ y \in \RanVar$ and $y \in \MV(c)$,
our overall strategy is to first connect $F$ with $f$ and show the operation on variable $y$ is a monotone map,
and then apply monotone map closure to establish the NA between $y$ and $\eta$.

Since $(\sigma, \pi_{S_1}\mu)
= (\sigma, k_1) \models \phi$, by persistence $(\sigma, \mu) \models \phi$.
By side-condition that $\vdash \{\phi\} c \{ \apEq{y}{f(X)} \}$ and by induction
that the proof rules are sound, it must $\denot{c}(\sigma,
\mu) =  (\sigma_e, \mu_e)  \models \apEq{y}{f(X)}$.  By restriction, $(\sigma_e, \pi_{X \cup \{y\}} \mu_e)
\models \apEq{y}{f(X)}$.

Since $X \cap \RanVar \subseteq (\RV(c) \cap \RanVar) \setminus \MV(c) \subseteq S_1
\setminus \MV(c)$ and $y \in \MV(c)$,

\begin{align}
\pi_{X \cup \{y\}}  \mu_e &= \pi_{X \cup \{y\}} \pi_{ S_1 \cup \MV(c)} \denot{c} \mu \notag\\
&= \pi_{X \cup \{y\}} \dbind(\pi_{S_1}  \mu, m \mapsto F(\p_{R_1} \sigma \bowtie \p_{R_2} m) \otimes \dunit(\p_{S_1 \setminus M_2} m)) \notag \\
&=\dbind(\pi_{S_1}  \mu,  m \mapsto \pi_{\{y\}} F(\p_{R_1} \sigma \bowtie \p_{R_2} m) \otimes \dunit(\p_{X \cap \RanVar} m)) 																										\label{eq:projecty}
\end{align}

Since $(\sigma_e, \pi_{X \cup \{y\}}  \mu_e)  \models \apEq{y}{f(X)}$, for every $m_e$ in the support of $ \pi_{X \cup \{y\}}  \mu_e$,
we have $\Sem{y} (\sigma_e, m_e) = \Sem{f(X)} (\sigma_e, m_e)$.
By <Ref>, a memory $m_e$ is in the support of $ \pi_{X \cup \{y\}}  \mu_e$ if and only if there exists some $m, m_F$
such that $m$ is in the support of $\mu$, and $m_F$ is in the support of $\pi_{\{y\}} F(\p_{R_1} \sigma \bowtie \p_{R_2} m)$,
and $m_e = m_F \bowtie \p_{X \cap \RanVar} m$.
Thus, the condition we have is:
for every  $m$ is in the support of $\mu$ and $m_F$ is in the support of $\pi_{\{y\}} F(\p_{R_1} \sigma \bowtie \p_{R_2} m)$,

\[ \Sem{y} (\sigma_e,m_F \bowtie \p_{X \cap \RanVar} m )
= \Sem{f(X)} (\sigma_e, m_F \bowtie \p_{X \cap \RanVar} m ) . \]

Since $f$ does not depend on states and $X$ do not depend on $m_F$,
we also have that $\Sem{f(X)} (\sigma_e, m_F \bowtie \p_{X \cap \RanVar} m ) =   \Sem{f(X)} (\sigma, m)$.

If $y \in \RanVar$, then $\Sem{y} (\sigma_e,m_F \bowtie \p_{X \cap \RanVar} m) = m_F(y)$,
so it must $m_F(y) = \Sem{f(X)} (\sigma, m) $.
so although $F$ is a randomized function according to its type,
for any $m$ in the support of $\mu$,
$\pi_{\{y\}} F(\p_{R_1} \sigma \bowtie \p_{R_2} m) $  is a Dirac distribution:

\[ \pi_{\{y\}} F(\p_{R_1} \sigma \bowtie \p_{R_2} m) = \delta(\Sem{f(X)} (\sigma, m)). \]

Fixing $\sigma$, then there exists $f'$ such that $ \Sem{f(X)} (\sigma, m) = f'(\p_{X \cap \RanVar} m)$
and $f'$ is monotone as $f$ is monotone. Since $X \cap \RanVar \subseteq S_1 $,
we can also make $f'$ to have type $\Mem[S_1] \to \Val$.

\begin{align*}
\pi_{\{y\} \cup S_2} \mu_e
&= \dbind(\pi_{S_1 \cup S_2}  \mu, (m_1, m_2) \mapsto  \pi_y F(\p_{R_1} \sigma \bowtie \p_{R_2} m_1) \otimes \dunit(m_2))\\
&= \dbind(\pi_{S_1 \cup S_2}  \mu, (m_1, m_2) \mapsto  \dunit(\Sem{f(X)} (\sigma, m_1)) \otimes \dunit(m_2))\\
&= \dbind(\pi_{S_1 \cup S_2}  \mu, (m_1, m_2) \mapsto  \dunit(f'(m_1)) \otimes \dunit(m_2)) .
\end{align*}

Let $	\mu_c = \pi_{\{y\} \cup S_2} (\mu_e)$.
We will then show that
$(\sigma_e, \mu_c) \models \apIn{y} \sepand \eta. $

Let $g_1 = \pi_{y} (\mu_e)$, $g_2 = \pi_{S_2} \mu $,
it suffices to show that $\mu_c \in g_1 \oplus g_2$.
and $g_1 \models \apIn{y} $,
$g_2 \models \eta$:

* $(\sigma_e, \mu_e) \models \apEq{y}{f(X)}$, so $(\sigma_e, \mu_e) \models \apIn{y}$.
By restriction, $(\sigma_e, g_1) \models \apIn{y}$.

* $g_2 = \pi_{S_2} \mu = \pi_{FV(\eta)} \pi_{dom(k_2)} \mu = \pi_{FV(\eta)} k_2 $,
so $(\sigma, g_2) \models \eta$.
By <Ref>, for any $m \in \Mem[\DetVar \setminus \FV(\eta)]$,
$(\p_{\FV(\eta)} \sigma \bowtie m, g_2) \models \eta$.
Since $	\sigma_e = G(\p_{R_1} \sigma) \bowtie \p_{\DetVar \setminus M_1} \sigma $,
and $\FV(\eta) \cap \MV(c) = \emptyset$ implies that $\FV(\eta) \subseteq \DetVar \setminus M_1$,
$(\sigma_e, g_2) \models \eta$.

* First,
$\pi_{\{ y\}} \mu_c = \pi_{\{ y\}} \mu_e = g_1$,
and $\pi_{S_2} \mu_c = \pi_{S_2} \mu_e = \pi_{S_2} \mu = g_2$.

Second, $\pi_{dom(k_1) \cup dom(k_2)} \mu \in k_1 \oplus k_2$
implies that $\pi_{dom(k_1) \cup dom(k_2)} \mu$ is
$\mathcal{S}' \cup \mathcal{T}'$-for any $\mathcal{S}', \mathcal{T}'$ such that $k_1$ is $\mathcal{S}'$-, $k_2$ is $\mathcal{T}'$-.
Because $\pi_{S_1} \mu$ is always $\{S_1\}$-,
$\pi_{S_1 \cup S_2}\mu$ is $\{S_1\} \cup \mathcal{T}$-for  any $\mathcal{T}$ such that $g_2$ is $\mathcal{T}$-.
Recall that

\begin{align*}
\mu_c = \dbind(\pi_{S_1 \cup S_2}  \mu, (m_1, m_2) \mapsto  \dunit(f'(m_1)) \otimes \dunit(m_2)) .
\end{align*}

Thus, by the monotonicity map closure <Ref>,
$\mu_c$ is $\{y\} \cup \mathcal{T}$ -for  any $\mathcal{T}$ such that $g_2$ is $\mathcal{T}$-.
Thus, $\mu_c \in g_1 \oplus g_2$, and therefore $(\sigma_e, \mu_c) \in (\sigma_e, g_1) \oplus (\sigma_e, g_2) $.

Therefore, $(\sigma_e, \mu_c) \models \apIn{y} \indand \eta$.

By persistence,  $(\sigma_e, \mu_e) \models \apIn{y} \indand \eta$.

§ COMPLETENESS OF $M$-BI

§.§ $\idxset$-BI Algebras

An BI algebra is an algebra $\mathcal{A} = (A, \land, \lor, \rightarrow, \top, \bot, \sepand, \sepimp, \top^{\sepand})$ such that

* $(A, \land, \lor, \rightarrow, \top, \bot)$ is a Heyting algebra

* $(A, \sepand, \top^{\sepand})$ is a commutative monoid

* $a \sepand b \leq c$ if and only if $a \leq b \sepimp c$

where $\leq$ is the ordering associated with the Heyting algebra.

An $\idxset$-BI algebra is an algebra $\mathcal{A} = (A, \land, \lor, \rightarrow, \top, \bot, \sepand_{\idx \in \idxset}, \sepimp_{\idx \in \idxset}, \top^{\sepand}_{\idx \in \idxset})$ such that

* For each $\idx \in \idxset$, the structure $(A, \land, \lor, \rightarrow, \top, \bot, \sepand_{\idx}, \sepimp_{\idx}, \top^{\sepand}_{\idx})$ is a BI-algebra

* If $\idx_1 \leq \idx_2$ then $a \sepand_{\idx_1} b \leq a \sepand_{\idx_2} b$

We can interpret $M$-BI in an $M$-BI algebra $A$. Let $\valuation :
\mathcal{AP} \rightarrow A$ be a map assigning atomic propositions to elements
of $A$. We extend $\valuation$ to an interpretation $\llbracket - \rrbracket_{\valuation}$
mapping propositions to elements of $A$, defined by:

\begin{align*}
\alginterp{p} &= \valuation(p) \\
\alginterp{\top} &= \top \\
\alginterp{\sepid_\idx} &= \top^{\sepand}_{\idx} \\
\alginterp{\bot} &= \bot \\
\alginterp{P \land Q}_\valuation &= \alginterp{P}_\valuation \land \alginterp{Q}_\valuation \\
\alginterp{P \lor Q}_\valuation &= \alginterp{P}_\valuation \lor \alginterp{Q}_\valuation \\
\alginterp{P \rightarrow Q}_\valuation &= \alginterp{P}_\valuation \rightarrow \alginterp{Q}_\valuation \\
\alginterp{P \sepand_{\idx} Q}_\valuation &= \alginterp{P}_\valuation \sepand_{\idx} \alginterp{Q}_\valuation \\
\alginterp{P \sepimp_{\idx} Q}_\valuation &= \alginterp{P}_\valuation \sepimp_{\idx} \alginterp{Q}_\valuation \\
\end{align*}

If $P \vdash Q$ is provable, then for all $\valuation$, $\alginterp{P}_\valuation \leq \alginterp{Q}_\valuation$.

By induction on the derivation of $P \vdash Q$. The cases for everything except the Inclusion rules show follow from the exact same argument as for standard BI and BI-algebra, as in Simon Docherty's thesis.

For the remaining case of $\sepand$-inclusion, let $\idx_1 \leq \idx_2$. Then we have

\[\alginterp{P \sepand_{\idx_1} Q}_\valuation = \alginterp{P}_\valuation \sepand_{\idx_1} \alginterp{Q}_\valuation \leq \alginterp{P}_\valuation \sepand_{\idx_2} \alginterp{Q}_\valuation \leq \alginterp{P \sepand_{\idx_2} Q}_\valuation\]

The Lindenbaum-Tarski algebra corresponding to $\idxset$-BI is the set of all equivalence classes of interprovable propositions. That is, define the equivalence relation $P \sim Q$ as $P \vdash Q$ and $Q \vdash P$. We will show that the set of equivalence classes of this relation forms an $\idxset$-BI algebra. Let $[P]_\sim$ be the equivalence class of $P$ under $\sim$.
Take $\sepid_{\idx}$, $\top$, and $\bot$ to be $[\sepid_{\idx}]_{\sim}$, $[\top]_{\sim}$, and $[\bot]_{\sim}$, respectively. Then we define:

\begin{align*}
[P]_{\sim} \land [Q]_\sim &= [P \land Q]_\sim \\
[P]_{\sim} \lor [Q]_\sim &= [P \lor Q]_\sim \\
&\vdots \\
[P]_{\sim} \sepand_{\idx} [Q]_\sim &= [P \sepand_{\idx} Q]_\sim \\
[P]_{\sim} \sepimp_{\idx} [Q]_\sim &= [P \sepimp_{\idx} Q]_\sim \\
\end{align*}

The fact that these operations are well-defined and form a $\idxset$-BI algebra follows almost entirely from the corresponding result for normal BI outlined in Docherty's thesis. The only remaining case is to check that if $\idx_1 \leq \idx_2$ then $[P]_{\sim} \sepand_{\idx_1} [Q]_{\sim} \leq [P]_{\sim} \sepand_{\idx_2} [Q]_\sim$. We have

\begin{align*}
[P]_{\sim} \sepand_{\idx_1} [Q]_\sim
&= [P \sepand_{\idx_1} Q]_{\sim} \\
&\leq [P \sepand_{\idx_2} Q]_{\sim} \tag{Since $P \sepand_{\idx_1} Q \leq P \sepand_{\idx_2} Q$} \\
&= [P]_{\sim} \sepand_{\idx_2} [Q]_{\sim}
\end{align*}

$P \vdash Q$ if and only if $[P]_{\sim} \leq [Q]_{\sim}$.

In the proof that the Lindenbaum-Tarski algebra indeed formed an $\idxset$-BI algebra, we already showed that $P \vdash Q$ implies $[P]_{\sim} \leq [Q]_{\sim}$. Consider the opposite direction. Then we have that $[P]_{\sim} \land [Q]_{\sim} = [P]_{\sim}$, hence $[P \land Q]_{\sim} = [P]_{\sim}$. This implies that $P \land Q \dashv\vdash P$.  Since $P \land Q \vdash Q$, by transitivity we have $P \vdash Q$.

If $\alginterp{P}_\valuation \leq \alginterp{Q}_\valuation$ for all $\valuation$, then $P \vdash Q$.

Consider the valuation $\valuation$ which maps $p \in \mathcal{AP}$ to $[p]_\sim$. Then $\alginterp{P}_\valuation = [P]_{\sim}$ and $\alginterp{Q}_\valuation = [Q]_{\sim}$. Hence we have
$[P]_{\sim} \leq [Q]_{\sim}$ which implies $P \vdash Q$.

§.§ $\idxset$-BI Frames

$\idxset$-BI formulas are interpreted on Down-Closed $\idxset$-BI frames.
We define a complex algebra on frames.

If $\mathcal{X}$ is an $\idxset$-BI frame, then the complex algebra of $\mathcal{X}$, written $\complex(\mathcal{X})$ is the structure $(\mathcal{P}_{\sqsubseteq}(X), \cap, \cup, \rightarrow_{\mathcal{X}}, X, \emptyset, \sepand_{\idx \in \idxset}, \sepimp_{\idx \in \idxset}, E_{\idx \in \idxset})$ where

\begin{align*}
\mathcal{P}_{\sqsubseteq}(X) &= \{ A \subseteq X \ | \ a \in A \land a \sqsubseteq b \rightarrow b \in A \} \\
A \rightarrow_{\mathcal{X}} B &= \{ a \ | \ \forall b.\, a \sqsubseteq b \land b \in A \rightarrow b \in B \} \\
A \sepand_{\idx} B &= \{ x \ | \ \exists w, y, z.\, w \sqsubseteq x \land w \in y \oplus_{\idx} z \land y \in A \land z \in B \} \\
A \sepimp_{\idx} B &= \{ x \ | \ \forall w, y, z.\, (x \sqsubseteq w \land z \in w \oplus_{\idx} y \land y \in A) \rightarrow z \in B \}
\end{align*}

If $\mathcal{X}$ is an $\idxset$-BI frame, then $\complex(\mathcal{X})$ is an $\idxset$-BI algebra.

Each $(X, \sqsubseteq, \oplus_\idx, E_{\idx})$ is a
BI frame. <cit.> shows that the complex of a BI frame is a
BI algebra. Thus the only thing to check is that the ordering on $\sepand$
respects the ordering on $\idxset$.  Let $\idx_1 \leq \idx_2$. We must show
that $A \sepand_{\idx_1} B \subseteq A \sepand_{\idx_2} B$. Let $x \in A
\sepand_{\idx_1} B$. Then there exists $w, y, z$ such that $w \sqsubseteq x$
and $w \in y \oplus_{\idx_1} z$, with $y \in A$ and $z \in B$.
by the Operation Inclusion property, we have that $w \in y \oplus_{\idx_2} z$, hence
$x \in A \sepand_{\idx_2} B$.

If $(L, \land, \lor)$ is a bounded distributive lattice, a prime filter on $F$ is a non-empty proper subset of $A$ such that:

* If $x \in F$ and $x \leq y $ then $y \in F$.

* If $x \in F$ and $y \in F$ then $x \land y \in F$.

* If $x \lor y \in F$ then $x \in F$ or $y \in F$.

We write $\prf(L)$ for the set of prime filters on $L$.

If $\mathcal{A}$ is an $\idxset$-BI algebra, then the prime filter $\idxset$-frame of $\mathcal{A}$ is defined as $\prf(\mathcal{A}) = (\prf(A), \subseteq, \oplus_{\idx \in \idxset}, E_{\idx \in \idxset})$

\begin{align*}
F_1 \oplus_{\idx} F_2 &= \{ F \in \prf(A) \ | \ \forall a_1 \in F_1.\, \forall a_2 \in F_2.\, a_1 \sepand_{\idx} a_2 \in F \} \\
E_{\idx} &= \{ F \in \prf(A) \ | \ \top^{\sepand}_{\idx} \in F \}
\end{align*}

If $\mathcal{A}$ is an $\idxset$-BI algebra, then $\prf(\mathcal{A})$ is an $\idxset$-BI frame.

<cit.> shows that for each $\idx \in \idxset$, $(\prf(A), \subseteq, \oplus_{\idx}, E_{\idx})$ is a BI frame. Therefore, we only need to check the Operation Inclusion property. Let $\idx_1 \leq \idx_2$
and let $F, G, H \in \prf(A)$ with $F \in G \oplus_{\idx_1} H$.
Let $a \in G$ and $b \in H$. Then $a \sepand_{\idx_1} b \in F$. Since $a \sepand_{\idx_1} b \leq a \sepand_{\idx_2} b$, and filters are upward-closed,
$a \sepand_{\idx_2} b \in F$, hence $F \in G \oplus_{\idx_2} H$.

Every $\idxset$-BI algebra is isomorphic to a subalgebra of a complex algebra. In particular, if $\mathcal{A}$ is an $\idxset$-BI algebra,
then the map $\theta : \mathcal{A} \rightarrow \complex(\prf(\mathcal{A}))$ defined as

\[ \theta(x) = \{ F \in \prf(\mathcal{A}) \ | \ x \in F \} \]

is an embedding.

<cit.> proves that for each $\idx \in \idxset$, this map $\theta$ is an embedding of $(A, \land, \lor, \rightarrow, \top, \bot, \sepand_{\idx}, \sepimp_{\idx}, \top^{\sepand}_{\idx})$ as a BI algebra into the complex algebra, viewed as a BI algebra for the operations indexed by $\idx$. Hence, $\theta$ is injective and a homomorphism with respect to all of the $\idxset$-BI algebra operations.

Let $\mathcal{A} = (A, \dots)$ be an $\idxset$-BI algebra and let $\valuation_{\textsf{a}} : \mathcal{AP} \rightarrow A$ be an interpretation of atomic propositions. Let $\mathcal{X} = (X, \dots)$ be an $\idxset$-BI frame and let $\valuation_{\textsf{f}} : \PROP \rightarrow \mathcal{P}(X)$ be a persistent valuation on $\mathcal{X}$. Let $\theta$ be the embedding from the previous result. Define the persistent valuation $\valuation_{\textsf{a}}' : \mathcal{AP} \rightarrow \mathcal{P}(\prf(A))$ and the interpretation $\valuation_{\textsf{f}}' : \mathcal{AP} \rightarrow \complex(\mathcal{X})$ by:

\begin{align*}
\valuation_{\textsf{a}}'(p) &= \theta(\valuation_{\textsf{a}}(p)) \\
\valuation_{\textsf{f}}'(p) &= \valuation_{\textsf{f}}(p) .
\end{align*}

Then we have

* $x \models_{\valuation_{\textsf{f}}} P$ if and only if $x \in \alginterp{P}_{\valuation_{\textsf{f}}'}$

* $F \models_{\valuation_{\textsf{a}}'} P$ if and only if $\alginterp{P}_{\valuation_{\textsf{a}}} \in F$ .

For the first part, we proceed by induction on $P$.

* Case $P = p$: We have:

\begin{align*}
x \models_{\valuation_{\textsf{f}}} p
& \lra x \in \valuation_{\textsf{f}}(p) \\
& \lra x \in \valuation_{\textsf{f'}}(p) \\
& \lra x \in \alginterp{p}_{\textsf{f'}}
\end{align*}

* Case $P = \top$: Then $x \models_{\valuation_{\textsf{f}}} \top$ holds for all $x$, and $\top$ in $\complex(\mathcal{X})$ is defined to be $X$, so $x \in \alginterp{\top}_{\valuation_{\textsf{f}}'}$ holds for all $x$.

* Case $P = \sepid_{\idx}$: Similar to $P = \top$.

* Case $P = \bot$: Similar to $P = \top$.

* Case $P = Q_1 \land Q_2$:

\begin{align*}
x \models_{\valuation_{\textsf{f}}} Q_1 \land Q_2
& \lra x \models_{\valuation_{\textsf{f}}} Q_1 \textrm{ and } x \models_{\valuation_{\textsf{f}}} Q_2  \tag{By satisfication rule}\\
& \lra x \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}} \textrm{ and } x \in \alginterp{Q_2}_{\valuation_{\textsf{f}'}} \tag{$\valuation_{\textsf{f}'}$ and $\valuation_{\textsf{f}'}$ the same} \\
& \lra x \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}} \cap \alginterp{Q_2}_{\valuation_{\textsf{f}'}} \\
& \lra x \in \alginterp{Q_1 \land Q_2}_{\valuation_{\textsf{f}'}} \tag{By the $\land$ operation in Complex algebra and the recursive definition of $\valuation$}
\end{align*}

* Case $P = Q_1 \lor Q_2$:

\begin{align*}
x \models_{\valuation_{\textsf{f}}} Q_1 \lor Q_2
& \lra x \models_{\valuation_{\textsf{f}}} Q_1 \textrm{ or } x \models_{\valuation_{\textsf{f}}} Q_2 \\
& \lra x \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}} \textrm{ or } x \in \alginterp{Q_2}_{\valuation_{\textsf{f}'}} \\
& \lra x \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}} \cup \alginterp{Q_2}_{\valuation_{\textsf{f}'}} \\
& \lra x \in \alginterp{Q_1 \lor Q_2}_{\valuation_{\textsf{f}'}}
\end{align*}

* Case $P = Q_1 \rightarrow Q_2$: Let $x \models_{\valuation_{\textsf{f}}} Q_1 \rightarrow Q_2$. Then, for all $y$ such that $x \sqsubseteq y$,
if $y \models_{\valuation_{\textsf{f}}} Q_1$, then $y \models_{\valuation_{\textsf{f}}} Q_2$. Applying the induction hypothesis, we have that for all $y$ such that $x \sqsubseteq y$,
if $y \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}}$, then
$y \in \alginterp{Q_2}_{\valuation_{\textsf{f}'}}$.
Hence, $x \in \alginterp{Q_1 \rightarrow Q_2}_{\valuation_{\textsf{f}'}}$. The reverse direction is similar.

* Case $P = Q_1 \sepand_{\idx} Q_2$: Let $x \models_{\valuation_{\textsf{f}}} Q_1 \sepand_{\idx} Q_2$. Then there exists $x'$, $y$, and $z$ such that $x' \sqsubseteq x$ and $x' \in y \oplus_{\idx} z$, where $y \models_{\valuation_{\textsf{f}}} Q_1$ and $z \models_{\valuation_{\textsf{f}}} Q_2$. By the induction hypothesis, we have that $y \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}}$ and $z \in \alginterp{Q_2}_{\valuation_{\textsf{f}'}}$. Hence, $x \in \alginterp{Q_1 \sepand_{\idx} Q_2}_{\valuation_{\textsf{f}'}}$.

* Case $P = Q_1 \sepimp_{\idx} Q_2$: Let $ x \models_{\valuation_{\textsf{f}}} Q_1 \sepimp_{\idx} Q_2$. Then for all $x'$, $y$, and $z$ such that $x \sqsubseteq x'$ and $z \in x' \oplus_{\idx} y$, if $y \models_{\valuation_{\textsf{f}}} Q_1$,  then $z \models_{\valuation_{\textsf{f}}} Q_2$.

To show that $x \in \alginterp{Q_1 \sepimp_{\idx} Q_2}_{\valuation_{\textsf{f}'}}$, let $w$, $y$, and $z$ be such that $x \sqsubseteq w$, $z \in w \oplus_{\idx} y$, and $y \in \alginterp{Q_1}_{\valuation_{\textsf{f}'}}$. We must show that $z \in \alginterp{Q_2}_{\valuation_{\textsf{f}'}}$. Applying the induction hypothesis, we have that $y \in \models_{\valuation_{\textsf{f}}} Q_1$. Thus, by the preceding paragraph, we have that $z \models_{\valuation_{\textsf{f}}} Q_2$. Applying the induction hypothesis again, we get that $z \in \alginterp{Q_2}_{\valuation_{\textsf{f}'}}$.

For the second part, assuming $F \in \prf(\mathcal{A})$,
then for any $P$, we have

\begin{align*}
F \models_{\valuation_{\textsf{a}}'} P
& \lra F \in \valuation_{\textsf{a}'}(P) \\
& \lra F \in  \prf(\mathcal{A}) \text{ and } \valuation_{\textsf{a}}(P) \in F \\
& \lra \valuation_{\textsf{a}}(P) \in F \\
& \lra \alginterp{P}_{\valuation_{\textsf{a}}} \in F .
\end{align*}

If $P \models_\valuation Q$ for all $\valuation$, then $P \vdash Q$

Suppose $P \not\vdash Q$. Then by algebraic completeness, there exists some
$\idxset$-BI algebra $\mathcal{A}$ and an interpretation
$\valuation_{\textsf{a}}$ such that $ \alginterp{P}_{\valuation_{\textsf{a}}}
\nleq \alginterp{Q}_{\valuation_{\textsf{a}}}$. By the prime filter theorem,
there exists <cit.> a prime filter $F$ such that $\alginterp{P}_{\valuation_{\textsf{a}}} \in F$
and $\alginterp{Q}_{\valuation_{\textsf{a}}} \not\in F$. Let $\valuation_{\textsf{a}}'$ be as in the previous theorem, then we have
$F \models_{\valuation_{\textsf{a}}'} P$ and $F \not\models_{\valuation_{\textsf{a}}'} Q$ which contradicts the assumption that $P \models_{\valuation_{\textsf{a}}'} Q$.

§ EXAMPLES: OMITTED DETAILS

§.§ Bound false positive rate in Bloom filter

One detail we omitted is that, since the first line of the program Bloom,
$bloom$ has been kept as a bit-array throughout, i.e.,
all its entries are either 0 or 1. So it is easy to prove that

\[
\hoare{\top}{\textsc{Bloom}}
{\bigwedge_{\beta = 0}^{N}(bloom[\beta] = 0 \lor bloom[\beta] = 1 )}.
\]

Then, by the conjunction rule Conj, we have

\begin{align*}
\hoare{\top}{\textsc{Bloom}}
{\Pr \left[\sum_{\beta = 0}^N bloom[\beta] < K + T(\delta, N) \right] \geq 1 - \delta },
\end{align*}

where $K = \EE\left[\sum_{\beta = 0}^N bloom[\beta]\right]$.

In the following, we will abbreviate formulas that assert
$b$ is a bit-array where exactly $J$ of its first $N$ entries
are one,

\[
\left( \sum_{\beta = 0}^N b[\beta] = J \right) \land
\bigwedge_{\beta = 0}^{N}(b[\beta] = 0 \lor b[\beta] = 1),
\]

as $\bv{b}{J}{N}$.
Similarly, we will use $\bv{b}{< J}{N}$ to abbreviate

\[
\left( \sum_{\beta = 0}^N b[\beta] < J \right) \land \bigwedge_{\beta =
0}^{N}(b[\beta] = 0 \lor b[\beta] = 1).
\]

Now we restate our goal as

\begin{align*}
\hoare{\bv{bloom}{< K}{N}}{\CheckMem}{\Pr[allhit] \leq(K/N)^H}.
\end{align*}

first initializes $h$ and $allhit$ deterministically to 1.
Then, using RAssn and Frame, we can show that

\[
\vdash \hoare{\top}
{\Assn{h}{0}; \Assn{allhit}{1}}
{\left( \apEq{h}{0} \right) \sepand \left( \apEq{allhit}{1} \right)}.
\]

Using the (<ref>) axiom and the fact that $1 \leq (K/N)^0$ for any $K$ and $N$,
we can show $\models \left( \apEq{h}{0} \right) \sepand \left( \apEq{allhit}{1} \right)
\to \Pr[allhit] \leq (K/N)^h$.

\[
\vdash \hoare{\top}
{\Assn{h}{0}; \Assn{allhit}{1}}
{\Pr[allhit] \leq (K/N)^h}.
\]

Because the assignments $\Assn{h}{0}; \Assn{allhit}{1}$ do not modify the
Bloom filter array $bloom$, we can then apply the frame rule Frame to

\begin{align}
\label{eq:ex:checkmem:init}
\vdash \hoare{\bv{bloom}{< K}{N}}
{\bv{bloom}{< K}{N} \sepand \Pr[allhit] \leq (K/N)^h}.
\end{align}

We will abbreviate $\bv{bloom}{< K}{N} \sepand \Pr[allhit] \leq (K/N)^h$ as $\eta$.
Because $\sum_{\beta = 0}^N b[\beta]$ is an integer upper bounded by $N$,

\[
\models_{\Mem} \eta \to \bigvee_{0 \leq J < K} \eta_J,
\]

where $\eta_J$ abbreviates $J < K \land \left(
\bv{bloom}{J}{N} \sepand \Pr[allhit] \leq (K/N)^h \right)$.

We will then prove that for each $J$, the formula $\eta_J$
is a loop invariant of 's loop body.

The loop body first uniformly sample an element from $[N]$,
so by RSamp${}^*$,

\begin{align}
\eta_J \sepand \apUnif{bin}{[N]} .
\label{eq:ex:checkmem:loop1}
\end{align}

Together with the axiom $\models P \sepand Q \to P$, <Ref>

\[
J < K \land \left(\bv{bloom}{J}{N} \sepand \left( \Pr[allhit] \leq
(\frac{K}{N})^h \right) \sepand \apUnif{bin}{[N]} \right).
\]

Then, $hit$ gets assigned to $bloom[bin]$, so by RAssn, we have

\[
\hoare{ \bv{bloom}{J}{N} \sepand \apUnif{bin}{[N]}
}{\Assn{hit}{bloom[\beta]}}{ \left( \bv{bloom}{J}{N} \sepand \apUnif{bin}{[N]}
\right) \land \apEq{hit}{bloom[bin]}}.
\]

Since the array $bloom$ only contains zero-one entries, when the sum of its entries is $J$,
an entry $bloom[bin]$ drawn uniformly at random has probability $\frac{J}{N}$ to be 1.
If the entry is in addition chosen independently from values in $bloom$,
then the bit $bloom[bin]$ is distributed independent from the distribution of $bloom$.
The (<ref>) axiom encodes this fact:

\[
\models \left( \left( \bv{b}{J}{N} \sepand  \apUnif{x}{[N]} \right)
\land \apEq{hit}{b[x]} \right)
\to \apBern{hit}{\frac{J}{N}}\sepand \bv{b}{J}{N} .
\]

Thus, we have

\[
\hoare{ \bv{bloom}{J}{N} \sepand \apUnif{bin}{[N]}
}{\Assn{hit}{bloom[\beta]}}{\apBern{hit}{\frac{J}{N}} \sepand
\bv{bloom}{J}{N} }.
\]

Because $\Assn{hit}{bloom[bin]}$ does not modify $allhit$, we
can apply the frame rule for $\sepand$ Frame and get

\begin{align*}
&	\left\{ \bv{bloom}{J}{N} \sepand \apUnif{bin}{[N]} \sepand \Pr[allhit] \leq \left(\frac{K}{N}\right)^h \right\}\\
& \quad\quad\quad\quad\quad\quad \Assn{hit}{bloom[\beta]}\\
& \left\{ \apBern{hit}{\frac{J}{N}} \sepand \bv{bloom}{J}{N} \sepand  \Pr[allhit] \leq \left(\frac{K}{N}\right)^h \right\}.
\end{align*}

Next, with the assignment $\Assn{allhit}{hit \mathop{\&\&} allhit}$,
by applying the axioms (<ref>), (<ref>)
and the RAssn rule,
we get:

\begin{align*}
&\left\{ \apBern{hit}{\frac{J}{N}} \sepand \bv{bloom}{J}{N} \sepand  \Pr[allhit] \leq \left(\frac{K}{N}\right)^h\right\} \\
& \quad\quad\quad\quad\quad \Assn{allhit}{hit \mathop{\&\&} allhit}\\
&\left\{ \left(\Pr[allhit] \leq \frac{J}{N} \cdot \left(\frac{K}{N}\right)^h \right) \sepand \bv{bloom}{J}{N}\right\}
\end{align*}

We can then apply the rule of constancy Const and get

\begin{align*}
&	\left\{ J < K \land \left( \bv{bloom}{J}{N} \sepand \apUnif{bin}{[N]} \sepand \Pr[allhit] \leq \left(\frac{K}{N}\right)^h \right)\right\}\\
&  \quad\quad\quad\quad \Assn{hit}{bloom[\beta]}; \Assn{allhit}{hit \mathop{\&\&} allhit}\\
&\left\{ J < K \land \left( \left(\Pr[allhit] \leq \frac{J}{N} \cdot \left(\frac{K}{N}\right)^h \right) \sepand \bv{bloom}{J}{N}\right) \right\}
\end{align*}

When we have $J <  K$, then $ (K/N)^h \cdot \frac{J}{N}  \leq  (K/N)^{h+1}$, so the post condition

\[
J < K \land \left( \left(\Pr[allhit] \leq  \left(\frac{K}{N}\right)^{h + 1} \right) \sepand \bv{bloom}{J}{N}\right)
\]

The last step in the loop body is the assignment $\Assn{h}{h + 1}$.
By the deterministic assignment rule DAssn,
we can establish the post condition $\eta_J$ afterwards:

\[
J < K \land \left(\bv{bloom}{J}{N} \sepand \Pr[allhit] \leq \left(\frac{K}{N}\right)^h \right).
\]

Thus, we have $\hoare{\eta_J}{\textit{loop body}}{\eta_J}$

By Loop rule, we can establish $\hoare{\eta_J}{loop}{\eta_J \land h \geq H}$.
Since $\eta_J \land h \geq H$ implies $\Pr[allhit] \leq (K/N)^H $, we then have

\[
\hoare{\eta_J}{loop}{\Pr[allhit] \leq \left(\frac{K}{N}\right)^H}.
\]

Because $\Pr[allhit] \leq (K/N)^H$ is closed under mixtures,
and $\eta$ is closed under conditioning, we can then apply RCase to prove that

\begin{align}
\label{eq:ex:checkmem:loop}
\hoare{\eta}{loop}{ \Pr[allhit] \leq \left(\frac{K}{N}\right)^H}.
\end{align}

Using the Seqn rule to combine the proved judgments for 's
initialization (<ref>) and loop (<ref>), we derive

\begin{align*}
\hoare{\sum_{\beta = 0}^N bloom[\beta] < K}{\CheckMem}{\Pr[allhit] \leq \left(\frac{K}{N}\right)^H}.
\end{align*}

§.§ Permutation Hashing

We sketch how to replicate the informal reasoning in . For the main
loop, we apply the rule Loop with the following loop invariant:

\[
\bigwedge_{\alpha = 0}^n \apEq{hitZ[\alpha]}{[mod(g[\alpha], B) = Z]}
\land \apPerm{g}{[B \cdot K]}
\land ct = \sum_{\alpha = 0}^n hitZ[\alpha]
\land (\neg (n < N) \to \apEq{n}{N})
\]

The loop invariant is preserved by the body of the loop, using the assignment
rule (RAssn) and the rule of constancy (Const). Thus we can
show the following judgment:

\[
\hoare{\apEq{ct}{0} \land \apEq{n}{0}}{loop}{%
\bigwedge_{\alpha = 0}^N \apEq{hitZ[\alpha]}{[mod(g[\alpha], B) = Z]}
\land \apPerm{g}{[B \cdot K]}
\land \apEq{ct}{\sum_{\alpha = 0}^N hitZ[\alpha]}}
\]

Applying (<ref>), the post-condition implies:

\[
\bigwedge_{\alpha = 0}^N \apEq{hitZ[\alpha]}{[mod(g[\alpha], B) = Z]}
\land \bigsep_{\alpha = 0}^N \apDist{hitZ[\alpha]}
\land \apPerm{g}{[B \cdot K]}
\land \apEq{ct}{\sum_{\alpha = 0}^N hitZ[\alpha]}
\]

Applying basic axioms about expected value and the permutation distribution
((<ref>) (<ref>) (<ref>)), we have:

\[
\bigsep_{\alpha = 0}^N \apDist{hitZ[\alpha]}
\land \apEq{ct}{\sum_{\alpha = 0}^N hitZ[\alpha]}
\land \apEq{\EE[ct]}{N / B}
\]

And we can apply the negative-association Chernoff bound (<ref>)
to conclude:

\[
\hoare{\top}
{\Pr [ |ct - N / B| > T(\beta, N) ] < \beta}
\]

This conclusion corresponds to Proposition A.2 in
<cit.> algorithm for fast set
<cit.> apply a variant of the Chernoff bound to
obtain a multiplicative, rather than an additive, error guarantee. We present
the additive version since the bound is a bit simpler, but there is no
difficulty to handling the multiplicative version in our framework.]

§.§ Fully-Dynamic Dictionary

We outline the main steps in the formal proof; the most interesting step is the
last one, where we use negative association, but all steps can be handled in our

We will refer to the two outer-most loops as (1) and (2), the next two
outer-most loops as (1.1) and (2.1), and the inner-most loop as (1.1.1).

*Computing $\EE[binCt[c][p]]$.
For loop (1), we apply Loop with the following loop invariant:

\[
\bigwedge_{\gamma = 0}^C \bigwedge_{\beta = 0}^P
\apEq{\EE[binCt[\gamma][\beta]]}{n / (P \cdot C)}
\land ( \neg (n < N) \to \apEq{n}{N} ) .
\]

To show that this invariant is preserved by the loop, by two applications of
RSamp* the following holds after the sampling commands:

\[
\apOnehot{pocket[n]}{[P]} \indand \apOnehot{crate[n]}{[C]}
\land \apEq{bin[n]}{crate[n]^\top \cdot pocket[n]} .
\]

Using an axiom about independence and products of one-hot vectors
(<ref>), this implies:

\[
\apOnehot{bin[n]}{[C] \times [P]} .
\]

Using an axiom about the one-hot encoding (<ref>):

\[
\apEq{\mathbb{E}[bin[\alpha][\gamma][\beta]]}{1/(P \cdot C)}
\]

for every $\alpha$, $\gamma$, and $\beta$. Standard loop invariants for loop
(1.1) and (1.1.1) show that:

\[
\apEq{binCt[c][p]}{\sum_{\alpha = 0}^n bin[\alpha][c][p]} ,
\]

and linearity of expectation establishes the invariant condition for loop (1).
The invariant holds at the start of loop (1) since $binCt$ is zero-initialized,
and it also holds at the end of loop (1). Since $binCt$ is not modified further,
the expectation bound also holds at the end of the program (Const).

*Bounding $\Pr[binCt[c][p] > T_{bin}]$.
For loop (1), we apply Loop with the following loop invariant:

\[
\left( \bigind_{\alpha = 0}^n \apDist{bin[\alpha]} \right)
\land
\bigwedge_{\gamma = 0}^C \bigwedge_{\beta = 0}^P
\apEq{binCt[\gamma][\beta]}{\sum_{\alpha = 0}^N bin[\alpha][\gamma][\beta]}
\land ( \neg (n < N) \to \apEq{n}{N} ) .
\]

The first conjunction is an invariant, by applying the sampling rule
Samp* and the independence frame rule Frame from PSL. The rest
of the invariant is preserved, following standard invariants for loops (1.1) and
(1.1.1). By projection (<ref>), at the end of loop (1) we can

\[
\bigwedge_{\gamma = 0}^C \bigwedge_{\beta = 0}^P
\left( \bigind_{\alpha = 0}^N \apDist{bin[\alpha][\gamma][\beta]} \right)
\land \apEq{binCt[\gamma][\beta]}{\sum_{\alpha = 0}^N bin[\alpha][\gamma][\beta]} .
\]

Thus a (standard) Chernoff bound gives:

\[
\bigwedge_{\gamma = 0}^C \bigwedge_{\beta = 0}^P
\Pr [ binCt[\gamma][\beta] > \EE[binCt[\gamma][\beta]] + T(\rho_{bin}, N) ] \leq \rho_{bin} .
\]

where $\EE[binCt[\gamma][\beta]]$ is $N/(P \cdot C)$ by the previous step.
Again, property holds until the end of the program since $binCt$ is not modified
further (Const).

*Bounding $\EE[overCt[c]]$.

Using standard loop invariants, at the end of loop (2) we have:

\[
\bigwedge_{\gamma = 0}^C
\apEq{overCt[\gamma]}{\sum_{\beta = 0}^P \sum_{\delta = 0}^C bin[\delta][\beta]}
\land \bigwedge_{\beta = 0}^P \apEq{over[\gamma][\beta]}{[binCt[\gamma][\beta] > T_{bin}]} .
\]

Using linearity of expectation and the fact that $over[\gamma][\beta]$ is either
zero or one, we have:

\[
\EE[overCt[\gamma]]
\sim \sum_{\beta = 0}^P \mathbb{E}[over[\gamma][\beta]]
\sim \sum_{\beta = 0}^P \Pr[over[\gamma][\beta] = 1]
\sim \sum_{\beta = 0}^P \Pr[binCt[\gamma][\beta] > T_{bin}]
\leq P \cdot \rho_{bin}
\]

since we have bound the probability in the previous step.

*Bounding $\Pr[overCt[c] > T_{over}]$.

We want the following loop invariant for (1):

\[
\bigwedge_{\gamma = 0}^C \bigwedge_{\beta = 0}^P \bigneg_{\beta = 0}^P \apDist{binCt[\gamma][\beta]}
\land
( \neg(n < N) \to \apEq{n}{N} ) .
\]

We want the following loop invariant for (1.1):

\[
\bigwedge_{\gamma = 0}^C
\bigneg_{\beta = 0}^P \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = c}^P \apDist{bin[n][\gamma][\beta]}
\land
( \neg(p < P) \to \apEq{p}{P} ) .
\]

And the following loop invariant for (1.1.1):

\[
\bigwedge_{\gamma = 0}^C
\bigneg_{\beta = 0}^P \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + [c > \gamma]}^P \apDist{bin[n][\gamma][\beta]} .
\]

We show the invariant post-conditions for a fixed $\gamma$; the big conjunction
then follows by applying Conj. Working from inside-to-outside, we start
with loop (1.1.1). To establish the invariant condition, the critical case is $c
= \gamma$. We can pull out:

\[
\bigneg_{\beta = 0}^p \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + 1}^P \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + 1}^P \apDist{bin[n][\gamma][\beta]}
\negand
\underbrace{
\apDist{binCt[\gamma][p]}
\negand
\apDist{bin[n][\gamma][p]}
\]

Now, we can use the assignment rule to show:

\[
\hoare{\Phi}{\Assn{upd}{binCt[c][p] + bin[n][c][p]}}{\apEq{upd}{binCt[c][p] + bin[n][c][p]}}
\]

Since addition is a monotone function, the NA frame rule (NegFrame)

\[
\bigneg_{\beta = 0}^p \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + 1}^P \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + 1}^P \apDist{bin[n][\gamma][\beta]}
\negand
\apDist{upd}
\]

after the assignment to $upd$. After the assignment to $bin[c][p]$, we can fold:

\[
\bigneg_{\beta = 0}^P \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + 1}^P \apDist{bin[n][\gamma][\beta]}
\]

to establish the invariant for loop (1.1.1).

To establish the invariant for loop (1.1), when the inner-most loop (1.1.1)
terminates we have $c > \gamma$, and so we have:

\[
\bigneg_{\beta = 0}^P \apDist{binCt[\gamma][\beta]}
\negand
\bigneg_{\beta = p + 1}^P \apDist{bin[n][\gamma][\beta]} .
\]

To establish the invariant for loop (1), note that the invariant for loop (1.1)
holds on loop entry since $z$ is zero-initialized (<ref>). And the
loop invariant for loop (1) is established when loop (1.1) exits, when $p = P$.

Next, we tackle loop (2). We take the invariant:

\[
\bigwedge_{\gamma = 0}^C
\bigneg_{\beta = 0}^p \apDist{over[\gamma][\beta]}
\negand
\bigneg_{\beta = p}^P \apDist{binCt[\gamma][\beta]} .
\]

For the inner loop (2.1), we take the invariant:

\[
\bigwedge_{\gamma = 0}^C
\bigneg_{\beta = 0}^{p + [c > \gamma]} \apDist{over[\gamma][\beta]}
\negand \bigneg_{\beta = p + [c > \gamma]}^P \apDist{binCt[\gamma][\beta]} .
\]

Again, we show the invariant post-conditions for a fixed $\gamma$.  For the
critical iteration $c = \gamma$, we again isolate $binCt[\gamma][p]$, observe
that addition is monotone and the function $[binCt[c][p] > T_{bin}]$ is monotone in
$binCt[\gamma][p]$, and apply the NA frame rule (NegFrame).

Finally at the end of the program, we can show:

\[
\bigneg_{\beta = 0}^P \apDist{over[\gamma][\beta]}
\]

along with the regular invariant

\[
\apEq{overCt[\gamma]}{\sum_{\beta = 0}^P over[\gamma][\beta]} .
\]

We can then apply the negative-dependence Chernoff bound (<ref>):

\[
\Pr [ overCt[\gamma] > \EE[overCt[\gamma]] + T(\rho_{over}, P) ] \leq \rho_{over} .
\]

Using the expectation bound from the previous step and putting everything
together, we conclude:

\[
\hoare{\top}
{\bigwedge_{\gamma = 0}^C \Pr [ overCt[\gamma] > P \cdot \rho_{bin} + T(\rho_{over}, P) ] \leq \rho_{over}} ,
\]

thus showing a high-probability upper-bound on the number of overfull pocket
dictionaries within each crate.

§.§ Repeated Balls-into-Bins

We will refer to the loops in <Ref> using the same scheme we
used before: the outer-most loop is loop (1), the three next-outer-most loops
are loops (1.1), (1.2), and (1.3), and the inner-most loop is loop (1.2.1).
Starting from the outside, we take the following invariant for loop (1):

\[
\Pr\left[ \bigvee_{\beta = 0}^r (emptyCt[\beta] > T_{empty}) \right] \leq r \cdot \rho_{empty}
\land \apEq{\sum_{\alpha = 0}^N ct[\alpha]}{N}
\]

Showing the invariant condition requires some work. First, note that:

\[
\models_\Mem \apEq{\sum_{\alpha = 0}^N ct[\alpha]}{N}
\to \bigvee_{\sigma : [N] \to [N]} \bigwedge_{\alpha = 0}^N
\apEq{ct[\alpha]}{|\sigma^{-1}(\alpha)|}
\]

where $\sigma : [N] \to [N]$ ranges over all assignments of $N$ balls to $N$
bins, and where we write $\models_\Mem$ to denote that the formula is valid in
all memories, rather than distributions over memories. We write
$\tau(\alpha) = |\sigma^{-1}(\alpha)|$ for the number of balls in bin $\alpha$.
We will show:

\[
\hoare{\bigwedge_{\alpha = 0}^N \apEq{ct[\alpha]}{\tau(\alpha)} }
{\Pr\left[ emptyCt[r] < T_{empty} \right] \leq \rho_{empty}}
\]

where $body$ is the body of loop (1). For loop (1.1), it is straightforward to
show the invariant using the loop rule Loop:

\[
\bigwedge_{\alpha = n}^N (\apEq{ct[\alpha]}{\tau(\alpha)})
\land \bigwedge_{\alpha = 0}^n (\apEq{ct[\alpha]}{\tau(\alpha)- [\tau(\alpha) > 0]})
\land \apEq{rem}{\sum_{\alpha = 0}^n [\sigma(\alpha) > 0]}
\land ( \neg(n < N) \to \apEq{n}{N} )
\]

At the exit of loop (1.1), we have:

\[
\bigneg_{\alpha = 0}^N \apDist{ct[\alpha]}
\]

since counts are all equal to expressions of logical variables, so conditioning
on the logical variables, they are all deterministic; we take this formula to be
the invariant for loop (1.2). Note that the loop guard is not deterministic,
since the value of $rem$ is randomized. However, under our conditioning,
$rem$ is deterministic under our conditioning since it is fully determined by
the initial counts (i.e., it is the number of buckets that are initially
non-empty). Hence, we may apply the loop rule Loop, treating the loop
guard as deterministic. This is the power of reasoning under conditioning.

Now to establish the invariant for loop (1.2), we reason much as in the previous
examples. The sampling rule Samp* gives:

\[
\bigneg_{\alpha = 0}^N \apDist{ct[\alpha]} \indand \apDist{bin[j]}
\]

By negative association for one-hot encoding (<ref>):

\[
\bigneg_{\alpha = 0}^N \apDist{ct[\alpha]} \indand \bigneg_{\alpha = 0}^N \apDist{bin[j][\alpha]}
\]

This implies:

\[
\bigneg_{\alpha = 0}^N \apDist{ct[\alpha]} \negand \bigneg_{\alpha = 0}^N \apDist{bin[j][\alpha]}
\]

For the inner-most loop (1.2.1), we apply the same technique as for loop (1.2).
Since loop (1.2) has a randomized guard, $k$ is a random variable and loop
(1.2.1) also has a randomized guard. However, under the conditioning, we may
assume that $k$ is deterministic and apply Loop on loop (1.2.1) with
the following invariant:

\[
\bigneg_{\alpha = 0}^k \apDist{ct[\alpha]}
\negand \left(\apDist{ct[k]} \negand \bigneg_{\alpha = k}^N \apDist{bin[j][\alpha]}\right)
\negand \bigneg_{\alpha = k + 1}^N \apDist{ct[\alpha]}
\land (\neg (k < N) \to \apEq{k}{N})
\]

Like in earlier examples, we can establish this invariant using the negative
dependence frame rule since $ct[n] + bin[j][n]$ is monotone. Thus at exit of
loop (1.2.1), we have:

\[
\bigneg_{\alpha = 0}^N \apDist{ct[\alpha]}
\]

Next, three applications of the assignment rule RAssn give:

\[
\bigneg_{\alpha = 0}^N \apDist{ct[\alpha]}
\land \apEq{n}{0}
\land \apEq{emptyCt[r]}{0}
\land \apEq{empty}{isZero(ct)}
\]

The function $isZero(v)$ takes a vector of numbers $v$, and returns a vector
where each index $i$ $1$ if $v[i]$ is zero, else it holds $0$. This is an
antitone function: it is non-increasing in its argument. Thus, the monotone
mapping axiom (<ref>) gives:

\[
\bigneg_{\alpha = 0}^N \apDist{empty[\alpha]}
\]

Then, a standard loop invariant for loop (1.3) gives:

\[
\bigneg_{\alpha = 0}^N \apDist{empty[\alpha]}
\land \apEq{emptyCt[r]}{\sum_{\alpha = 0}^N empty[\alpha]}
\]

Now, we are in position to apply the negative association Chernoff bound
(<ref>), giving the judgment:

\[
\hoare{\bigwedge_{\alpha = 0}^N \apEq{ct[\alpha]}{\tau(\alpha)}}
{ \Pr [ emptyCt[r] < \EE[emptyCt[r]] - T(\rho_{empty}, N) ] \leq \rho_{empty} }
\]

where $body$ is the body of loop (1). However, we are not yet done. We want
to combine these judgments—one for each map $\sigma : [N] \to [N]$—using the
randomized case analysis rule RCase

We can take the trivial pre-condition $\phi = \top$, and the case condition:

\[
\eta = \bigwedge_{\alpha = 0}^N \apEq{ct[\alpha]}{\tau(\alpha)}
\]

Since $\eta$ asserts that the equality holds with probability $1$, it is closed
under conditioning. However, our post-condition has a problem: it mentions the
expected value $\EE[emptyCt[r]]$, which may not be preserved under mixtures, so
the entire assertion is not CM. However, translating an argument by <cit.> into our logic gives:

\[
\hoare{\bigwedge_{\alpha = 0}^N \apEq{ct[\alpha]}{\tau(\alpha)}}
{ \EE[emptyCt[r]] \geq N/15 }
\]

assuming that $N \geq 2$. The argument makes use of basic properties of expected
values and the exponential function; we omit the details. Thus, we have:

\[
\hoare{\bigwedge_{\alpha = 0}^N \apEq{ct[\alpha]}{\tau(\alpha)}}
{ \Pr [ emptyCt[r] < N/15 - T(\rho_{empty}, N) ] \leq \rho_{empty} }
\]

and the post-condition is now a CM assertion. Applying RCase, we have:

\[
\hoare{\sum_{\alpha = 0}^N \apEq{ct[\alpha]}{N}}
{ \Pr [ emptyCt[r] < N/15 - T(\rho_{empty}, N) ] \leq \rho_{empty} }
\]

Recalling that we wanted the following invariant for loop (1):

\[
\Pr\left[ \bigvee_{\beta = 0}^r (emptyCt[\beta] < T_{empty}) \right] \leq r \cdot \rho_{empty}
\land \sum_{\alpha = 0}^N \apEq{ct[\alpha]}{N}
\]

we can use the rule of constancy Const and the assignment rule
RAssn to preserve the first conjunct to show:

\[
\Pr\left[ \bigvee_{\beta = 0}^{r-1} (emptyCt[\beta] < T_{empty}) \right] \leq (r - 1) \cdot \rho_{empty}
\]

at the end of the body of loop (1). Combined with the probability bound for
$emptyCt[r]$, an application of the union bound (<ref>) establishes
the invariant for loop (1). Putting everything together, we have:

\[
\hoare{N \geq 2 \land \sum_{\alpha = 0}^N \apEq{ct[\alpha]}{N}}
\Pr\left[ \bigvee_{\beta = 0}^R (emptyCt[\beta] < N/15 - T(\rho_{empty}, N)) \right] \leq R \cdot \rho_{empty}
\]

analogous to <cit.>.

§.§ Axioms for Examples

For completeness, we present the probability-related axioms that we need for the
examples. For simplicity we present the axioms in binary form, though most
extend directly to big operations.

* Linearity of expectation. Let $e, f$ be bounded expressions.

\begin{equation} \label{ax:lin:exp}
\models \apEq{\EE[\alpha \cdot e + \beta \cdot f]}{\alpha \cdot \EE[e] + \beta \cdot \EE[f]}
\tag{LinExp}
\end{equation}

* Union bound. Let $ev_1, ev_2 \in \Event$,

\begin{equation} \label{ax:union:bd}
\models \Pr [ ev_1 \lor ev_2 ] \leq \Pr [ ev_1 ] + \ Pr [ ev_2 ]
\tag{UnionBd}
\end{equation}

* Permutation marginal. Let $x$ be an array variable, and let $S$ be a
finite set.

\begin{equation} \label{ax:perm:marg}
\models \apPerm{x}{S} \to \apUnif{x[\alpha]}{S}
\tag{PermMarg}
\end{equation}

* Expectation Indicator. Let $e$ be a 0/1 valued expression,

\begin{equation} \label{ax:expect:ind}
\models \apEq{\EE[ e ]}{\Pr[e = 1]}
\tag{ExpectInd}
\end{equation}

* Bernoulli variables probabilities. Let $e$ be an expression,

\begin{equation} \label{ax:bernoulli:p}
\models \apBern{e}{p} \to \Pr[e = 1] = p
\tag{BernProb}
\end{equation}

* Probability of uniform. Let $S$ be a finite set.

\begin{equation} \label{ax:prob:unif}
\models \apEq{\Pr[ \apUnif{x}{S} = \alpha ]}{1/|S|}
\tag{ProbUnif}
\end{equation}

* Bijection uniform. Let $S$ be a finite set, and let $f : S
\to S$ be a bijection.

\begin{equation} \label{ax:biject:unif}
\models \apUnif{x}{S} \to \apUnif{f(x)}{S}
\tag{BijectUnif}
\end{equation}

* One-hot marginal. Let $x$ be an array variable.

\begin{equation} \label{ax:oh:marg}
\models \apOnehot{x}{S} \to \apUnif{x[\alpha]}{S}
\tag{OHMarg}
\end{equation}

* Independent product one-hot.

\begin{equation} \label{ax:ind:prod:oh}
\models \apOnehot{x}{[M]} \indand \apOnehot{y}{[N]} \to \apOnehot{x^\top \cdot y}{[M] \times [N]}
\tag{IndProdOH}
\end{equation}

* Independent map. Let $x$ be an array variable of length $N$.

\begin{equation} \label{ax:ind:map}
\models \bigind_{\alpha = 0}^N \apDist{x[\alpha]}
\to \bigind_{\alpha = 0}^N \apDist{f(x[\alpha])}
\tag{IndMap}
\end{equation}

* Deterministic independent. Let $x$ be a variable.

\begin{equation} \label{ax:det:ind}
\models \apDetm{x} \to \apDist{x} \indand \apDist{e}
\tag{DetInd}
\end{equation}

* Events happen only if they have probability one. Let $ev \in \Event$,

\begin{equation} \label{ax:prob:one}
\models \apEvent{ev} \to \Pr(ev) = 1
\tag{ProbOne}
\end{equation}

* Uniform sampling from a population.
We represent a population as a bit-vector, where each entry is an individual
and 1 indicates they have some feature and 0 indicates not. Then, if we
uniformly sample from the population,  the probability of getting a one is
equal to population-level ratio of ones, regardless how they are distributed
in the population. Let $N \geq J$ be constants or logical variables, $b$ be an
array variable of length $N$, and $x, hit$ be variables:

\begin{equation} \label{ax:unif:samp}
\models \left( \left( \bv{b}{J}{N} \sepand  \apUnif{x}{[N]} \right) \land
\apEq{hit}{b[x]} \right) \to \apBern{\frac{J}{N}}{hit}\sepand\left(
\sum_{\beta = 0}^N b[\beta] = J \right).
\tag{UniformSamp}
\end{equation}

* Independent product probabilities. Let $ev_1, ev_2 \in \Event$ ,
$J, K$ be two real numbers,

\begin{equation} \label{ax:ind:prob}
\models \Pr[ev_1] \leq J  \sepand \Pr[ev_2] \leq K \to \Pr[ev_1 \land ev_2]\leq J \cdot K.
\tag{IndepProb}
\end{equation}

* Equal probabilities.
Let $b_1, b_2$ be two boolean expressions. Recall that $b_1, b_2 \in \Event$ too.

\begin{equation} \label{ax:equal:prob}
\models \apEq{b_1}{b_2} \to \Pr[b_1]  = \Pr[b_2]
\tag{EqualProb}
\end{equation}