Suppose $\Gamma;\Delta \vdash b : \tau$. Then for any $\pctx$ such that $\pctx \vdash \Gamma;\Delta$ and any $\yctx$ such that $\fv_{\mathcal{Y}}(b) \subseteq \yctx$,
\[
\pctx; \yctx \vdash \rho(b) : \tau\quad \text{and}\quad \pctx; \yctx \vdash \cn(b) : \text{Formula}.
\]
\label{prop:wellsorted}
\end{proposition}
\begin{proof}
This proceeds by induction on the typing derivation.
Let $\pctx$ be such that $\pctx \vdash \Gamma;\Delta$ and let $\yctx$ be such that $\fv_{\mathcal{Y}}(b)\subseteq \yctx$.
\begin{description}
\item[\rname{T-Vltn}] This is immediate.
\item[\rname{T-Split}]
Then $b = (\kwlet\ x_1,\ldots ,x_{n},w_1 ,\ldots ,w_{n'} = \kwsplit\ b_1\ \kwin\ b_2)$, and necessarily that $\Gamma;\Delta \vdash b_1 : \ut_{1}\times \cdots \times \ut_{n}\times \lint_{1}\times \cdots \times \lint_{n'}$, and
\[
\Gamma, x_1 : \tau_1,\ldots ,x_{n}, \rd{w_{1}} : \rd{\lint_1} ,\ldots ,\rd{w_{n'}} : \rd{\lint_{n'}};\Delta, w_{1} : \lint_1 ,\ldots ,w_{n} : \lint_{n'} \vdash b_2 : \tau.
\]
We also have
\[
\rho(b) = \rho(b_2)\{x_{i}\mapsto \pi_{i} \rho(b_1)\mid 1 \leq i \leq n\} \{w_{i} \mapsto \pi_{n + i}\rho(b_1), \rd{w_{i}} \mapsto \pi_{n + i}\rho(b_1)\mid 1 \leq i \leq n'\}.
\]
\begin{align*}
S_{\var} &= \{x_{i }\mapsto  \pi_{i} \rho(b_1)\mid 1 \leq i \leq n\}\\
S_{\lvar} &= \{w_{i}\mapsto \pi_{n + i}\rho(b_1)\mid 1 \leq i \leq n'\}\\
S_{\rd{\lvar}} &= \{\rd{w_{i}}\mapsto \pi_{n + i}\rho(b_1)\mid 1 \leq i \leq n'\}.
\end{align*}
In this case, $\rho(b) = S_{\var}S_{\lvar}S_{\rd{\lvar}}(\rho(b_2))$.
By induction, $\pctx;\yctx \vdash \rho(b_1) : \ut_1 \times \cdots \times \ut_{n}\times \lint_{1} \times \cdots \times \lint_{n'}$. By the projection sorting rule, $\pctx;\yctx \vdash \pi_{i} \rho(b_1) : \ut_{i} $ for $1 \leq i \leq n$ and $\pctx;\yctx \vdash \pi_{n + i} \rho(b_1) : \lint_{i}$ for $1 \leq i \leq n'$.

\[
\pctx' = \pctx, x_1 : \ut_1 ,\ldots , x_{n} : \ut_{n}, \rd{w_1} : \lint_1 ,\ldots ,\rd{w_{n'}} : \lint_{n'}, w_{1} : \lint_{1} ,\ldots ,w_{n} : \lint_{n'}.
\]
\[
\pctx' \vdash \Gamma, x_1 : \ut_1,\ldots ,x_{n} : \ut_{n},\rd{w_{1}} : \rd{\lint_1} ,\ldots ,\rd{w_{n'}} : \rd{\lint_{n'}} ;\Delta, w_1 : \lint_1 ,\ldots ,w_{n} : \lint_{n'}.
\]
As $\dom(S_{x})\cup \dom(S_{w})$ does not contain any variables from $\mathcal{Y}$, we also have $\fv_{\mathcal{Y}}(b_2)$. By induction, $\pctx' ; \yctx \vdash \rho(b_2) : \tau$.
\begin{align*}
\dom(S_{\var}) &= \{x_1 ,\ldots x_{n}\} \\
\dom(S_{\lvar}) &= \{w_1 ,\ldots ,w_{n'}\}\\
\dom(S_{\rd{\lvar}}) &= \{\rd{w_{1}},\ldots ,\rd{w_{n'}}\},
\end{align*}
we have $\pctx; \yctx \vdash S_{\var}S_{\lvar}S_{\rd{\lvar}}(\rho(b_2)) : \tau$.
This means $\pctx; \yctx \vdash \rho(b) : \tau$. Using this fact and in a similar manner, we can argue $\pctx;\yctx \vdash \cn(b) : \text{Formula}$.
\item[\rname{T-Ops}]
Then $b = o(b_1,\ldots ,b_{n})$, and necessarily that $\Gamma ; \Delta\vdash  b_{i} : \ut_{i}$ where $o : \ut_{1},\ldots ,\ut_{n}\to \ut$. By induction, $\pctx; \yctx \vdash  \rho(b_{i}) : \ut_{i}$, and $\pctx; \yctx \vdash \cn(b_{i}) : \text{Formula}$. Then by the ops sorting rule, $\pctx; \yctx  \vdash \rho(b) : \tau$ and by the conjunction sorting rule, $\pctx; \yctx \vdash \cn(b) : \text{Formula}$.
\item[\rname{T-Assert}]
Then $b = \pt{b_1}{b_2}$, and necessarily $\Gamma;\Delta \vdash b_{1} : \mathsf{Bool}$, $\Gamma ; \Delta \vdash b_{2} : \tau$.
By induction, $\pctx;\yctx \vdash \rho(b_1) : \mathsf{Bool}$, $\pctx;\yctx \vdash \rho(b_2) : \tau$, and $\pctx;\yctx \vdash \cn(b_1)$, $\pctx; \yctx \vdash \cn(b_{2}) : \text{Formula}$. From the first statement, we have $\pctx; \yctx \vdash \rho(b_1) = \mathsf{true} : \text{Formula}$. As $\rho(b) = \rho(b_2)$, we have $\pctx; \yctx \vdash \rho(b) : \tau$. From the conjuction sorting rule, $\pctx ;\yctx \vdash \cn(b) : \text{Formula}$.
\item[\rname{T-Mark}]
Then $b = \emark{a}{b_1}{b_2}\# s$, and necessarily that $\Gamma; \Delta \vdash b_1 : \mathsf{Intvl}$, $\Gamma; \Delta \vdash b_2 : \mathsf{Vltn}$.
As $\rho(b) \in \fv_{\mathcal{Y}}(b)$, and we assume that $\fv_{\mathcal{Y}}(b)\subseteq \yctx$, then we have $\pctx;\yctx \vdash \rho(b) : \mathsf{Point}$.
By induction, $\pctx; \yctx \vdash \rho(b_1) : \mathsf{Intvl}$, $\pctx;\yctx \vdash \rho(b_2) : \mathsf{Real}$, and $\pctx;\yctx \vdash \cn(b_1) : \text{Formula}$, $\pctx; \yctx \vdash \cn(b_2): \text{Formula}$. By the former two statements we can obtain through a straightforward series of sorting rules
\[
\pctx; \yctx \vdash \val_{a}([\tleft(\rho(b_1)), \rho(b)]) = \rho(b_2) : \text{Formula}.
\]
We can apply the sorting conjuction rule with this and the latter two statements to net
$\pctx;\yctx \vdash \cn(b) : \text{Formula}$.

\item[\rname{T-EvalPc}]
Then $b = \eeval{a}{b'}$, and necessarily that $\Gamma; \Delta \vdash b' : \mathsf{Piece}$. By induction, $\pctx; \yctx \vdash \rho(b') : \mathsf{Piece}$ and $\pctx; \yctx \vdash \cn(b') : \text{Formula}$, which means by the Val sorting rule $\pctx; \yctx \vdash \rho(b) : \mathsf{Vltn}$ and since $\cn(b') = \cn(b)$, $\pctx; \yctx \vdash \cn(b) : \text{Formula}$.

\item[\rname{T-EvalIntvl}] Almost identical to the argument for \rname{T-EvalPc}.

\item[\rname{T-Div}]
Then $b = \ediv{b_1}{b_2}$, and necessarily that $\Gamma;\Delta \vdash b_1 : \mathsf{Intvl}$, $\Gamma;\Delta \vdash b_2 : \mathsf{Point}$. By induction, $\pctx;\yctx \vdash \rho(b_1): \mathsf{Intvl}$, $\pctx;\yctx \vdash \rho(b_2): \mathsf{Point}$, and $\pctx; \yctx \vdash \vdash \cn(b_1)$, $\pctx;\yctx \vdash \cn(b_2) : \text{Formula}$. The former statements, through a straightforward set of sorting rules can be used to show both
\[
\pctx; \yctx \vdash ([\tleft(\rho(b_1)), \rho(b_2)], [\rho(b_2), \tright(\rho(b_1))]) : \mathsf{Intvl}\times \mathsf{Intvl}
\]
\[
\pctx; \yctx \vdash\tleft(\rho(b_1)) \leq \rho(b_2) \leq \tright(\rho(b_1)) : \text{Formula}.
\]
We can apply the sorting conjuction rule with this and the latter two statements from the induction hypothesis to net
\[
\pctx; \yctx \vdash \cn(b) : \text{Formula}.
\]
As $\rho(b) = ([\tleft(\rho(b_1)), \rho(b_2)], [\rho(b_2), \tright(\rho(b_1))])$, we have
$\pctx;\yctx \vdash \rho(b) : \mathsf{Intvl}\times \mathsf{Intvl}$.

\item[\rname{T-Piece}] This is very similar to that of \rname{T-Ops}. \qed
\end{description}
\end{proof}

We now move toward semantic results about constraints.
Fix an interpretation and variable assignment. We say that two substitutions $S_1$ and $S_2$ are interpreted the same $\dom(S_1) =\dom(S_2)$ and for all $x\in \dom(S_1)$, $\interp,\assn \vDash S_1(x) = S_2(x)$. We have the following related lemma.
\begin{lemma}
Let $S_1$ and and $S_2$ be two logical substitutions. If $S_1$ and $S_2$ are interpreted the same, then $\interp, \assn \vDash S_1(t) = S_2(t)$ for any term $t$, and  $\interp, \assn\vDash S_1(f) \iff S_2(f)$.
\label{prop:semsub}
\end{lemma}

Since our constraints contain variables intended to represent points marked within the protocol, it will be important to ensure that our variable assignment maps the variables to the proper value for a given derivation.
\begin{definition}
Let $\assn$ be a variable assignment and $D$ a derivation. We say that $\assn$ \emph{agrees with} $D$ if for any $\#s$, occuring such that $\emark{a}{e_1}{e_2}\#s \eval r\pnt$ occurs in $D$, we have that $\assn(y_{\#s}) = r\pnt$.
\end{definition}
If we assume that each mark within a protocol has a unique identifier, any derivation involving that protocol will always have an assignment that agrees with it.

\begin{proposition}[Soundness]
Let $\vset$ be a valuation set and suppose $b$ is disjoint and  $\cdot \vdash b : \tau$.
If $D : b\eval_{\vset} \v$, then $\interp_{\vset}, \assn\vDash \cn(b)$ and $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$ for any variable assignment $\assn$ that agrees with $D$.
\label{prop:soundness}
\end{proposition}
\begin{proof}
This proceeds by induction on $D$.
Suppose that $D : b \eval_{\vset} \v$ and suppose $\assn$ agrees with $D$.
We omit $\vset$ as a subscript from here on. We break up our cases based on the last rule applied.

\begin{description}
\item[\rname{Split}]
Then $b = (\kwlet\ x_1,\ldots ,x_{n}, w_1,\ldots ,w_{n'} = \kwsplit\ b_1\ \kwin\ b_2)$. It must be that $b_1 \eval (\v_1 ,\ldots ,\v_{n+ n'})$ and $S(b_2) \eval \v$ where we set
\[
S = \{x_{i} \mapsto \v_{i} \mid 1 \leq i \leq n\}\{w_{i} \mapsto \v_{n  +i}, \rd{w_{i}} \mapsto \rd{\v_{n  +i}} \mid 1 \leq i \leq n'\}.
\]
Immediately by induction, $\interp, \assn \vDash \cn(b_1) $ and $\sem{\rho(b_1)}_{\interp}^{\assn} = (\unrd{\v_1} ,\ldots ,\unrd{\v_{n+ n'}})$. Also immediately by induction, $\interp,\assn \vDash \cn(S(b_2))$ and $\sem{\rho(S(b))}_{\interp}^{\assn} = \unrd{\v}$. By \Cref{prop:subswapf}, $\cn(S(b_2)) = \unrd{S}(\cn(b_2))$ and $\rho(S(b_2)) = \unrd{S}(\rho(b_2))$. Therefore $\interp,\assn \vDash\unrd{S}(\cn(b_2))$ and $\sem{\unrd{S}(\rho(b_2))}_{\interp}^{\assn} = \unrd{\v}$.

\[
S_{\rho} = \{x_{i} \mapsto \pi_{i}\rho(b_1) \mid 1 \leq i \leq n\}\{w_{i} \mapsto \pi_{n + i}\rho(b_1), \rd{w_{i}} \mapsto \pi_{n + i}\rho(b_1) \mid 1 \leq i \leq n'\}.
\]
As $\sem{\rho(b_1)}_{\interp}^{\assn} = (\unrd{\v_1} ,\ldots, \unrd{\v_{n + n'}})$, we have $\sem{\pi_{i}\rho(b_1)}_{\interp}^{\assn} = \unrd{\v_{i}}$. This means $S_{\rho}$ and $\unrd{S}$ are interpreted the same. Then by
\Cref{prop:semsub}, $\interp,\assn \vDash_{\vset} S_{\rho}(\cn(b_2))$, and $\sem{S_{\rho}(\rho(b_2))}_{\interp}^{\assn} = \unrd{\v}$.
Because $\cn(b) = \cn(b_1)\wedge S_{\rho}(\cn(b_2))$ and $\rho(b) = S_{\rho}(\rho(b_2))$, we have established this case.
\item[\rname{Ops}]
Then $b = o(b_1,\ldots ,b_{n})$, $b_{i}\eval \v_{i}$, $\rd{\sem{o}(\unrd{\v_1} ,\ldots ,\unrd{\v_{n}})} = \v$, $\rho(b) = \mathtt{o}(\rho(b_1),\ldots ,\rho(b_n))$, and $\cn(b) = \cn(b_1)\land \cdots \land \cn(b_{n})$. By induction, $\sem{\rho(b_{i})}_{\interp}^{\assn} = \unrd{\v_{i}}$ and $\interp,\assn \vDash \cn(b_{i})$.  Therefore $\interp,\assn\vDash \cn(b)$. Also,
\[
\sem{\rho(b)}_{\interp}^{\assn} = \sem{o}(\sem{\rho(b_1)}_{\interp}^{\assn} ,\ldots , \sem{\rho(b_n)}_{\interp}^{\assn} ) = \sem{o} (\unrd{\v_1},\ldots ,\unrd{\v_{n}}) = \unrd{\v}.
\]
\item[\rname{Assert}]
Then $b = \pt{b_1}{b_2}$, and $b_1 \eval \mathsf{true}$, $b_2\eval \v$.
By induction, $\sem{\rho(b_{1})}_{\interp}^{\assn} = \mathsf{true}$, $\interp,\assn \vDash \cn(b_1)$, $\sem{\rho(b_2)}_{\interp}^{\assn} = \unrd{\v}$, and $\interp,\assn \vDash \cn(b_2)$. This immediately gives us $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$ and $\interp,\assn \vDash \cn(b)$.
\item[\rname{Mark}]
Then $b = \emark{a}{b_1}{b_2}$, and $b_1 \eval [r_1, r'_1]$ for some $r_1,r'_1\in [0,1]$, $b_2\eval \v_{a'}(P)$, with $V_{a}[r_1,r] = V_{a'}(P)$. Let $y =\rho(b)$.
Since $\assn$ agrees with $D$, $\assn(y) = r\pnt$. This already establishes $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$.

By induction, $\sem{\rho(b_1)}_{\interp}^{\assn} = [r_1,r'_{1}]$, $\sem{\rho(b_2)}_{\interp}^{\assn} = V_{a'}(P)$, and both $\interp,\assn \vDash\cn(b_1)$ and $\interp,\assn\vDash\cn(b_2)$.
As $V_{a}[r_1, r] = V_{a'}(P)$ and $\sem{\rho(b)}_{\interp}^{\assn} = r\pnt$, we have $\interp,\assn\vDash (\val_{a}[\tleft(\rho(b_1)), \rho(b)] = \rho(b_2))$.
In culmination, $\interp,\assn\vDash\cn(b)$.

\item[\rname{EvalPc}]
Then $b = \eeval{a}{b'}$, and $b' \eval P_{i}[r_{i}, r'_{i}]$ and $\v = V_{a}(P_{i}[r_{i},r'_{i}])$. By induction, $\sem{\rho(b')}_{\interp}^{\assn} = P_{i}[r_{i},r'_{i}]$ and $\interp,\assn \vDash \cn(b')$. The former gives us $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$. The latter gives us $\interp,\assn \vDash \cn(b)$ since $\cn(b) = \cn(b')$.

\item[\rname{EvalIntvl}] The argument here is just a more simple verion of the argument for \rname{EvalPc}.

\item[\rname{Div}]
Then $b = \ediv{b_1}{b_2}$, and $b_1 \eval [r_1,r'_{1}]$, $b_2 \eval r_2$ with $r_1 \leq r_2 \leq r'_{1}$. By induction, $\sem{\rho(b_1)}_{\interp}^{\assn} = [r_1, r'_{1}]$, $\sem{\rho(b_2)}_{\interp}^{\assn} = r_2\pnt$, and both $\interp,\assn \vDash\cn(b_1)$ and $\interp,\assn\vDash \cn(b_2)$.  We can conclude with the former inductive statements that $\sem{\rho(b)}_{\interp}^{\assn} = ([r_1, r_{2}], [r_{2}, r'_{1}]) = \unrd{\v}$. Since $r_1 \leq r_2 \leq r'_{1}$, we also have $\interp,\assn \vDash \tleft(\rho(b_1))\leq \rho(b_2) \leq \tright(\rho(b_1))$ which we can use to conclude $\interp,\assn \vDash \cn(b)$.

\item[\rname{Tup}] Then $b = (b_1,\ldots ,b_{n})$, $b_{i} \eval \v_{i}$, $\v = (\v_1 ,\ldots ,\v_{n})$, $\rho(b) = (\rho(b_1) ,\ldots ,\rho(b_{n}))$, and $\cn(b) = \cn(b_1) \land \cdots \land \cn(b_{n})$. By induction, $\sem{\rho(b_{i})}_{\interp}^{\assn} = \unrd{\v_{i}}$, and $\interp,\assn \vDash \cn(b_{i})$. Clearly $\interp,\assn \vDash \cn(b)$. Also,
\[
\sem{\rho(b)}_{\interp}^{\assn} = (\sem{\rho(b_{1})}_{\interp}^{\assn}, \sem{\rho(b_{n})}_{\interp}^{\assn}) = (\unrd{\v_1} ,\ldots ,\unrd{\v_{n}}) = \unrd{\v}.
\]

\item[\rname{Piece}] This is very similar to the case for \rname{Tup}.

\end{description}
\qed
\end{proof}

\begin{proposition}[Completeness]
\label{prop:completeness}
Let $\vset$ be a valuation set, and $\Gamma; \Delta \vdash b : \tau$. Let $\gamma\vDash \Gamma$ and $\delta \vDash \Delta$. Suppose $\interp_{\vset}, \assn \vDash \cn(\gamma;\delta (b))$. Then there is a derivation $D$ such that $\assn$ agrees with $D$ and $D : b \eval_{\vset} \v$ and $\unrd{\v} = \sem{\rho(\gamma;\delta (b))}_{\interp_{\vset}}^{\assn}$.
\end{proposition}
\begin{proof}
We prove for any $\assn$ and any $\gamma \vDash \Gamma$, $\delta \vDash \Delta$ such that $\interp_{\vset},\assn \vDash \cn(\gamma;\delta (b))$, there is $D : b \eval \v$, $\unrd{\v} = \sem{\rho(\gamma;\delta b))}_{\interp}^{\assn}$ and $\assn$ agrees with $D$.
This proceeds by induction on $\Gamma;\Delta \vdash b : \tau$. Suppose that $\interp, \assn\vDash_{\vset} \cn(\gamma;\delta(b))$. We break up our cases based on the structure of $b$.
The cases for $\rname{Bool}$, $\rname{Real}$, $\rname{Point}$, $\rname{Piece}$, and $\rname{Cake}$ are obvious.
\begin{description}
\item[\rname{Var}] This is also obvious.
Then $b = x$ and $x\in \var$, or $b = \rd{w}$ and $w \in \lvar$. The former is obvious so suppose the latter.
Then $\Gamma(\rd{w}) = \rd{\v}$ and $\gamma;\delta(\rd{w}) \eval \rd{\v}$. Also, $\sem{\gamma;\delta(\rd{w})}_{\interp}^{\assn} = \sem{\rd{\v}}_{\interp}^{\assn} = \v = \unrd{\rd{\v}}$, which completes this case.
\item[\rname{AffVar}]  This is obvious.
\item[\rname{Split}] Then
\begin{align*}
\cn(\gamma;\delta (b)) = \cn(\gamma; \delta (b_1))\land S_{b}(\cn(\gamma ;\delta (b_2))) \quad \text{and}\quad \rho(\gamma;\delta (b)) = S_{b}(\rho(\gamma;\delta (b_2)))
\end{align*}
where we set
\[
S_{\rho} = \{x_{i} \mapsto \pi_{i}\rho(b_1) \mid 1 \leq i \leq n\}\{w_{i} \mapsto \pi_{n + i}\rho(b_1), \rd{w_{i}} \mapsto \pi_{n + i}\rho(b_1) \mid 1 \leq i \leq n'\}.
\]
We also have
\begin{align*}
&\Gamma;\Delta_1 \vdash b_1 : \ut_1 \times \cdots \times \ut_{n} \times \lint_{1} \times \cdots \times \lint_{n'} \\
&\Gamma; x_1 : \ut_1 ,\ldots ,x_{n} : \ut_{n}, \rd{w_1} : \rd{\lint_{1}} ,\ldots ,\rd{w_{n'}} ; \Delta_2, w_1 : \lint_1 ,\ldots ,w_{n'} : \lint_{n'}\vdash b_2 : \tau.
\end{align*}
According to \Cref{prop:partitiondelta}, we can partition $\delta$ into $\delta_1$ and $\delta_2$ such that $\gamma;\delta_1 (b_1) = \gamma;\delta(b_1)$, $\gamma;\delta_2 (b_2) = \gamma;\delta(b_2)$ and $\delta_1 \vDash \Delta_1$, $\delta_2 \vDash \Delta_2$.
By induction, there is $D_1$ agreeing with $\assn$ for which
\[
D_1 : \gamma;\delta_1 (b_1) \eval \v',
\]
and $\unrd{\v'} = \sem{\rho(\gamma;\delta_1 (b_1))}_{\interp}^{\assn}$.
As $\Gamma;\Delta_1 \vdash b_1 : \ut_1 \times \cdots \times \ut_{n}\times \lint_{1} \times \cdots \times \lint_{n}$,
we have $\cdot \vdash \gamma;\delta_1 (b_1) : \ut_1 \times \cdots \times \ut_{n}\times \lint_{1} \times \cdots \times \lint_{n}$.
by \Cref{prop:typesoundness} we have $\v' = (\v_1 ,\ldots ,\v_{n+ n'})$, where $\v_{i} \in \sem{\ut_{i}}$ for $1 \leq i \leq n$ and $\v_{n + i}\in \sem{\lint_{n'}}$ for $1 \leq i \leq n'$. This means $\sem{\pi_{i} \rho(\gamma;\delta_1 (b_1))}_{\assn}^{\interp} = \unrd{\v_{i}}$ for all $i$. By \Cref{prop:semsub},
\begin{equation}
\interp,\assn \vDash S_{b'}(\cn(\gamma;\delta_2 (b_2))) \quad \text{and} \quad \sem{S_{b}(\rho(\gamma;\delta_2 (b_2)))}_{\interp}^{\assn} = \sem{S_{b'}(\rho(\gamma;\delta_2 (b_2)))}_{\interp}^{\assn}
\label{eq:complsplit1}
\end{equation}
where $S_{b'} = \{x_{i} \mapsto \v_{i} \mid 1 \leq i \leq n + n'\}$. If we set
\[
S = \{x_{i} \mapsto \v_{i} \mid 1 \leq i \leq n\}\{w_{i} \mapsto \v_{n + i}\mid 1 \leq i \leq n'\} \{\rd{w_{i}} \mapsto \rd{\v_{n + i}} \mid 1 \leq i \leq n'\}
\]
by \Cref{prop:subswapf},
\begin{equation}
\interp,\assn \vDash \cn(S(\gamma;\delta_2 (b_2)) ) \quad \text{and}\quad \sem{\rho(S(\gamma;\delta_2 (b_2)))}_{\interp}^{\assn} =\sem{S_{b'}(\rho(\gamma;\delta_2 (b_2)))}_{\interp}^{\assn}.
\label{eq:complsplit2}
\end{equation}
If we let $\gamma' = \gamma \{x_{i} \mapsto \v_{i} \mid 1 \leq i\leq n\}\{\rd{w_{i}} \mapsto \rd{\v_{n + i}} \mid 1 \leq i\leq n'\}$ and $\delta' = \delta_2  \{w_{i} \mapsto \v_{n + i}\mid 1 \leq i \leq n'\}$, then
\begin{equation}
S(\gamma;\delta_2 (b_2)) = \gamma';\delta' (b_2).
\label{eq:complsplit3}
\end{equation}
Evidently $\gamma' \vDash \Gamma, x_1 : \ut_{1},\ldots , x_{n} : \ut_{n}, \rd{w_{1}} : \rd{\lint_1},\ldots ,\rd{w_{n'}} : \rd{\lint_{n'}}$ and $\delta' \vDash \Delta_2, w_1 : \lint_1 ,\ldots ,w_{n'} : \lint_{n'}$.

By induction, there is $D_2$ agreeing with $\assn$ such that $D_{2} : \gamma';\delta'(b_2)\eval \v $ and $\unrd{\v} = \sem{\rho(\gamma';\delta'( b_2))}_{\interp}^{\assn}$. By \Cref{eq:complsplit3}, we can conclude $D : \gamma;\delta (b) \eval \v$, with $D_1$ and $D_2$ being the premises of $D$. As $\assn$ agrees with both $D_1$ and $D_2$, $\assn$ also agrees with $D$.

By combining \Cref{eq:complsplit1}, \Cref{eq:complsplit2}, and \Cref{eq:complsplit3}, we obtain that $\sem{\rho(\gamma;\delta (b))}_{\interp}^{\assn} = \sem{\rho(\gamma'; \delta' (b_2))}_{\interp}^{\assn}$. This means $\unrd{\v} = \sem{\rho(\gamma;\delta (b))}_{\interp}^{\assn}$, concluding this case.

\item[\rname{Ops}] Then $\rho(b) = o(\rho(b_1),\ldots ,\rho(b_{n}))$, $\cn(b) = \cn(b_1) \land \cdots \land \cn(b_{n})$ and $o : \ut_1 ,\ldots ,\ut_{n} \to \tau$ so $\Gamma;\Delta_{i} \vdash b_{i} : \ut_{i}$, where $\Delta = \Delta_1,\ldots ,\Delta_{n}$. According to $\Cref{prop:partitiondelta}$, $\gamma;\delta_{i} (b_{i}) = \gamma;\delta(b_{i})$ and $\delta_{i} \vDash \Delta$. Then by induction, $D_{i} : b_{i} \eval \v_{i}$ and $\unrd{\v_{i}} = \sem{\gamma;\delta_{i}(b_{i})}_{\interp}^{\assn}$ and $\assn$ agrees with $D_{i}$. By \Cref{prop:typesoundness}, $\v_{i} \in \sem{\ut_{i}}$. This enables us to apply \rname{Ops} so $\gamma;\delta(b) \eval \sem{o}(\v_1 ,\ldots ,\v_{n})$.
We also have $\sem{\gamma;\delta(\rho(b))}_{\interp}^{\assn} = \sem{o}(\sem{\gamma;\delta_{1}(b_1)}_{\interp}^{\assn},\ldots ,\sem{\gamma;\delta_{n}(b_n)}_{\interp}^{\assn})$.

\item[\rname{Mark}] Then $\rho(b) = y$ for some $y\in \mathcal{Y}$, $\cn(b) = \cn(b_1) \land \cn(b_2) \land (\val_{a}([\tleft(\rho(b_1)), \rho(b)]) = \rho(b_2))$, and $\tau = \mathsf{Point}$, $\Gamma;\Delta_1 \vdash b_1 : \rd{\mathsf{Intvl}}$, $\Gamma;\Delta_2 \vdash b_2 : \mathsf{Vltn}$, where $\Delta = \Delta_1, \Delta_2$.
According to \Cref{prop:partitiondelta}, $\gamma;\delta_1 (b_1) = \gamma;\delta(b_1)$, $\gamma;\delta_2(b_2) = \gamma;\delta(b_2)$, and $\delta_1 \vDash \Delta_1$, $\delta_2 \vDash \Delta_2$. By induction, $D_1 : \gamma;\delta_1 (b_1 ) \eval \v_1$, where $\unrd{\v_1} = \sem{\rho(\gamma;\delta_1(b_1))}_{\interp}^{\assn}$ and $\assn$ agrees with $D_1$. By \Cref{prop:typesoundness} $\v_1 = \rd{[r, r']}$ for some $r, r' \in \mathbb{R}$.
Also by induction, $D_2 : \gamma;\delta_2(b_2) \eval \v_2$, where $\unrd{\v_2} = \sem{\gamma;\delta_2(\rho(b_2))}_{\interp}^{\assn}$ and $\assn$ agrees with $D_2$. By \Cref{prop:typesoundness}, $\v_2 = \val_{a'}(P)$ for some piece or interval $P$ and some agent $a'$.

Now $\sem{\tleft(\rho(\gamma;\delta_1(b)))}_{\interp}^{\assn} = r\pnt$.
As $\interp,\assn \vDash \cn(b)$, we have $V_{a}[r, \assn(y)] = V_{a'}(P)$. So using $D_1$, $D_2$, and $V_{a}[r, \assn(y)] = V_{a'}(P)$ as premises for \rname{Mark}, we can apply it to obtain $D: \gamma;\delta(b) \eval \assn(y)$ for which $\assn$ evidently agrees with $D$. Now $\unrd{\assn(y)} = \assn(y) = \sem{y}_{\interp}^{\assn}$, completing this case.

\item[\rname{EvalPc}] Then $\Gamma;\Delta \vdash b : \mathsf{Vltn}$, and $\Gamma;\Delta \vdash b' : \mathsf{Piece}$. By induction, there is $D' : b' \eval \v'$ and $\unrd{\v'} = \sem{\rho(\gamma;\delta(b'))}_{\interp}^{\assn}$, and $\assn$ agrees with $D'$. By \Cref{prop:typesoundness}, $\v = \rd{P}$ for some piece $P$. We can apply \rname{EvalPc} to obtain $\gamma;\delta(b)\eval V_{a}(P)$.
\begin{align*}
\sem{\rho(\gamma;\delta(b))}_{\interp}^{\assn} = \sem{\val_{a}(\rho(\gamma;\delta(b')))}_{\interp}^{\assn} = V_{a}(\sem{\rho(\gamma;\delta(b'))}_{\interp}^{\assn}) = V_{a}(P) = \unrd{V_{a}(P)}.
\end{align*}
The argument for when $\Gamma;\Delta \vdash b' : \mathsf{Intvl}$ is nearly identical.

\item[\rname{EvalIntvl}] The argument here is nearly identical to the argument for \rname{EvalPc}.
\item[\rname{Div}] Then $\rho(b) = ([\tleft(\rho(b_1)), \rho(b_2)], [\rho(b_2), \tright(\rho(b_1))])$, $\cn(b) = \cn(b_1)\land \cn(b_2)\land \tleft(\rho(b_1))\leq  \rho(b_2) \leq \tright(\rho(b_1))$, $\Gamma;\Delta_1 \vdash b_1 : \mathsf{Intvl}$, $\Gamma;\Delta_2 \vdash b_2 : \mathsf{Point}$, and $\Delta = \Delta_1, \Delta_2$. By \Cref{prop:partitiondelta}, $\gamma;\delta_1(b_1) = \gamma;\delta(b_1)$ and $\gamma;\delta_2(b_2) = \gamma;\delta(b_2)$, and $\delta_1 \vDash \Delta_1$, $\delta_2 \vDash \Delta_2$. So by induction, $D_1 : \gamma;\delta_1 (b_1)\eval [r,r']$, $[r,r'] = \sem{\rho(\gamma;\delta_1(b_1))}_{\interp}^{\assn}$ and $\assn$ agrees with $D_1$. Also by induction, $D_2 :\gamma;\delta_2 (b_2) \eval r_2\pnt$, $r_2\pnt = \sem{\rho(\gamma;\delta_2(b_2))}_{\interp}^{\assn}$, and $\assn$ agrees with $D_2$.
Thus, $\sem{\tleft(\rho(\gamma;\delta_1(b_1)))}_{\interp}^{\assn} = r_1$ and $\sem{\tright(\rho(\gamma;\delta_1(b_1)))}_{\interp}^{\assn} = r'_1$.
Since $\interp,\assn \vDash \cn(b)$, we have $r_1 \leq r_2 \leq r'_{1}$. Therefore we can apply \rname{Div} with $D_1$ and $D_2$ as premises to obtain
$D : \gamma;\delta(b) \eval ([r_1, r_2], [r_2, r'_{1}])$, and $\assn$ agrees with $D$ as it agreed with $D_1$ and $D_2$. We are done as $\sem{([\tleft(\rho(b_1)), \rho(b_2)], [\rho(b_2), \tright(\rho(b_1))])}_{\interp}^{\assn} = ([r_1, r_2], [r_2, r'_{1}]) =\unrd{([r_1, r_2], [r_2, r'_{1}])}$.

\item[\rname{Assert}] Then $\rho(b) = \rho(b_2)$, $\cn(b) = (\rho(b_1) = \kwtrue)\land \cn(b_1)\land \cn(b_2)$, and $\Gamma;\Delta_1 \vdash b_1 : \mathsf{Bool}$, $\Gamma;\Delta_2 \vdash b_2 : \tau$, where $\Delta = \Delta_1, \Delta_2$. According to \Cref{prop:partitiondelta}, $\gamma;\delta_1 (b_1) = \gamma;\delta(b_1)$, $\gamma;\delta_2 (b_2)=\gamma;\delta(b_2) $, and $\delta_1 \vDash \Delta_1$, $\delta_2 \vDash \Delta_2$. By induction, $D_1 : \gamma;\delta_1(b_1)\eval \kwtrue$, where $\assn$ agrees with $D_1$. Also by induction, $D_2 : \gamma;\delta_2(b_2) \eval \v$ where $\unrd{\v} = \sem{\rho(\gamma;\delta_2(b_2))}_{\interp}^{\assn}$, and $\assn$ agrees with $D_2$. This allows us to use \rname{Assert} to obtain $D : \gamma;\delta(b)\eval \v$, with premises $D_1$ and $D_2$. As $D$ is composed in this way, $\assn$ agrees with $D$. Since $\rho(b) = \rho(b_2)$, we are done with this case.

\item[\rname{Tup}] Then $b = (b_1 ,\ldots ,b_{n + n'})$, $\rho(b) = (\rho(b_1),\ldots ,\rho(b_{n+ n'}))$, $\cn(b) = \cn(b_1) \land \cdots \land \cn(b_{n + n'})$, and  $\Gamma ;\Delta_{i} \vdash b :  \ut_i$ for $1 \leq i \leq n$ and $\Gamma; \Delta_{n + i} \vdash b_{n + i} : \lint_{i}$ for $1 \leq i \leq n'$, and $\Delta = \Delta_1 ,\ldots ,\Delta_{n + n'}$. According to \Cref{prop:partitiondelta}, $\gamma;\delta_{i}(b_{i}) = \gamma;\delta(b_{i})$, and $\delta_{i} \vDash \Delta_{i}$ for $1 \leq i \leq n + n'$.
By induction, $D_{i} : \gamma;\delta_{i}(b_{i})\eval \v_{i}$, where $\unrd{\v_{i}} = \sem{\rho(\gamma;\delta_{i}(b_{i}))}_{\interp}^{\assn}$, and $\assn$ agrees with $D_{i}$ for $1 \leq i \leq n + n'$. Using $D_1 ,\ldots ,D_{n + n'}$ as premises, we can apply \rname{Tup} to obtain $D : \gamma;\delta(b) \eval (\v_1 ,\ldots ,\v_{n + n'})$ where $\assn$ agrees with $D$. We have
\begin{align*}
\unrd{(\v_1 ,\ldots ,\v_{n + n'})} = (\unrd{\v_1} ,\ldots ,\unrd{\v_{n + n'}}) &= (\sem{\rho(\gamma;\delta_1(b_1))}_{\interp}^{\assn} ,\ldots ,\sem{\rho(\gamma;\delta_{n+ n'}(b_{n + n'}))}_{\interp}^{\assn}) \\
&= \sem{(\rho(\gamma;\delta_1(b_1)) ,\ldots ,\rho(\gamma;\delta_{n+ n'}(b_{n + n'})))}_{\interp}^{\assn}\\
&= \sem{\rho(\gamma;\delta((b_1 ,\ldots ,b_{n + n'})))}_{\interp}^{\assn},
\end{align*}
concluding this case.

\item[\rname{Piece}] This is nearly identical to the tuple case.
\end{description}
\end{proof}

Soundness and completeness results lead to the following corollary.
\ccharacterization*

We now argue for the following theorem:
\solvingthm*
We first generalize to the envy-freeness formula to formulae that have mild restrictions.
\begin{definition}
We say that a formula $F$ is a \emph{well-formed property} if $x : \mathtt{S}_{\tau} \vdash F : \text{Formula}$, and $F$ contains no point values.
\end{definition}
Here, $x$ stands in for what a protocol might possibly output. The point value restriction is not overly restrive, as most interesting properties do not reference constant points, however, our theory could be modified slightly to relax this restriction. \Cref{eq:envyfree} is easily seen to be a well-formed property.
We also require some mild assumptions on our expressions.
\begin{definition}
We say that an expression $e$ is \emph{well-formed} if $e$ is closed, well-typed, disjoint, $e$ does not contain any point values (besides 0 and 1), and each mark subexpression contains a unique identifier.
\end{definition}
Similar to protocol properties, very few interesting protocols consider constant points (besides 0 and 1) within the cake.

Here we also generalise $e \vDash E(x)$ to arbitrary formulae.
Given an expression $\cdot \vdash e : \tau$ and a formula $F$ such that $x : \mathtt{s}_{\tau} \vdash F : \text{Formula}$, we say that $e \vDash F$ if for all valuation sets $\vset$, $e\eval_{\vset} \v$ implies $\interp_{\vset} \vDash F\fsub{x}{\lv}$. Now we state and prove our generalized theorem.
\begin{proposition}
\label{prop:solvingthm}
Suppose that $e$ is a well-formed expression and $\cdot \vdash e : \tau$. Let $F$ be a formula such that $x : \mathtt{S}_{\tau} \vdash F : \text{Formula}$.
\begin{equation}
\interp_{\vset} \vDash \bigwedge_{b \in B(e)} \forall \mathcal{Y}_{b}.(\cn(b)\Rightarrow F\fsub{x}{\rho(b)})
\label{eq:solving}
\end{equation}
for all $\vset$ if and only if $e \vDash F$.
\end{proposition}

\begin{proof}
Let $\interp = \interp_{\vset}$.
Suppose that $D: e \eval_{\vset} \v$. By \Cref{prop:pathtype} and \Cref{prop:path}, there is $b \in B(e)$ such that $\vdash b : \tau$ and $D: b\eval_{\vset} \v$. By \Cref{prop:soundness}, for any $\assn$ that agrees with $D$, $\interp,\assn \vDash c(b)$ and $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$. By \Cref{eq:solving},  $\interp_{\vset},\assn \vDash F\fsub{x}{\rho(b)}$.
By \Cref{prop:semsub}, $\interp_{\vset},\assn \vDash F\fsub{x}{\lv}$. $F\fsub{x}{\v}$ is a closed formula so $\interp_{\vset} \vDash F\fsub{x}{\lv}$.

Suppose \Cref{eq:solving} does not hold. Then there is some interpretation $\interp$ and variable assignment $\assn$ such that $\interp,\assn \vDash \cn(b)$ yet $\interp,\assn \not\vDash F\fsub{x}{\rho(b)}$. Then by \Cref{prop:completeness}, $b \eval_{\vset} \v$, where $\unrd{\v} = \sem{\rho(b)}_{\interp}^{\assn}$ for some $b \in B(e)$. By \Cref{prop:path}, $e \eval_{\vset} \v$. By \Cref{prop:semsub}, we have that $\interp,\assn \not\vDash F\fsub{x}{\lv}$, and since $F\fsub{x}{\lv}$ is closed, $\interp \not\vDash F\fsub{x}{\lv}$, which completes the proof.
\end{proof}

\subsection{Protocol execution replication}
\label{app:repl}
The goal of this subsection is to prove the following theorems:
\pured*
\pufequiv*
We first become more precise about derivations and points considered within them.
First recall our \hyperlink{dnotation}{derivation notation}. Briefly, given a derivation of an evaluation judgement $D$, we write $D : e \eval_{\vset} \v$ if the conclusion of $D$ is $e \eval_{\vset}\v$.
Define \[M(D) \triangleq \{r \mid r\pnt\ \text{is a subexpression of}\ \v, \v\ \text{appears in}\ D\}.\]
\Cref{thm:red} can now be expressed as:
\begin{theorem}
Let $\uset$ and $\vset$ be a valuation set, and suppose $D: e\eval_{\vset} \v$. If $\uset$ and $\vset$ agree on $M(D)$, then $D: e \eval_{\uset} \v$.
\end{theorem}

\begin{proof}
This goes by induction on $D$. We break it up into cases based on the last rule applied, of which there are 4 interesting cases.
\begin{description}
\item[\rname{E-EvalPc}]

Here $e = \kweval(e')$ for some $e'$, $D': e'\eval_{\vset}P_{i = 1 }^{n}[r_{i},r'_{i}]$, and $\v = \vset_{a}(P_{i=1}^{n}[r_i,r'_i])$. Now $r_{i}, r'_{i}\in M(D)$ for all $i$ so $\cup_{i = 1}^{n}[r_{i},r'_{i}]$ has all boundary points in $M(D)$. Therefore, since $\uset$ and $\vset$ agree on $M(D)$, ${\uset}_{a}(\cup_{i =1}^{n}[r_{i},r'_{i}]) = \vset_{a}(\cup_{i=1}^{n}[r_{i},r'_{i}])$.
By induction $D' : e'\eval_{\uset}P_{i= 1}^{n}[r_{i},r'_{i}]$, so
we can apply \rname{E-EvalPc} to obtain $D : e\eval_{U_{\vset}}\v$.
\item[\rname{E-EvalIntvl}] This argument is nearly identical to the argument for \rname{E-EvalPc}.
\item[\rname{E-Mark}]
Here $e = \kwmark_{a}(e_1,e_2)$ for some $e_1$ and $e_2$, $D_1 : e_1\eval_{\vset}[r_1,r_2]$, $D_2 : e_2\eval_{\vset}\v_{2}$, $\vset_{a}[r_1,r] = \v_{2}$ with $\v = r\pnt$. Now $r_1,r \in M(D)$. Since $\uset$ and $\vset$ agree on $M(D)$, ${{\uset}}_{a} [r_1,r] = \v_2$. By induction, $D_1 : e_1\eval_{{\uset}}[r_1,r_2]$ and $D_2: e_2\eval_{{\uset}}\v_2$, so applying \rname{E-Mark}, we obtain $D : e\eval_{{\uset}}\v$. \qed
\end{description}
\end{proof}

We restate \Cref{thm:pufequiv} in the following way:
\begin{theorem}
Suppose that $\yctx \vdash \varphi : \text{Formula}$. Let $\vset$ and $\uset$ be valuation sets and $\assn$ be a variable assignment. Suppose $\uset$ and $\vset$ agree on $\{ \sem{t}_{\interp_{\vset}}^{\assn}\mid \yctx \vdash t : \mathtt{Point}, t\ \text{occurs in}\ \varphi\}$. Then
$\interp_{\vset},\assn \vDash \varphi \iff \interp_{\uset},\assn\vDash \varphi$.
\label{thm:pufequivfull}
\end{theorem}
\begin{proof}
By \Cref{prop:simpl}, it suffices to check this on simplified formulas. So assume that $\varphi$ is simplified. This argument proceeds by induction on the structure of $\varphi$.
Set $M = \{\sem{t}_{\interp_{\vset}}^{\assn}\mid \yctx \vdash t : \mathtt{Point}, t\ \text{occurs in}\ \varphi\}$.
The whole argument boils down to showing $\sem{\val_{a}(t)}_{\interp_{\vset}}^{\assn} = \sem{\val_{a}(t)}_{\interp_{U_{\vset}}}^{\assn}$.

Let $\val_{a}(t)$ be a term contained in $\varphi$. Then either $t = [t_1, t'_1]$ for some $t_1,t'_1 \in R_{\mathtt{Point}}$ or $t = \cup ([t_1,t_1'] ,\ldots ,[t_{n},t'_{n}])$ for some $t_{i},t'_{i} \in R_{\mathtt{Point}}$.
We note that $\sem{t_{i}}_{\interp_{\vset}}^{\assn} = \sem{t_{i}}^{\assn} = \sem{t_{i}}_{\interp_{\uset}}^{\assn}$ for all $i$, which also gives $\sem{t}_{\interp_{\vset}}^{\assn} = \sem{t}^{\assn} = \sem{t}_{\interp_{\uset}}^{\assn}$.
Since $\uset$ and $\vset$ agree on $M$, we have that $\uset_{a}(\sem{t}^{\assn}) = \vset_{a}(\sem{t}^{\assn})$ as $\sem{t}^{\assn}$ has boundary points in $M$. This means $\sem{\val_{a}(t)}_{\interp_{\vset}}^{\assn} = \sem{\val_{a}(t)}_{\interp_{U_{\vset}}}^{\assn}$.
\qed
\end{proof}

\subsection{Piecewise uniform valuations}
\label{app:pu}
Here we discuss the arguments for \hyperlink{def:pu}{piecewise uniform valuations}.
In this section we prove the following theorem.
\puexists*

We first start by introducing a form of a valuation and argue some facts about it. Following this, we consider a whole valuation set of this form.

Given an arbitrary valuation $V$ and a finite set of points $\{0,1\} \subseteq M$, we can have a piecewise uniform valuation replicate $V$ on pieces whose endpoints are in $M$.

Let $M = \{m_1,\ldots ,m_{k}\}$ be given such that $ 0= m_0 \leq m_1 < \cdots < m_{k}= 1$. Now let $V$ be any valuation on $[l,r]$, and define
\[
\maxdens{V}{M} = \max_{0 \leq i < k} V[m_{i},m_{i+1}]/(m_{i + 1} - m_{i}).
\]
This quantity is referred to as the \emph{max density of $V$ on $M$}. It represents the largest density of $V$ on adjacent points in $M$. Recall that a piece uniquely determines a piecewise uniform valuation on that piece.
\begin{definition}
Let $d \geq \maxdens{V}{M}$. We let $U_{V}(M,d)$ be the piecewise uniform valuation determined by the piece
\[
P = \bigcup _{i = 1}^{k} [m_{i} - V[m_{i - 1}, m_{i}]/d, m_{i} ] = [m_{1} - V[0, m_{1}]/d, m_{1} ] \cup \cdots \cup [m_{k} - V[m_{k - 1}, m_{k}]/d, m_{k} ].
\]
That is, $U_{V}(M,d) = U_{P}$, in the notation below \Cref{def:pu}.
\end{definition}
$U_{V}(M,d)$ is not well-defined for $ d< \maxdens{V}{M}$. For if this is the case, some intervals in the piece above would overlap further than their endpoints.

We first aim to show this valuation \hyperlink{def:repl}{agrees with $V$ on $M$}. To do so, we state a basic fact about $U_{V}(M,d)$.
\begin{lemma}
$c(U_{V}(M,d)) = d$.
\label{prop:uconst}
\end{lemma}
\begin{proof}
Let $c$ be the constant associated with $U_{V}(M,d)$. Then
\begin{align*}
V[l,r] &= U_{V}(M,d)[l, r] \\
&= U_{V}(M,d)[m_{0}, m_{k}]\\
&= c\sum_{k \geq i > 0}m_{i} - l_{i}\\
&= c\sum_{k \geq i  > 0}(m_{i} - (m_{i} - V[m_{i-1}, m_{i}]/d)\\
&= c\sum_{k \geq i > 0}V[m_{i-1},m_{i}] /d \\
&= cV[m_{0},m_{k}] /d \\
&= cV[l,r] /d
\end{align*}
which implies that $c = d$.
\qed
\end{proof}

\begin{restatable}[]{lemma}{pup}
Let $P$ be any piece with boundary points entirely within $M$ then
\begin{equation}
U_{V}(M,d)(P) = V(P).
\end{equation}
\label{prop:puequiv}
\end{restatable}
\begin{proof}
First, write $M = \{m_0, m_1,\ldots ,m_{k}\}$ where $0 = m_0 \leq m_1 < \cdots < m_{k} = 1$.
We have for any $1 \leq i \leq k$,
\begin{align*}
U_{W}(M,d)[m_{i-1}, m_{i}] &= d(m_{i} - (m_{i} - W[m_{i-1}, m_{i}]/d)) \\
&= d(W[m_{i-1}, m_{i}]/d) \\
&= W[m_{i-1}, m_{i+1}]
\end{align*}
and since $[m_{i}, m_{i'}]$ is the disjoint union of $[m_{j-1}, m_{j}]$ for $i < j \leq i'$, we have by disjointness,
\[
U_{W}(M,d)[m_{i}, m_{i'}] = W[m_{i},m_{i'}]
\]
for any $0 \leq i \leq i' \leq k$. Since $P$ has boundary points entirely within $M$, we can write $P = [m_{i_1}, m'_{i_1}] \cup \cdots \cup [m_{i_{n}}, m'_{i_{n}}]$, for $m_{i_1}\leq m'_{i_{1}}\leq \cdots \leq m_{i_{n}} \leq m'_{i_{n}}$. This means
\begin{align*}
U_{W}(M,d)(P) &= U_{W}(M,d)([m_{i_1}, m'_{i_1}] \cup \cdots \cup [m_{i_{n}}, m'_{i_{n}}]) \\
&= U_{W}(M,d)[m_{i_1}, m'_{i_1}] + \cdots + U_{W}(M,d)[m_{i_{n}}, m'_{i_{n}}] \\
&= W[m_{i_1}, m'_{i_1}] + \cdots + W[m_{i_{n}}, m'_{i_{n}}]\\
&= W([m_{i_1}, m'_{i_1}] \cup \cdots \cup [m_{i_{n}}, m'_{i_{n}}])\\
&= W(P).
\end{align*}
\qed
\end{proof}

We now extend both the above definition and lemma to valuation sets. We define for $\vset$ a valuation set, $\maxdens{\vset}{M} \triangleq \max_{a \in \agents}\maxdens{\vset_{a}}{M}$.
\begin{definition}
Let $\vset$ be a valuation set, $M \supseteq \{0,1\}$ a set of points, and $d \geq \maxdens{\vset}{M}$. Then $U_{\vset}(M,d)$ is the valuation set with $U_{\vset}(M,d)_{a} \triangleq U_{\vset_{a}}(M,d)$ for all $a \in \agents$.
\end{definition}
Let $d \geq \maxdens{\vset}{M}$. In particular, this means for each $a \in \agents$, $d \geq \maxdens{\vset_{a}}{M}$. Thus,
by \Cref{prop:puequiv}, $U_{\vset}(M,d)$ and $\vset$ agree on $M$.
We now show that $U_{\vset}(M,d)$ is \hyperlink{def:er}{easily replaceable} on $M$.
If for each $m \in \noz{M}$, we set $l_{a}(m_{i}) \triangleq m_{i} - V[m_{i - 1}, m_{i}]/d$, then
\[P(U_{\vset}(M,d)_{a}) = \bigcup_{m \in \noz{M}}[l_{a}(m), m], \]
which satisfies condition (1). To satisfy condition (2), we note that by \Cref{prop:uconst}, $c(U_{\vset}(M,d)_{a}) = d$ for all $a$. This shows that $U_{\vset}(M,d)$ is easily replaceable on $M$.
\subsection{Formula simplification}
\label{app:simpl}
Before proving any theorems about simplification, we write the definition for $\pnt(t)$ and $\pnt(f)$ more carefully.
\begin{definition}
Let $t \in R_{\mathtt{Intvl}}$. Then $\pnt(t) = \{t_1, t_2\}$, where $t = [t_1, t_2]$ and $t_1, t_2 \in R_{\mathtt{Intvl}}$.
Let $t \in R_{\mathtt{Piece}}$. Then
\begin{align*}
\pnt(t) \triangleq \pnt(t_1)\cup \cdots \cup \pnt(t_{n})
\end{align*}
where $t = \cup t_1 ,\ldots ,t_{n}$ for $t_{i} \in R_{\mathtt{Intvl}}$.
Let $t\in R_{\mathtt{s}}$. We define $\pnt(t)$ as the union of all $\pnt(t')$ for $t'$ an interval or point in $t$. For a simplified formula $f$, we let $\pnt(f)$ denote the union of $\pnt(t)$ for all terms $t$ in $f$. We refer to the elements of $\pnt(f)$ as \emph{point atoms}.
\end{definition}

We first aim to prove the following theorem:
\purepsound*
This requires the following lemma.
\begin{lemma}
\label{prop:techsum}
Suppose we have $\con{S}{\assn}{\uset}$.
If $t \in R_{\mathtt{Piece}}$ and $\pnt(t)\subseteq S$, let $\underline{S}|_{t} = \{y \in S|_{t} \mid \forall y' \in S.\assn(y) = \assn(y') \Rightarrow y \leq_{S} y' \}$. Then
\[
\uset_{a}(\sem{t}^{\assn}) = c(\uset_{a})\sum_{y \in \underline{S}|_{t}} \assn(y) - \assn(z_{a,y}).
\]
\end{lemma}
\begin{proof}
Before proceeding, we give a formula for $\uset_{a}(\sem{t}^{\assn})$. Write $t = \cup [y_1, y'_{1}],\ldots ,[y_{n},y'_{n}]$ and let $\assn(S)|_{t} = \{m \in \assn(S) \mid \assn(y_{i}') \geq m > \assn(y_{i})\ \text{for some}\ 1\leq i \leq n\}$. Since $\sem{t}^{\assn} = \bigcup_{i = 1}^{n} [\assn(y_{i}),\assn(y_{i}')]$ and $\pnt(t)\subseteq S$, we have that $\partial\sem{t}^{\assn}\subseteq \assn(S)$. Therefore by (1) and by \Cref{eq:pusum}, we have
\[
\uset_{a} (\sem{t}^{\assn}) =  c(\uset_{a})\cdot \sum_{m \in \assn(S)|_{t}} (m - l_{a}(m)).
\]
To complete this argument, it suffices to show that $\assn$ gives a bijection between $\assn(S)|_{t}$ and $\underline{S}|_{t}$, for if $\assn(y) = m\in M$ and $y = \min\{y' \in S \mid \assn(y') = m\}$ then $\assn(y) - \assn(z_{a,y}) = m - l_{a}(m)$ according to (2), agreeing with the summand above.

Let $y \in \underline{S}|_{t}$. As $y \in S|_{t}$, we have $y_{i}' \geq_{S} y >_{S} y_{i}$ for some $1 \leq i \leq n$. By (4), $\assn(y'_{i}) \geq \assn(y) \geq \assn(y_{i})$. It also must be that $\assn(y) > \assn(y_{i})$, as $y = \min\{y' \in S\mid \assn(y') = m\}$. Therefore $\assn(y) \in \assn(S)|_{t}$.
Thus, $\assn|_{\underline{S}|_{t}} : \underline{S}|_{t} \to \assn(S)|_{t}$. It remains to show that $\assn|_{\underline{S}|_{t}}$ is injective and surjective.

Injectivity is almost immediate.  Since $>_{S}$ is a total order, $\min \{y' \in S\mid \assn(y') = m\}$ is unique for each $m \in \assn(S)$. Therefore $\underline{S}|_{t}$ contains at most one $y$ such that $\assn(y) = m$ for each $m \in \assn(S)$.

Let $m \in \assn(S)|_{t}$. Let $y_{m} = \min \assn|_{S}^{-1}(m)$. If we show that $y_{m}\in \underline{S}|_{t}$, surjectivity is established. As $m \in \assn(S)|_{t}$, $\assn(y_{i}') \geq m > \assn(y_{i})$ for some $1 \leq i \leq n$. Hence $\assn(y_{i}') \geq \assn(y_{m}) > \assn(y_{i})$, so by (4), $y' \geq_{S} y_{m} >_{S} y$. This means $y_{m} \in \sub{y}{y'}\subseteq S|_{t}$. As $y_{m} = \min \assn|_{S}^{-1}(m)$, $y_{m} \in \underline{S}|_{t}$. This completes the proof.
\qed
\end{proof}

\begin{proof}[\Cref{prop:purepsound}]
Let $\interp = \interp_{\uset}$.
As $f$ is simplified, it only consists of predicates of the form given in \Cref{prop:lra}. $S$ does nothing to predicates of the form $\sum_{i}r_{i}d_{i} \geq \sum_{j}r_{j}d_{j}$, so we focus on those of the form
\[
\sum_{i}r_{i}\val_{a_{i}}(t_{i}) \geq \sum_{j} r_{j}\val_{a_{j}}(t_{j}),
\]
for $t_{i}$,$t_{j}\in R_{\mathtt{Intvl}}\cup R_{\mathtt{Piece}}$. Without loss of generality, we can assume that $t_{i}, t_{j} \in R_{\mathtt{Piece}}$, for if $t \in R_{\mathtt{Intvl}}$, then $\sem{\val_{a}(t_{i})}_{\interp}^{\assn} = \sem{\val_{a}(\cup t_{i})}_{\interp}^{\assn}$.
We know that $\pnt(f) \subseteq S$ so $\pnt(t_{i})\subseteq S$ and $\pnt(t_{j})\subseteq S$ for all $i$ and $j$. Let $P_{i} = \sem{t_{i}}^{\assn}$ and $P_{j} = \sem{t_{j}}^{\assn}$.
Let $\underline{S}|_{t} = \{y \in S|_{t} \mid \forall y' \in S. \assn(y) = \assn(y') \Rightarrow y \leq_{S} y'\}$.
We have
\begin{align*}
\sem{S(\val_{a_{i}}(t_{i}))}_{\interp}^{\assn}
&= \sum_{y\in S|_{t_{i}}} \assn(y) - \assn(z_{a_{i},y}) \\
&= \sum_{y\in \underline{S}|_{t}} \assn(y) - \assn(z_{a_{i},y}) + \sum_{y\in S|_{t_{i}}\setminus \underline{S}|_{t}} \assn(y) - \assn(z_{a_{i},y}) \\
&= \sum_{y \in \underline{S}|_{t}} \assn(y) - l_{a_{i}}(\assn(y)) + \sum_{y \in S|_{t} \setminus \underline{S}|_{t}} \assn(y) - \assn(y) \\
&= {{\uset}}_{a_{i}}(P_{i})/ d
\end{align*}
where we use $\con{S}{\assn}{\uset}$ (2) and (3) for the third equality, and \Cref{prop:techsum} for the fourth equality.
\begin{align*}
\sem{S(\val_{a_{j}}(t_{j}))}_{\interp}^{\assn} = {{\uset}}_{a_{j}}(P_{j})/ d.
\end{align*}

\begin{align*}
&\interp,\assn \vDash \sum_{i}r_{i}\val_{a_{i}}(t_{i}) \geq   \sum_{j}r_{j}\val_{a_{j}}(t_{j}) \\
&\iff \sem{\sum_{i}r_{i}\val_{a_{i}}(t_{i})}_{\interp}^{\assn} \geq \sem{\sum_{j}r_{j}\val_{a_{j}}(t_{j})}_{\interp}^{\assn} \\
&\iff \sum_{i} r_{i} {\uset}_{a_{i}}(P_{i}) \geq \sum_{j} r_{j} {{\uset}}_{a_{j}}(P_{j}) \\
&\iff \sum_{i} r_{i} \sem{S(\val_{a_{i}}(t_{i}))}_{\interp}^{\assn}\geq \sum_{j} r_{j} \sem{S(\val_{a_{j}}(t_{j}))}_{\interp}^{\assn}\\
&\iff \interp,\assn \vDash S\left(\sum_{i}r_{i}\val_{a_{i}}(t_{i}) \geq   \sum_{j}r_{j}\val_{a_{j}}(t_{j})\right).
\end{align*}
This completes our argument.
\qed
\end{proof}

We now aim to prove the following theorem:
\simplsolvingenvy*

Like with \Cref{prop:solvingenvy}, we generalize to well-formed properties:
\begin{restatable}[]{theorem}{simplsolvingthm}
Suppose $e$ is well-formed and $\cdot \vdash e : \tau$. Let $F$ be a well-formed property such that $x : \mathtt{s}_{\tau}; \cdot \vdash F : \text{Formula}$. Then
\begin{equation}
\label{eq:pusolving}
\vDash \bigwedge_{b \in B(e)}  \bigwedge_{S \in S_{b}} \forall \mathcal{Y}_{b}.S(\simpl(\cn(b)\wedge \conj(S) \Rightarrow F\fsub{x}{\rho(b)}))
\end{equation}
if and only if $e \vDash F$.
\label{prop:simplsolving}
\end{restatable}
Here we state and prove some results which help connect points in programs to points in their constraints.
\begin{lemma}
For any interpretation $\interp$, if $\con{S}{\assn}{{\uset}}$, then
\[ \interp , \assn \vDash \conj(S).\]
\label{prop:orderformula}
\end{lemma}
\begin{proof}
Straightforward from the construction of $U_{\vset}(M,d)$ and the definition of $\con{S}{\assn}{\uset}$.
\qed
\end{proof}

\begin{lemma}
\label{prop:dmarks}
Suppose $D : b \eval_{\vset} \v$. Then $M(D) = \{r\pnt \mid \emark{a}{b_1}{b_2}\# s \eval r\pnt\ \text{occurs in}\ D\}\cup M(b)$.
\end{lemma}
\begin{proof}
Let $M(D)' \triangleq \{r\pnt \mid \emark{a}{e_1}{e_2}\# s\eval r\pnt\ \text{occurs in}\ D\}\cup M(e)$.
This argument proceeds by induction on $D$.
\begin{description}
\item[\rname{E-Val}]
First note that $\{ r \mid r\pnt\ \text{appears in}\ \v\} = M(\v)$. And then observe that if $D : \v \eval \v$, then
$\{ r \mid r\pnt\ \text{appears in}\ \v\} = \{ r \mid r\pnt\ \text{appears in}\ \v, \v\ \text{appears in}\ D\}$. Therefore, $M(D) = M(\v) = M(e)$ in this case.

\item[\rname{E-Ops}]
Then $e  = o(e_1 ,\ldots ,e_{n})$, $D_{i} : e_{i} \eval \v_{i}$, and $\v = \sem{o}(\v_1,\ldots ,\v_{n})$ for some $o \in O$.
Inspection of the allowed operations enables us to claim that $r\pnt$ only occurs in $\v$ if it occurs also in $\v_{i}$ for some $i$.
Therefore, $M(D) = M(D_1)\cup \cdots M(D_{n})$. Also, $M(D)' =M(D_1)'\cup \cdots \cup M(D_{n})'$. By induction, $M(D_{i}) = M(D_{i})'$, concluding this case.

\item[\rname{E-Mark}] Then $e = \emark{a}{e_1}{e_2} \# s $,  $\v = r\pnt$, $D_1 : e_1 \eval \rd{[r_1,r'_{1}]}$, $D_2 : e_2 \eval \vset_{a'}(P)$, and $\vset_{a}[r_1,r] = \vset_{a'}(P)$. Let $\pnt(P)$ be the set of points within $P$.
Now $M(D) = M(D_1)\cup M(D_2)\cup \{ r_1\pnt, r'_1\pnt, r\pnt\}\cup \pnt(P)$. Since $D_2 : e_2 \eval \vset_{a'}(P)$, $\pnt(P) \subseteq M(D)'$. Since $D_1 : e_1 \eval \rd{[r_1, r'_{1}]}$, we have $r_1, r'_{1}\in M(D_1)$. Therefore, $M(D)=  M(D_1)\cup M(D_2)\cup \{r\pnt\}$.
We also have $M(D)' = M(D_1)'\cup M(D_2)'\cup \{r\pnt\}$.
By induction, $M(D_1) = M(D_1)'$ and $M(D_2) = M(D_2)'$. This completes the case.

\item[\rname{E-EvalPc}]
Then $e = \eeval{a}{e'}$, $\v = \vset_{a}(P)$, and $D' :e' \eval P$. Let $\pnt(P)$ be the set of points in $P$. Then $M(D) = M(D')\cup \pnt(P)$. Since $D' : e' \eval P$, $\pnt(P) \subseteq M(D')$. Therefore $M(D) = M(D')$. Now $M(D)' = M(D')'$. By induction, $M(D')' = M(D')$, so we can conclude this case.
\item[\rname{E-EvalIntvl}] The argument is very similar to the argument for \rname{EvalPc}.

\item[\rname{E-Div}]
Then $e = \ediv{e_1}{e_2}$, $\v = ([r_1, r_2], [r_2, r_1'])$, $D_1 : e_1 \eval [r_1, r'_{1}]$, and $D_2 : e_2 \eval r_2\pnt$. Then $M(D) = M(D_1)\cup M(D_2)\cup \{r_1, r_1', r_2\}$. Since $D_1 : e_1 : \eval [r_1, r_1']$, $\{r_1, r_1'\}\subseteq M(D_1)$, and as $D_2 : e_2 \eval r_2\pnt$, we have $r_2\pnt \in M(D_2)$. Therefore $M(D) = M(D_1) \cup M(D_2)$.
Now $M(D)' = M(D_1)' \cup M(D_2)'$. By induction, $M(D_1) = M(D_1)'$ and $M(D_2) = M(D_2)'$. This case is then complete.
\item[\rname{E-Split}]
Then $e = \kwlet\ x_1 ,\ldots ,x_{n}, w_1,\ldots ,w_{n'} = \kwsplit\ e_1\ \kwin\ e_2$, $D_1 : e_1 \eval (\v_1 ,\ldots ,\v_{n + n'})$, $D_2 : S_{\var}S_{\rd{\lvar}}S_{\lvar}(e_2) \eval \v$, where
\begin{align*}
S_{\var} &\triangleq \{x_{i} \mapsto \v_{i}\mid 1 \leq i \leq n\} \\
S_{\rd{\lvar}} &\triangleq \{\rd{w_{i}} \mapsto \rd{\v_{n +i}}\mid 1 \leq i \leq n'\} \\
S_{\var} &\triangleq \{w_{i} \mapsto \v_{n + i}\mid 1 \leq i \leq n'\}.
\end{align*}
Now $M(D) = M(D_1)\cup M(D_2)$, and $M(D)' = M(D_1)'\cup M(D_2)'\cup M(e_2)$. Since $M(D_2)'\supseteq M(S_{\var}S_{\rd{\lvar}}S_{\lvar}(e_2))$ and $M(S_{\var}S_{\rd{\lvar}}S_{\lvar}(e_2))\supseteq M(e_2)$, we have $M(D)' = M(D_1)' \cup M(D_2)'$. By induction, $M(D_1) = M(D_1)'$ and $M(D_2) = M(D_2)'$, completing this case.
\qed
\end{description}
\end{proof}

\begin{lemma}
Suppose that $D : b \eval \v$. Suppose that $\assn$ is a variable assignment that agrees with $D$. Then $M(D) \subseteq M(b)\cup \assn( \{y_{\#s}\in \mathcal{Y}\mid \# s \in \id(b)\})$.
\label{prop:mpoints}
\end{lemma}
\begin{proof}
According to \Cref{prop:dmarks}, $M(D) = M(b) \cup \{r \mid \emark{a}{b_1}{b_2}\#s \eval r\pnt\ \text{occurs in}\ D \}$. Therefore we just have to show
\[
\{r \mid \emark{a}{b_1}{b_2}\#s \eval r\pnt\ \text{occurs in}\ D \} \subseteq  \assn( \{y_{\#s}\in \mathcal{Y}\mid \# s \in \id(b)\}).
\]
So let $r$ be in the left hand side. Then $\emark{a}{b_1}{b_2}\# s \eval r\pnt$ occurs in $D$. We have $\#s \in \id(b)$ and since $\assn$ agrees with $D$, we have that $\assn(y_{\#s}) = r\pnt$. Therefore $r\pnt$ is in the right hand side. This completes the argument.
\qed
\end{proof}

\begin{lemma}
\label{prop:yvarids}
For any path $b$, $\fv(\rho(b))\cap \mathcal{Y} \subseteq \fv(\cn(b))\cap \mathcal{Y}$, and $\fv(\cn(b))\cap \mathcal{Y} = \{ y_{\# s} \in \mathcal{Y} \mid \# s \in \id(b)\}$.
\end{lemma}
\begin{proof}
Straightforward. \qed
\end{proof}

\begin{lemma}
Let $\pnt(b)$ be the set of point values contained in $\cn(b)$ and $\rho(b)$. Then $\pnt(b) \subseteq M(b)$.
\end{lemma}
\begin{proof}
This argument goes by induction on the structure of $b$ and is straightforward.
\qed
\end{proof}

\begin{proof}[\Cref{prop:simplsolving}]
Suppose that $e \eval_{\vset} \v$. By \Cref{prop:path}, there is $b \in B(e)$ such that $D : b \eval_{\vset} \v$.

Let $\assn'$ be a variable assignment that agrees with $D$ and let $S$ be any piecewise uniform substitution on $\mathcal{Y}_{b}$ whose order is such that if $\assn'(y) < \assn'(y')$, then $y <_{S} y'$.
By \Cref{prop:mpoints}, $\mathcal{Y}_{b} = \{y_{\# s}\mid \#s \in \id(b)\}$, so by \Cref{prop:yvarids}, $M(D) \subseteq \assn'(\mathcal{Y}_{b})$. Let $M = \assn'(\mathcal{Y}_{b})$.
By \Cref{prop:puexists}, there is a valuation set $\uset$ that agrees with $\vset$ on $M$ and is easily replaceable on $M$.
By \Cref{thm:red}, $D : b \eval_{\uset} \v$.
Now let $\assn$ be any assignment that agrees with $\assn'$ on all of $\mathcal{Y}_{b}$, but assigns $z_{a,y}$ for all $a \in \agents$ and $y\in S$ such that $\con{S}{\assn}{\uset}$. This is possible since $\mathcal{Z}$ is disjoint from $\mathcal{Y}$ and for each $a$ and $y$, there is a unique $z_{a,y}\in \mathcal{Z}$.
Let $\interp = \interp_{\uset}$.
By \Cref{prop:soundness}, $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$ and $\interp, \assn \vDash \cn(b)$.
By \Cref{prop:simpl}, $\sem{\simpl(\rho(b))}_{\interp}^{\assn} = \unrd{\v}$ and $\interp,\assn\vDash \simpl(\cn(b))$. By \Cref{prop:orderformula}, $\interp, \assn \vDash \conj(S)$. Then we have
\begin{align*}
&\interp,\assn \vDash S(\simpl(\cn(b)\land \conj(S))) \tag{\Cref {prop:purepsound}} \\
&\interp, \assn \vDash S(\simpl (F\fsub{x}{\rho(b)})) \tag{\Cref{eq:pusolving}} \\
&\interp \vDash \simpl (F\fsub{x}{\rho(b)}) \tag{\Cref {prop:purepsound}} \\
&\interp \vDash F\fsub{x}{\rho(b)} \tag{\Cref{prop:simpl}}
\end{align*}
and by \Cref{prop:semsub} as $\sem{\rho(b)}_{\interp}^{\assn} = \unrd{\v}$,
\[
\interp \vDash F\fsub{x}{\lv}.
\]
Now $\cdot \vdash F\fsub{x}{\lv} : \text{Formula}$ so that $\cdot \vdash F : \text{Formula}$. Since $F$ is well-formed, $F$ contains no point values. Therefore all point values are contained within $\lv$. This allows us to apply \Cref{thm:pufequiv} to obtain
\[
\interp_{\vset} \vDash F\fsub{x}{\lv}.
\]

We approach this by assuming \Cref{eq:pusolving} does not hold and constructing a piecewise uniform valuation set witness to $e \not\vDash F$.
So suppose that \Cref{eq:pusolving} does not hold. Observe that \Cref{eq:pusolving} does not contain any $\val$ function symbols. Then there is some $\assn$, $b \in B(e)$, and $S\in S_{b}$ such that $\assn \vDash S(\simpl(\cn(b)))\land \conj(S)$ yet $ \assn \not\vDash F\fsub{x}{\rho(b)}$.
Write out $S = \{y_1 ,\ldots ,y_{n}\}$ such that $y_1 <_{S} \cdots <_{S} y_{n}$.
Consider the piece
\[
[\assn(z_{a,y_{1}}), \assn(y_{1})]\cup \cdots \cup [\assn(z_{a,y_{n}}), \assn(y_{n})].
\]
As $\assn\vDash \conj(S)$,
\begin{equation}
\assn(z_{a,y_{1}}) \leq \assn(y_{1}) \leq \cdots \leq \assn(z_{a,y_{n}}) \leq \assn(y_{n}).
\label{eq:witnessineq}
\end{equation}
Then let $U_{a}$ be the piecewise uniform valuation on the above piece.
Also observe by $\assn \vDash \conj(S)$, for any $a, a'$,
\[
\sum_{y \in S} \assn(y) - \assn(z_{a,y}) = \sum_{y \in S} \assn(y) - \assn(z_{a',y}).
\]
Therefore we can set $d$ to be the reciprocal of the above sum, and obtain that $d = c(U_{a})$ for all $a$.
Then $\uset \triangleq (a \mapsto U_{a}\mid a \in \agents)$ is a piecewise uniform valuation set which is easily replaceable on $\assn(S)$. Set $\interp = \interp_{U}$.

We can verify that $\con{S}{\assn}{U}$:
(1) is satisfied directly above.
(2) is also satisfied by definition.
(3) is mildly more difficult. Let $y \in \mathcal{Y}_{b}$ be such that there is $y' <_{S}y$ and $\assn(y') = \assn(y)$. Then $\assn(y') \leq \assn(z_{a,y})\leq \assn(y)$ hence $\assn(z_{a,y}) = \assn(y)$ for all $a \in \agents$.
(4) is verified by \Cref{eq:witnessineq} recalling that $y_1 <_{S} \cdots <_{S} y_{n}$.

Then by \Cref{prop:purepsound},
\[
\interp,\assn\vDash \simpl(\cn(b))\quad \text{and}\quad \interp,\assn \not\vDash \simpl(F\fsub{x}{\rho(b)}).
\]
By \Cref{prop:simpl},
\[
\interp,\assn\vDash \cn(b)\quad \text{and}\quad \interp,\assn \not\vDash F\fsub{x}{\rho(b)}.
\]
Therefore by \Cref{prop:completeness}, $b \eval_{\uset} \v$ where $\unrd{\v} = \sem{\rho(b)}_{\interp}^{\assn}$. By \Cref{prop:path}, $e \eval_{\uset} \v$. By \Cref{prop:semsub}, $\interp,\assn \not\vDash F\fsub{x}{\lv}$. Since $F\fsub{x}{\lv}$ has no unbound variables, $\assn$ is redundant. Therefore $\interp \not\vDash F\fsub{x}{\lv}$. This shows that $e \not\vDash F$.
\qed
\end{proof}

We also have the following generalization of \Cref{cor:decidable}
\begin{restatable}[]{corollary}{decidable}
Let $e$ be a well-formed protocol, only using standard operations, and let $F$ a well-formed property. Checking if $e$ satisfies $F$ is decidable.
\end{restatable}

\subsection{Evaluation of protocols with envy}
\label{app:exp}

\subsubsection{Non-Envy Free Protocols.}
To demonstrate the proficiency of our approach for finding envy, we deliberately incorporated errors into select protocols and time how long it takes to find envy, following methodology established by Lester~\cite{Lester}. The results, contained in \Cref{tab:experiment2}, demonstrate that our approach can also efficiently find envy in all protocols tested.

\begin{table}[htbp]
\centering
\caption{Time to find counterexamples to non-envy-free protocols.}
\begin{tabular}{@{}lrl@{}}
\toprule
{Protocol} & {Time} & {Description} \\
\midrule
Cut-Choose & 0.020 & Agent 1 cuts and chooses. \\
Cut-Choose & 0.021 & Slices allocated wrong way round in one branch. \\
Surplus    & 0.035 & Unsafe trim of slice smaller than reference. \\
Selfridge-Conway-Surplus        & 0.034 & Allocates trimmings of slice instead of trimmed slice. \\
Selfridge-Conway-Surplus        & 0.033 & Agent 2 not forced to take trimmed slice if available. \\
Selfridge-Conway-Full        & 0.161 & Trimmings cut by agent who took trimmed slice. \\
Aziz-Mackenzie-3 & 2.594 & Did not check if Agent 1 and 2 has the same favorite piece. \\
\bottomrule
\end{tabular}
\label{tab:experiment2}
\end{table}

\fi
\end{document}