$\displaystyle\zeta\circ\gamma(\sigma,t_{1},\dots,t_{n})=\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))\sqsubseteq_{\mathsf{IN}}\sigma(\zeta(s_{1}),\dots,\zeta(s_{n}))=\zeta\circ\gamma(\sigma,s_{1},\dots,s_{n})$

by monotonicity of $\zeta$.

For the fixed-point operators, let $t_{1}\leq_{!}t_{2}$ and
$\mathsf{v}\in\mathsf{Var}$.

$\displaystyle\zeta\circ\gamma(\beta\mathsf{v},t_{1})=\operatorname{lfp}_{\mathsf{v}}\zeta(t_{1})\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}\zeta(t_{2})=\zeta\circ\gamma(\beta\mathsf{v},t_{2})$

Monotonicity of $\gamma(\mu\mathsf{v},-)$ is trickier: it follows from the
more general observation that if $t_{1}\leq_{!}t_{2}$, $\mathsf{v}$ is guarded
in both $t_{i}$ (ie. there is a representative of $\zeta(t_{i})$ of the form
$p(\vec{\mathsf{u}},\langle\mathsf{a}_{j},r_{j}\rangle_{j\leq n})$ with
$\mathsf{v}\notin\vec{\mathsf{u}}$), and
$\zeta(s_{i})=\zeta(t_{i})\\{s_{i}\mathbin{/\\!/}\mathsf{v}\\}$ for $i=1,2$,
then $s_{1}\leq_{!}s_{2}$.

To show this, we need to reach into the _final sequence_ of $B_{M}$, the
$(\omega+\omega)^{op}$-chain in the top row of the following diagram

${Z_{0}}$${Z_{1}}$${Z_{2}}$${\cdots}$${Z_{\omega}}$${\cdots}$${Z}$${Z}$${B_{M}Z}$${B_{M}^{2}Z}$${\cdots}$${B_{M}^{\omega}Z}$${\cdots}$$\scriptstyle{\alpha_{10}}$$\scriptstyle{\alpha_{21}}$$\scriptstyle{\alpha_{\omega
n}}$$\scriptstyle{\alpha_{n}}$$\scriptstyle{\zeta}$$\scriptstyle{{!}_{\zeta}^{0}}$$\scriptstyle{{!}_{\zeta}^{1}}$$\scriptstyle{{!}_{\zeta}^{2}}$$\scriptstyle{{!}_{\zeta}^{\omega}}$$\scriptstyle{\zeta^{2}}$$\scriptstyle{\zeta^{\omega+1}}$

in which $Z_{0}=(1,=)$ and ${!}_{\zeta}^{0}$ is the unique map
$(Z,\leq_{!})\to(1,=)$, $Z_{n+1}=B_{M}(Z_{n},\leq)$ and
${!}_{\zeta}^{n+1}=B_{M}({!}_{\zeta}^{n})\circ\zeta$ , everything in the top
row is the limit of the cone to its left, and everything in the bottom row is
the colimit of the cocone to its left. We refer to ${!}_{\zeta}^{n}(t)$ as the
_$n$ th truncation_ of $t$. It was shown originally by Worrell that
$(Z,\leq_{!})$ is the limit of the diagram in the top row [33].

By the explicit construction of limits in $\mathbf{Pos}$, it suffices to show
that ${!}_{\zeta}^{n}(s_{1})\leq{!}_{\zeta}^{n}(s_{2})$ for all
$n<\omega+\omega$. Now, ${!}_{\zeta}^{0}(s_{1})\leq{!}_{\zeta}^{0}(s_{2})$
trivially, so we can immediately move on to the inductive steps. If
${!}_{\zeta}^{n}(s_{1})\leq{!}_{\zeta}^{n}(s_{2})$, then

$\displaystyle{!}_{\zeta}^{n+1}(s_{1})$
$\displaystyle=B_{M}({!}_{\zeta}^{n})\circ\zeta(s_{1})$
$\displaystyle=B_{M}({!}_{\zeta}^{n})(\zeta(t_{1})\\{s_{1}\mathbin{/\\!/}\mathsf{v}\\})$
$\displaystyle=B_{M}({!}_{\zeta}^{n})(\zeta(t_{1}))\\{{!}_{\zeta}^{n}(s_{1})\mathbin{/\\!/}\mathsf{v}\\}$
($\mathsf{v}$ gdd in $t_{i}$)
$\displaystyle\sqsubseteq_{\mathsf{IN}}B_{M}({!}_{\zeta}^{n})(\zeta(t_{2}))\\{{!}_{\zeta}^{n}(s_{1})\mathbin{/\\!/}\mathsf{v}\\}$
$\displaystyle\sqsubseteq_{\mathsf{IN}}B_{M}({!}_{\zeta}^{n})(\zeta(t_{2}))\\{{!}_{\zeta}^{n}(s_{2})\mathbin{/\\!/}\mathsf{v}\\}$
(ih) $\displaystyle={!}_{\zeta}^{n+1}(s_{2})$

Note that we use a minor abuse of notation above to denote the substitution of
the $n$th truncation of $s_{i}$ for $\mathsf{v}$ in the second component of
the transitions $\langle\mathsf{a},r\rangle$ that appear in the (truncated)
branching of $t_{i}$ (or possibly $m$th truncation $s_{i}$ for $m<n$ at
further truncated sections of $t_{i}$). This is defined analogously to guarded
semantic substitution, so we write
$B_{M}({!}_{\zeta}^{n})(\zeta(t_{1}))\\{{!}_{\zeta}^{n}(s_{1})\mathbin{/\\!/}\mathsf{v}\\}$
to denote this substitution.

At the $\omega^{op}$-limit,
${!}^{\omega}_{\zeta}(s_{1})\leq{!}^{\omega}_{\zeta}(s_{2})$ because
${!}^{n}_{\zeta}(s_{1})\leq{!}^{n}_{\zeta}(s_{1})$ for all $n<\omega$. This
completes the proof because
$s_{1}={!}_{\zeta}(s_{1})\leq_{!}{!}_{\zeta}(s_{2})=s_{2}$ if and only if
${!}_{\zeta}^{n}(s_{1})\leq_{!}{!}_{\zeta}^{n}(s_{2})$ for all
$n<\omega+\omega$. So, in particular,

$\displaystyle\zeta\circ\gamma(\mu\mathsf{v},t_{1})$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}\zeta(t_{1})\\{\gamma(\mu\mathsf{v},t_{1})\mathbin{/\\!/}\mathsf{v}\\}$
$\displaystyle=\zeta(\gamma(\beta\mathsf{v},t_{1}))\\{\gamma(\mu\mathsf{v},t_{1})\mathbin{/\\!/}\mathsf{v}\\}$
$\displaystyle\sqsubseteq_{\mathsf{IN}}\zeta(\gamma(\beta\mathsf{v},t_{2}))\\{\gamma(\mu\mathsf{v},t_{2})\mathbin{/\\!/}\mathsf{v}\\}$
$\displaystyle=\zeta\circ\gamma(\mu\mathsf{v},t_{2})$

if $t_{1}\leq_{!}t_{2}$. ∎

See 5.1

###### Proof.

The proof is essentially the same as that of [1, Theorem 1], with the added
case of the unguarded loop. That is, we need to show that
$B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)\circ\epsilon(\beta\mathsf{v}~{}e)=\zeta\circ\gamma(\beta\mathsf{v},\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)$ given the analogous equation for $e$.

$\displaystyle\zeta(\gamma(\beta\mathsf{v},\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor))$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(e))$
$\displaystyle=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\operatorname{lfp}_{\mathsf{v}}\epsilon(e))$
$\displaystyle=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(\beta\mathsf{v}~{}e))$

by condition 2 of Definition 3.6. ∎

##  Appendix E Proofs from Section 4

######  Lemma E.1.

The small-step semantics map $\epsilon$ is monotone.

###### Proof.

We show that $e\sqsubseteq_{\exp}f$ implies
$\epsilon(e)\sqsubseteq_{\mathsf{IN}}\epsilon(f)$ by induction on the proof of
$e\sqsubseteq_{\exp}f$. The only interesting cases are in the inductive step
concerning congruence of $\beta\mathsf{v}$ and $\mu\mathsf{v}$, since
$\epsilon$ (by definition) commutes with the $S$-operations.

By induction and the monotonicity of $\operatorname{lfp}_{\mathsf{v}}$, we
have

$\epsilon(\beta\mathsf{v}~{}e)=\operatorname{lfp}_{\mathsf{v}}\epsilon(e)\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}\epsilon(f)=\epsilon(\beta\mathsf{v}~{}f)$

From monotonicity of $(-)[-\mathbin{/\\!/}\mathsf{v}]$, we glean that

$\epsilon(\mu\mathsf{v}~{}e)=\operatorname{lfp}_{\mathsf{v}}\epsilon(e)[\mu\mathsf{v}~{}e\mathbin{/\\!/}\mathsf{v}]\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}\epsilon(f)[\mu\mathsf{v}~{}e\mathbin{/\\!/}\mathsf{v}]\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}\epsilon(f)[\mu\mathsf{v}~{}f\mathbin{/\\!/}\mathsf{v}]=\epsilon(\mu\mathsf{v}~{}f)\qed$

##  Appendix F Proofs from Section 6

See 6.2

###### Proof.

Uniqueness follows from the surjectivity of $[-]_{\equiv}$, so it suffices to
show existence. We use a diagonal fill-in to produce the map $\bar{\epsilon}$
in the diagram

${(\mathsf{Exp},\sqsubseteq_{exp})}$${({\mathsf{Prc}},\sqsubseteq)}$${B_{M}(\mathsf{Exp},\sqsubseteq_{exp})}$${B_{M}({\mathsf{Prc}},\sqsubseteq)}$$\scriptstyle{\epsilon}$$\scriptstyle{[-]_{\equiv}}$$\scriptstyle{\bar{\epsilon}}$

This requires us to show that whenever $e\sqsubseteq f$, we must also have the
inequality
$B_{M}([-]_{\equiv})\circ\epsilon(e)\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(f)$.
We show this by induction on the proof of $e\sqsubseteq f$.

($\mathsf{\mathsf{IN}}$)

Suppose $e\sqsubseteq f$ follows from $e\sqsubseteq_{\mathsf{IN}}f$. Then,
since $\epsilon$ is an $S$-algebra homomorphism,
$\epsilon(e)\sqsubseteq_{\mathsf{IN}}\epsilon(f)$. By monotonicity of
$B_{M}([-]_{\equiv})$,
$B_{M}([-]_{\equiv})\circ\epsilon(e)\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(f)$.

($\mathsf{S}$)

Suppose $e=\sigma_{1}(e_{1},\dots,e_{n})$ and
$f=\sigma_{2}(e_{1},\dots,e_{n})$ and $\sigma_{1}\leq_{S}\sigma_{2}$. Again,
$\epsilon$ is an $S$-algebra homomorphism, so is by definition monotonic wrt
to the operation order. It follows that
$\epsilon(e)\sqsubseteq_{\mathsf{IN}}\epsilon(f)$. By monotonicity of
$B_{M}([-]_{\equiv})$,
$B_{M}([-]_{\equiv})\circ\epsilon(e)\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(f)$.

($\mathsf{Act}$)

Suppose $e=\mathsf{a}_{1}e_{1}$ and $f=\mathsf{a}_{2}e_{1}$. Then by
monotonicity of $\langle-\rangle$,
$\langle\mathsf{a}_{1},e_{1}\rangle\leq\langle\mathsf{a}_{2},e_{1}\rangle$.
Again, it follows that $\epsilon(e)\sqsubseteq_{\mathsf{IN}}\epsilon(f)$.

($\mathsf{R1a}$)

Suppose that $\mathsf{v}\in\mathsf{gd}(g_{i})$ for $i\leq n$ and
$e=\beta\mathsf{v}~{}p(\mathsf{v},\vec{g})$ and
$f=(\operatorname{lfp}_{\mathsf{v}}p)(\vec{g})$. Then

$\epsilon(e)=(\operatorname{lfp}_{\mathsf{v}}p)(\epsilon(g_{1}),\dots,\epsilon(g_{n}))=\epsilon((\operatorname{lfp}_{\mathsf{v}}p)(g_{1},\dots,g_{n}))$

because $\epsilon$ is an $S$-algebra homomorphism. Therefore,
$B_{M}([-]_{\equiv})\circ\epsilon(e)=B_{M}([-]_{\equiv})\circ\epsilon(f)$ as
desired.

($\mathsf{R1b}$)

Suppose $e=\mu\mathsf{v}~{}e_{1}$ and
$f=\beta\mathsf{v}~{}e_{1}[e\mathbin{/\\!/}\mathsf{v}]$. Then

$\epsilon(e)=\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1})[e\mathbin{/\\!/}\mathsf{v}]=\epsilon(\beta\mathsf{v}~{}e_{1})[e\mathbin{/\\!/}\mathsf{v}]=\epsilon(\beta\mathsf{v}~{}e_{1}[e\mathbin{/\\!/}\mathsf{v}])$

because $\epsilon$ is an $S$-algebra homomorphism. Therefore,
$B_{M}([-]_{\equiv})\circ\epsilon(e)=B_{M}([-]_{\equiv})\circ\epsilon(f)$ as
desired.

This concludes the base case. For the inductive case, assume
$B_{M}([-]_{\equiv})\circ\epsilon(e_{i})\leq
B_{M}([-]_{\equiv})\circ\epsilon(f_{i})$ for all $i\leq n$. We skip the
($\mathsf{P}$i) cases, as these are trivially true by assumption.

($\mathsf{C1}$)

Suppose $e=\sigma(e_{1},\dots,e_{n})$ and $f=\sigma(f_{1},\dots,f_{n})$. Since
$\epsilon$ is an $S$-algebra homomorphism and $B([-]_{\equiv})$ is a monotone
$S$-algebra homomorphism,

$\displaystyle B([-]_{\equiv})\circ\epsilon(e)$
$\displaystyle=B([-]_{\equiv})(\sigma(\epsilon(e_{1}),\dots,\epsilon(e_{n})))$
$\displaystyle=\sigma(B([-]_{\equiv})\circ\epsilon(e_{1}),\dots,B([-]_{\equiv})\circ\epsilon(e_{n}))$
$\displaystyle\sqsubseteq_{\mathsf{IN}}\sigma(B([-]_{\equiv})\circ\epsilon(f_{1}),\dots,B([-]_{\equiv})\circ\epsilon(f_{n}))$
$\displaystyle=B([-]_{\equiv})\circ\epsilon(f)$

($\mathsf{C2}$)

Suppose $e=\mathsf{a}e_{1}$ and $f=\mathsf{a}f_{1}$. Then

$\displaystyle B([-]_{\equiv})\circ\epsilon(e)$
$\displaystyle=B([-]_{\equiv})(\langle\mathsf{a},e\rangle)$
$\displaystyle=\langle\mathsf{a},[e]_{\equiv}\rangle$
$\displaystyle\leq\langle\mathsf{a},[f]_{\equiv}\rangle$
$\displaystyle=B([-]_{\equiv})\circ\epsilon(f)$

by monotonicity of $\eta$.

($\mathsf{C3}$)

Suppose $e=\beta\mathsf{v}~{}e_{1}$ and $f=\beta\mathsf{v}~{}f_{1}$. We have

$\displaystyle B([-]_{\equiv})\circ\epsilon(e)$
$\displaystyle=B([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1}))$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}B_{M}([-]_{\equiv})\circ\epsilon(e_{1})$
$\displaystyle\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}B_{M}([-]_{\equiv})\circ\epsilon(f_{1})$
$\displaystyle=B([-]_{\equiv})\circ\epsilon(f)$

($\mathsf{C4}$)

Suppose $e=\mu\mathsf{v}~{}e_{1}$ and $f=\mu\mathsf{v}~{}f_{1}$. Then

$\displaystyle B([-]_{\equiv})\circ\epsilon(e)$
$\displaystyle=B([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1})[e\mathbin{/\\!/}\mathsf{v}])$
$\displaystyle=B([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1}))[[e]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}B([-]_{\equiv})\circ\epsilon(e_{1})[[e]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}B([-]_{\equiv})\circ\epsilon(f_{1})[[e]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle\sqsubseteq_{\mathsf{IN}}\operatorname{lfp}_{\mathsf{v}}B([-]_{\equiv})\circ\epsilon(f_{1})[[f]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=B([-]_{\equiv})\circ\epsilon(f)$

($\mathsf{R2a}$)

Suppose $e=\beta\mathsf{v}~{}p(v,\vec{f})$ and $f=g$ and
$p(g,\vec{f})\sqsubseteq g$, and assume that

$B_{M}([-]_{\equiv})\circ\epsilon(p(g,\vec{f}))\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(g).$

Then we have

$\displaystyle B([-]_{\equiv})\circ\epsilon(e)$
$\displaystyle=B([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(p(\mathsf{v},\vec{f})))$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}(B([-]_{\equiv})\circ\epsilon(p(\mathsf{v},\vec{f})))$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}(B([-]_{\equiv})\circ
p(\mathsf{v},\epsilon(\vec{f})))$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}(p(v,B([-]_{\equiv})\circ\epsilon(\vec{f})))$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}p(B([-]_{\equiv})\circ\epsilon(\vec{f}))$

In other words, $B([-]_{\equiv})\circ\epsilon(e)$ is the least fixed-point of
$p(\mathsf{v},B([-]_{\equiv})\circ\epsilon(\vec{f}))$, so it suffices to show
that $B_{M}([-]_{\equiv})\circ\epsilon(g)$ is another prefixed-point. To this
end, compute

$\displaystyle B_{M}([-]_{\equiv})\circ\epsilon(p(g,\vec{f}))$
$\displaystyle=B_{M}([-]_{\equiv})(p(\epsilon(g),\epsilon(\bar{f})))$
$\displaystyle=p(B_{M}([-]_{\equiv})\circ\epsilon(g),B_{M}([-]_{\equiv})\circ\epsilon(\bar{f}))$

By assumption, then,

$p(B_{M}([-]_{\equiv})\circ\epsilon(g),B_{M}([-]_{\equiv})\circ\epsilon(\bar{f}))\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(g)$

It follows that
$B([-]_{\equiv})\circ\epsilon(e)\sqsubseteq_{\mathsf{IN}}B([-]_{\equiv})\circ\epsilon(g)$.

($\mathsf{R2b}$)

Suppose $e=\mu\mathsf{v}~{}e_{1}$ and $f=g$ and
$\beta\mathsf{v}~{}e_{1}[g\mathbin{/\\!/}\mathsf{v}]\sqsubseteq g$, and assume
that

$B_{M}([-]_{\equiv})\circ\epsilon(\beta\mathsf{v}~{}e_{1}[g\mathbin{/}\mathsf{v}])\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(g).$

We have

$\displaystyle B_{M}([-]_{\equiv})\circ\epsilon(e)$
$\displaystyle=B_{M}([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1})[e\mathbin{/\\!/}\mathsf{v}])$
$\displaystyle=B_{M}([-]_{\equiv})(\beta{\mathsf{v}}~{}\epsilon(e_{1}))[[e]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})(\beta{\mathsf{v}}~{}\epsilon(e_{1}))[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=B_{M}([-]_{\equiv})(\beta{\mathsf{v}}~{}\epsilon(e_{1})[g\mathbin{/\\!/}\mathsf{v}])$
$\displaystyle\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})(g)$

($\mathsf{R3}$)

Suppose $e=g$ and $f=\mu\mathsf{v}~{}e_{1}$, and assume that
$g\sqsubseteq\beta\mathsf{v}~{}e_{1}[g\mathbin{/\\!/}\mathsf{v}]$ and

$B_{M}([-]_{\equiv})\circ\epsilon(g)\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})\circ\epsilon(\beta\mathsf{v}~{}e_{1}[g\mathbin{/\\!/}\mathsf{v}])$

Then we have

$\displaystyle B_{M}([-]_{\equiv})\circ\epsilon(g)$ $\displaystyle\leq
B_{M}([-]_{\equiv})\circ\epsilon(\beta\mathsf{v}~{}e_{1}[g\mathbin{/\\!/}\mathsf{v}])$
$\displaystyle=B_{M}([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1})[g\mathbin{/\\!/}\mathsf{v}])$
$\displaystyle=B_{M}([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1}))[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle\sqsubseteq_{\mathsf{IN}}B_{M}([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1}))[[\mu\mathsf{v}~{}e_{1}]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=B_{M}([-]_{\equiv})(\operatorname{lfp}_{\mathsf{v}}\epsilon(e_{1})[\mu\mathsf{v}~{}e_{1}\mathbin{/\\!/}\mathsf{v}])$
$\displaystyle=B_{M}([-]_{\equiv})\circ\epsilon(\mu\mathsf{v}~{}e_{1})\qed$

#### Proof of Completeness

We now turn our attention to the details of steps 1 through 4 in Section 6,
beginning with the association of each ordered process with a system of
equations. Given a poset $(X,\leq)$ of _indeterminates_ , the underlying set
of the poset $\mathsf{Exp}(X,\leq)$ is given by the grammar

$x\mid\mathsf{v}\mid\mathsf{a}e\mid\sigma(e_{1},\dots,e_{n})\mid\beta\mathsf{v}~{}e\mid\mu\mathsf{v}~{}e\qquad\qquad(x\in
X)$

and partially ordered by the smallest precongruence extending $\leq_{\exp}$
and the partial order $\leq$ on $X$. For any
$h:(X,\leq)\to(\mathsf{Exp},\leq_{\exp})$, we define a map
$h^{\\#}:\mathsf{Exp}(X,\leq)\to(\mathsf{Exp},\leq_{\exp})$ by simultaneously
substituting indeterminates for expressions, ie.

$h^{\\#}(x)=h(x)\qquad h^{\\#}(\mathsf{v})=\mathsf{v}\qquad
h^{\\#}(\mathsf{a}e)=\mathsf{a}~{}h^{\\#}(e)\qquad
h^{\\#}(\sigma(\vec{e}))=\sigma(h^{\\#}(e_{1}),\dots,h^{\\#}(e_{n}))$

and $h^{\\#}(\beta\mathsf{v}~{}e)=\beta\mathsf{v}~{}h^{\\#}(e)$ and
$h^{\\#}(\mu\mathsf{v}~{}e)=\mu\mathsf{v}~{}h^{\\#}(e)$ for any $x\in X$ and
$e,e_{i}\in\mathsf{Exp}(X,\leq)$.

######  Definition F.1.

A _(monotone) system of equations (with indeterminates from)_ $(X,\leq)$ is a
map $s:(X,\leq)\to\mathsf{Exp}(X,\leq)$. A map
$\phi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$ is a _solution_ to $s$ if
$\phi\equiv\phi^{\\#}\circ s$. We say that $s$ is _guarded_ if $x$ is guarded
in $s(x)$ for all $x\in X$.

Step 1 can now be completed as follows: Given an ordered process
$(X,\leq,\vartheta)$ and a state $x\in X$, we define $s_{\vartheta}(x)$ by
choosing a representative
$p(\vec{\mathsf{v}},\langle\mathsf{a}_{i},x_{i}\rangle_{i\leq n})$ of
$\vartheta(x)$ and setting
$s_{\vartheta}(x)=p(\vec{\mathsf{v}},\mathsf{a}_{1}x_{1},\dots,\mathsf{a}_{n}x_{n})$.
Any two choices in representatives produce equivalent syntactic systems up to
$\equiv$, so we simply refer to any $s_{\vartheta}$ constructed in this manner
as _the_ syntactic system associated with $(X,\leq,\vartheta)$. Notice also
that $s_{\vartheta}$ is necessarily guarded.

Step 2 is contained in the following theorem, which implies that the
behaviours of finite ordered processes can be compared (in ${\mathsf{Prc}}$)
by solving their systems and comparing terms.

######  Theorem F.2.

Let $(X,\leq,\vartheta)$ be an ordered process with associated system of
equations $s_{\vartheta}$. Then $\phi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$
is a solution to $s_{\vartheta}$ if and only if
$\phi:{(X,\leq,\vartheta)}\to({\mathsf{Prc}},\sqsubseteq,\bar{\epsilon})$.

The proof of this is made much easier by the following lemma.

######  Lemma F.3 (Fundamental).

The coalgebraic structure map $\bar{\epsilon}:({\mathsf{Prc}},\sqsubseteq)\to
B_{M}({\mathsf{Prc}},\sqsubseteq)$ has a monotone inverse.

###### Proof.

By ($\mathsf{\mathsf{IN}}$),
$({\mathsf{Prc}},\sqsubseteq,\bar{\operatorname{\mathsf{ev}}}|_{S})\models\mathsf{IN}$.
Thus, the monotone map
$(-)^{\heartsuit}:(\mathsf{Var}+\mathsf{Act}\times{\mathsf{Prc}},\leq)\to({\mathsf{Prc}},\sqsubseteq)$
defined by

$\mathsf{v}^{\heartsuit}=\mathsf{v}\qquad\qquad\mathsf{\langle}\mathsf{a},[e]_{\equiv}\rangle^{\heartsuit}=[\mathsf{a}e]_{\equiv}$

lifts to a unique $S$-algebra homomorphism
$(-)^{\heartsuit}:(B_{M}({\mathsf{Prc}},\sqsubset),\rho)\to({\mathsf{Prc}},\sqsubseteq,\bar{\operatorname{\mathsf{ev}}}|_{S})$.
This map is readily seen to be a right inverse to $\bar{\epsilon}$, as
$\bar{\epsilon}(\mathsf{v}^{\heartsuit})=\bar{\epsilon}(\mathsf{v})=\mathsf{v}$
and
$\bar{\epsilon}(\langle\mathsf{a},[e]_{\equiv}\rangle^{\heartsuit})=\bar{\epsilon}([\mathsf{a}e]_{\equiv})=\langle\mathsf{a},[e]_{\equiv}\rangle$
and both $\bar{\epsilon}$ and $(-)^{\heartsuit}$ are $S$-algebra
homomorphisms. It remains to see that $(-)^{\heartsuit}$ is a left inverse to
$\bar{\epsilon}$. We prove that
$\bar{\epsilon}([e]_{\equiv})^{\heartsuit}=[e]_{\equiv}$ by induction on $e$.

  * •

$\bar{\epsilon}([\mathsf{v}]_{\equiv})^{\heartsuit}=\mathsf{v}^{\heartsuit}=\mathsf{v}$

  * •

$\bar{\epsilon}([\mathsf{a}e]_{\equiv})^{\heartsuit}=\langle\mathsf{a},[e]_{\equiv}\rangle^{\heartsuit}=\mathsf{a}[e]_{\equiv}=[\mathsf{a}e]_{\equiv}$

This concludes the base cases. For the inductive step,

  * •

$\bar{\epsilon}([\sigma(e_{1},\dots,e_{n})]_{\equiv})^{\heartsuit}=\sigma(\bar{\epsilon}([e_{1}]_{\equiv})^{\heartsuit},\dots,\bar{\epsilon}([e_{n}]_{\equiv})^{\heartsuit})=\sigma([e_{1}]_{\equiv},\dots,[e_{n}]_{\equiv})=[\sigma(e_{1},\dots,e_{n})]_{\equiv}$

  * •

For the unguarded recursion case, let
$\bar{\epsilon}(e)=q(\mathsf{v},\vec{\mathsf{u}},\langle\mathsf{a}_{i},f_{i}\rangle_{i\leq
n})$. By induction,

$[e]_{\equiv}=\bar{\epsilon}([e]_{\equiv})^{\heartsuit}=(q(\mathsf{v},\vec{\mathsf{u}},\langle\mathsf{a}_{i},[f_{i}]_{\equiv}\rangle_{i\leq
n}))^{\heartsuit}=q(\mathsf{v},\vec{\mathsf{u}},(\mathsf{a}_{i}[f_{i}]_{\equiv})_{i\leq
n})$

Thus, we have

$\displaystyle\bar{\epsilon}([\beta\mathsf{v}~{}e]_{\equiv})^{\heartsuit}$
$\displaystyle=(\operatorname{lfp}_{\mathsf{v}}q(\vec{\mathsf{u}},\langle\mathsf{a}_{i},[f_{i}]_{\equiv}\rangle_{i\leq
n}))^{\heartsuit}$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}q(\vec{\mathsf{u}},\langle\mathsf{a}_{i},[f_{i}]_{\equiv}\rangle_{i\leq
n}^{\heartsuit})$
$\displaystyle=\operatorname{lfp}_{\mathsf{v}}q(\vec{\mathsf{u}},([\mathsf{a}_{i}f_{i}]_{\equiv})_{i\leq
n})$
$\displaystyle=\beta{\mathsf{v}}~{}q(\mathsf{v},\vec{\mathsf{u}},([\mathsf{a}_{i}f_{i}]_{\equiv})_{i\leq
n})$ $\displaystyle=[\beta\mathsf{v}~{}e]_{\equiv}$

as desired.

  * •

For the full recursion case, we need to first show that $(-)^{\heartsuit}$
commutes with $[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$ for any
$g\in\mathsf{Exp}$. This is achieved by recalling that
$[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$ is an $S$-algebra homomorphism
$B_{M}({\mathsf{Prc}},\subseteq)\to B_{M}({\mathsf{Prc}},\sqsubseteq)$ and
noting that

$([\mathsf{v}]_{\equiv}[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}])^{\heartsuit}=([\mathsf{v}]_{\equiv})^{\heartsuit}=[\mathsf{v}]_{\equiv}=[\mathsf{v}]_{\equiv}^{\heartsuit}[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$

and

$\displaystyle(\langle\mathsf{a},[e]_{\equiv}\rangle[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}])^{\heartsuit}$
$\displaystyle=(\langle\mathsf{a},[e[g\mathbin{/}\mathsf{v}]]_{\equiv}\rangle)^{\heartsuit}$
$\displaystyle=[\mathsf{a}e[g\mathbin{/}\mathsf{v}]]_{\equiv}$
$\displaystyle=[\mathsf{a}e]_{\equiv}[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=\langle\mathsf{a},[e]_{\equiv}\rangle^{\heartsuit}[[g]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$

Finally, we use the previous case to conclude that

$\displaystyle\bar{\epsilon}([\mu\mathsf{v}~{}e]_{\equiv})^{\heartsuit}$
$\displaystyle=(\bar{\epsilon}([\beta\mathsf{v}~{}e]_{\equiv})[[\mu\mathsf{v}~{}e]_{\equiv}\mathbin{/\\!/}\mathsf{v}])^{\heartsuit}$
$\displaystyle=(\bar{\epsilon}([\beta\mathsf{v}~{}e]_{\equiv}))^{\heartsuit}[[\mu\mathsf{v}~{}e]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=[\beta\mathsf{v}~{}e]_{\equiv}[[\mu\mathsf{v}~{}e]_{\equiv}\mathbin{/\\!/}\mathsf{v}]$
$\displaystyle=[\beta\mathsf{v}~{}e[\mu\mathsf{v}~{}e\mathbin{/\\!/}\mathsf{v}]]_{\equiv}$
$\displaystyle=[\mu\mathsf{v}~{}e]_{\equiv}\qed$

###### Proof of Theorem F.2.

It suffices to show that $\phi$ is a solution iff $(-)^{\heartsuit}\circ
B_{M}(\phi)\circ\vartheta=\phi$, since $\bar{\epsilon}$ is a monotone left
inverse to $(-)^{\heartsuit}$. This is straight-forward: for any $x\in X$,
observe that

$\displaystyle(-)^{\heartsuit}\circ B_{M}(\phi)\circ\vartheta(x)$
$\displaystyle=(B_{M}(\phi)\circ\vartheta(x))^{\heartsuit}$
$\displaystyle=(\vartheta(x)[\phi(z)\mathbin{/\\!/}z]_{z\in X})^{\heartsuit}$
$\displaystyle=(\vartheta(x))^{\heartsuit}[\phi(z)\mathbin{/\\!/}z]_{z\in X}$
$\displaystyle=s_{\vartheta}(x)[\phi(z)\mathbin{/\\!/}z]_{z\in X}$

The last expression is equal to $\phi(x)$ if $\phi$ is a solution, and the
first expression is equal to $\phi(x)$ if $\phi$ is a homomorphism. ∎

Step 3 takes the form of the following theorem, a variation on a result of
Milner [2, Theorem 5.7] that establishes the unique solvability of systems of
equations associated with finite LTSs. Extra care is needed in our result to
ensure the monotonicty of our solutions.

######  Theorem F.4.

Every finite guarded system of equations admits a unique solution.

The proof of this theorem requires the following lemma (particularly the last
statement), which establishes the crutial features of the inference system
given in Fig. 3.

######  Lemma F.5.

The following are derivable from the axioms in Fig. 3.

$\mathsf{(R3^{\prime})}$

If $e[g\mathbin{/}\mathsf{v}]\sqsubseteq g$, then
$\mu\mathsf{v}~{}e\sqsubseteq g$.

$\mathsf{(R\alpha a)}$

If $\mathsf{w}\notin\operatorname{fv}(f_{i})$ for any $i\leq n$, then
$\beta\mathsf{w}~{}p(\mathsf{w},\vec{f})\sqsubseteq\beta\mathsf{v}~{}p(\mathsf{v},\vec{f})$.

$\mathsf{(R\alpha b)}$

If $\mathsf{w}\notin\operatorname{fv}(e)$, then
$\mu\mathsf{w}~{}e[\mathsf{w}/\mathsf{v}]\sqsubseteq\mu\mathsf{v}~{}e$.

$\mathsf{(Rfp1)}$

$\beta\mathsf{v}~{}e\equiv e[\beta\mathsf{v}~{}e\raisebox{-3.00003pt}{
\leavevmode\hbox to5.11pt{\vbox to11.66pt{\pgfpicture\makeatletter\hbox{\hskip
0.4pt\lower-6.09045pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-5.69046pt}\pgfsys@lineto{4.30554pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\mathsf{v}]$ where
$[\beta\mathsf{v}~{}e\raisebox{-3.00003pt}{ \leavevmode\hbox to5.11pt{\vbox
to11.66pt{\pgfpicture\makeatletter\hbox{\hskip 0.4pt\lower-6.09045pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-5.69046pt}\pgfsys@lineto{4.30554pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\mathsf{v}]$
replaces unguarded instances of $\mathsf{v}$ with $\beta\mathsf{v}~{}e$

$\mathsf{(Rfp2)}$

$\mu\mathsf{v}~{}e\equiv e[\mu\mathsf{v}~{}e\mathbin{/}\mathsf{v}]$

$\mathsf{(Rex)}$

$\mu\mathsf{v}~{}\beta\mathsf{v}~{}e\equiv\mu\mathsf{v}~{}e$

$\mathsf{(UFP)}$

If $\mathsf{v}\in\mathsf{gd}(e)$ and $e[g\mathbin{/}\mathsf{v}]\equiv g$, then
$\mu\mathsf{v}~{}e\equiv g$.

###### Proof.

We show (UFP) because it is made use of in the next theorem.

Since $\mathsf{v}\in\mathsf{gd}(e)$, $e\equiv\beta\mathsf{v}~{}e$, so
$e[g\mathbin{/\\!/}\mathsf{v}]=e[g\mathbin{/}\mathsf{v}]\equiv(\beta\mathsf{v}~{}e)[g\mathbin{/}\mathsf{v}]$.
From (R3) we see that $g\sqsubseteq\mu\mathsf{v}~{}e$. The converse inequality
can be seen from (R2b). ∎

We use the fact ($\mathsf{UFP}$) above frequently in the proof of Theorem F.4.

###### Proof of Theorem F.4.

Let $X=\\{x_{1},\dots,x_{n}\\}$ and set
$e_{i}=s(x_{i})\in\mathsf{Exp}(X,\leq)$ for each $i\leq n$. We proceed by
induction on $n$, the base case being easy: if $n=1$, then $\phi(x_{1})=\mu
x_{1}~{}e_{1}$ is the unique solution by ($\mathsf{UFP}$).

Now suppose that any guarded system with fewer than $n$ indeterminates has a
unique solution. Since $X$ is finite, there is a minimal element of
$(X,\leq)$. We take this to be the last of the indexed indeterminates,
$x_{n}$, and solve the system $s$ by first solving for $x_{n}$.

To this end, let $f_{n}=\mu x_{n}~{}e_{n}$, and
$f_{i}=e_{i}[f_{j}\mathbin{/}x_{j}]_{j\leq n}$ for $i<n$. Then by monotonicity
of substitution, $s^{\prime}:((X,\leq)-x_{n})\to\mathsf{Exp}((X,\leq)-x_{n})$
defined $s^{\prime}(x_{i})=f_{i}$ for $i<n$ defines a monotone syntactic
system. And furthermore, $x_{i}$ is guarded in $s^{\prime}(x_{i})$ for each
$i<n$. By the induction hypothesis, there exists a unique solution
$\phi^{\prime}:((X,\leq)-x_{n})\to({\mathsf{Prc}},\sqsubseteq)$. Let
$g_{i}=\phi^{\prime}(x_{i})$ for $i<n$ and define
$g_{n}=f_{n}[g_{i}\mathbin{/}x_{i}]_{i<n}$. By assumption, $\phi^{\prime}$ is
monotone. If $x_{n}\leq x_{i}$, we know that $e_{n}\sqsubseteq e_{i}$, and so
by monotonicity of substitution

$\displaystyle g_{n}$
$\displaystyle=f_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle=\mu
x_{n}~{}e_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle\equiv
e_{n}[f_{n}\mathbin{/}x_{n}][g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle\equiv
e_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1},g_{n}\mathbin{/}x_{n}]$
$\displaystyle\sqsubseteq
e_{i}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1},g_{n}\mathbin{/}x_{n}]$
$\displaystyle\equiv g_{i}$

This establishes monotonicity of
$\phi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$, where $\phi(x_{i})=g_{i}$ for
$i\leq n$. We have $\phi(x_{i})\equiv e_{i}[g_{j}\mathbin{/}x_{j}]_{j\leq n}$
for each $i\leq n$, and therefore
$\phi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$ is a solution to $s$.

Now let $\psi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$ be another solution to
$s$, and write $h_{i}=\psi(x_{i})$ for $i\leq n$. Then in particular,

$h_{n}\equiv
e_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1},h_{n}\mathbin{/}x_{n}]$

so by ($\mathsf{UFP}$),

$h_{n}\equiv\mu
x_{n}~{}e_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1}]=f_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1}]$

It follows that
$\psi^{\prime}:((X,\leq)-x_{n})\to({\mathsf{Prc}},\sqsubseteq)$ defined
$\psi^{\prime}(x_{i})=h_{i}[f_{n}\mathbin{/}x_{n}]$ is a solution to
$s^{\prime}$. By the induction hypothesis, $\phi^{\prime}\equiv\psi^{\prime}$,
or in other words $g_{i}\equiv h_{i}$ for each $i<n$. By
$\Sigma_{S}$-precongruence,

$\displaystyle h_{n}$ $\displaystyle\equiv\mu
x_{n}~{}e_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle\equiv\mu
x_{n}~{}e_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle=g_{n}$

Thus, $\phi\equiv\psi$, and consequently $\phi$ is the unique solution. ∎

Finally, step 4 is a result of the following observation: Call an ordered
process $(X,\leq,\vartheta)$ _locally finite_ if for every $x\in X$ there is a
finite subcoalgebra $U\subseteq X$ of $(X\leq,\vartheta)$ with $x\in U$.

######  Lemma F.6.

Both $(\mathsf{Exp},\leq_{\exp},\operatorname{\mathsf{ev}})$ and
$(J,\leq_{!},\zeta_{J})$ are locally finite.

To prove Lemma F.6, we need the following.

######  Lemma F.7.

Let $p(x,\vec{y})\in M(X,\leq)$ and $q=\operatorname{lfp}_{x}p$. Then
$q=q(\vec{y})$.

###### Proof.

Let $z\notin\vec{y}$. It suffices to show that if $q=q(\vec{y},z)$ for some
$z\in X\setminus\\{x\\}$, then for any $r\in M(X,\leq)$,
$q(\vec{y},r)\equiv_{\mathsf{IN}}q$. Since
$p(q,\vec{y})\sqsubseteq_{\mathsf{IN}}q$, we know that
$p(q(\vec{y},r),\vec{y})\sqsubseteq_{\mathsf{IN}}q(\vec{y},r)$, so that
$q(\vec{y},r)\in\operatorname{Pfp}_{x}(p)$. By assumption,
$q\sqsubseteq_{\mathsf{IN}}q(\vec{y},r)$. But $r$ is arbitrary, so in
particular $q(\vec{y},z)\sqsubseteq_{\mathsf{IN}}q(\vec{y},0)$. Replacing $z$
with an arbitrary $r$ again reveals
$q(\vec{y},r)\sqsubseteq_{\mathsf{IN}}q(\vec{y},0)$, so in fact,
$q(\vec{y},r)\equiv_{\mathsf{IN}}q(\vec{y},0)$, and furthermore
$q(\vec{y},r_{1})\equiv_{\mathsf{IN}}q(\vec{y},r_{2})$ for any $r_{1},r_{2}\in
M(X,\leq)$. It follows that $q(\vec{y},z)\equiv_{\mathsf{IN}}q(\vec{y},r)$ for
all $r\in M(X,\leq)$. ∎

###### Proof of Lemma F.6.

It suffices to see that $(\mathsf{Exp},\leq_{\exp},\epsilon)$ is locally
finite. Given an arbitrary $e\in\mathsf{Exp}$, we will explicitly construct a
subcoalgebra of $(\mathsf{Exp},\leq_{\exp},\epsilon)$ that has a finite set of
states that includes $e$. To this end, we define a function
$U:\mathsf{Exp}\to\mathcal{P}_{\omega}(\mathsf{Exp})$ inductively. For any
$e\in\mathsf{Exp}$, write $e[0\raisebox{-3.00003pt}{ \leavevmode\hbox
to5.11pt{\vbox to11.66pt{\pgfpicture\makeatletter\hbox{\hskip
0.4pt\lower-6.09045pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-5.69046pt}\pgfsys@lineto{4.30554pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\mathsf{v}]$ for the
expression obtained by replacing every unguarded instance of $\mathsf{v}$ in
$e$ with $0$. Then

$\displaystyle U(\mathsf{v})=\\{\mathsf{v}\\}\qquad
U(\mathsf{a}e)=\\{\mathsf{a}e\\}\cup U(e)\qquad
U(\sigma(e_{1},\dots,e_{n}))=\\{\sigma(e_{1},\dots,e_{n})\\}\cup\bigcup_{i\leq
n}U(e_{i})$ $\displaystyle
U(\beta\mathsf{v}~{}e)=\\{\beta\mathsf{v}~{}e\\}\cup
U(e[0\raisebox{-3.00003pt}{ \leavevmode\hbox to5.11pt{\vbox
to11.66pt{\pgfpicture\makeatletter\hbox{\hskip 0.4pt\lower-6.09045pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-5.69046pt}\pgfsys@lineto{4.30554pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\mathsf{v}])\qquad
U(\mu\mathsf{v}~{}e)=\\{\mu\mathsf{v}~{}e\\}\cup\\{f[\mu\mathsf{v}~{}e\mathbin{/\\!/}\mathsf{v}]\mid
f\in U(e[0\raisebox{-3.00003pt}{ \leavevmode\hbox to5.11pt{\vbox
to11.66pt{\pgfpicture\makeatletter\hbox{\hskip 0.4pt\lower-6.09045pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-5.69046pt}\pgfsys@lineto{4.30554pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\mathsf{v}])\\}$

Note that $e\in U(e)$ for all $e\in\mathsf{Exp}$, and that $U(e)$ is finite.
We begin with following claim, which says that the derivatives of $e$ can be
given in terms of expressions from $U(e)$: for any $e\in\mathsf{Exp}$, there
is a representative $S$-term $p\in\epsilon(e)$ such that $p\in
S^{*}(\mathsf{Var}+\mathsf{Act}\times U(e))$. This can be seen by induction on
$e$. For the base cases, we see that

  * •

$\epsilon(\mathsf{u})=\mathsf{u}\in S^{*}(\mathsf{Var}+\mathsf{Act}\times
U(\mathsf{u}))=S^{*}(\mathsf{Var}+\mathsf{Act}\times\\{\mathsf{u}\\})$ if
$\mathsf{u}\in\mathsf{Var}$

  * •

$\epsilon(\mathsf{a}e)=\langle\mathsf{a},e\rangle\in
S^{*}(\mathsf{Var}+\mathsf{Act}\times U(\mathsf{a}e))$ since $e\in
U(\mathsf{a}e)$.

For the inductive cases,

  * •

$\epsilon(\sigma(e_{1},\dots,e_{n}))=\sigma(\epsilon(e_{1}),\dots,\epsilon(e_{n}))$
and since $\epsilon(e_{i})$ has a representative $p_{i}\in
S^{*}(\mathsf{Var}+\mathsf{Act}\times U(e_{i}))$ for each $i\leq n$,
$\sigma(p_{1},\dots,p_{n})\in
S^{*}(\mathsf{Var}+\mathsf{Act}\times\bigcup_{i\leq n}U(e_{i}))$.

  * •

$\epsilon(\beta\mathsf{u}~{}e)=\operatorname{lfp}_{\mathsf{u}}\epsilon(e)$, so
we need to show that if
$p(\vec{\mathsf{v}},\langle\mathsf{a}_{i},e_{i}\rangle_{i\leq n})\in
S^{*}(\mathsf{Var}+\mathsf{Act}\times U(e))$ is a representative of
$\epsilon(e)$, then at most the variables $\vec{\mathsf{v}}$ and
$\langle\mathsf{a}_{i},e_{i}\rangle_{i\leq n}$ need appear in a representative
of $\operatorname{lfp}_{\mathsf{u}}\epsilon(e)$. This is the content of Lemma
F.7.

  * •

$\epsilon(\mu\mathsf{v}~{}e)=\operatorname{lfp}_{\mathsf{v}}\epsilon(e)[\mu\mathsf{v}\mathbin{/\\!/}\mathsf{v}]$,
in which case we let $p\in\epsilon(e)$ and note that
$\operatorname{lfp}_{\mathsf{v}}p[\mu\mathsf{v}~{}e/\\!/v]$ is a
representative of $\epsilon(\mu\mathsf{v}~{}e)$ in
$S^{*}(\mathsf{Var}+\mathsf{Act}\times U(\mu v~{}e))$.

To finish the proof of the lemma, fix an $e\in\mathsf{Exp}$ and define a
sequence of sets beginning with $U_{0}=\\{e\\}$ and proceeding with

$U_{n+1}=U_{n}\cup\bigcup_{e_{0}\in
U_{n}}\\{g\mid(\exists\mathsf{a}\in\mathsf{Act})(\exists
p\in\epsilon(e_{0})\cap S^{*}(\mathsf{Var}+\mathsf{Act}\times
U(e_{0})))~{}\text{$\langle\mathsf{a},g\rangle$ appears in $p$}\\}$

Then $U_{0}\subseteq U_{1}\subseteq\cdots\subseteq U(e)$, and the latter set
is finite. Hence $U:=\bigcup U_{n}$ is finite and contained in $U(e)$. We
define a coalgebra structure $\epsilon_{U}:U\to B_{M}U$ by taking
$\epsilon_{U}(e)=p$ where if $e\in U_{n}$, then $p$ is a representative of
$\epsilon(e)$ in $S^{*}(\mathsf{Var}+\mathsf{Act}\times U_{n+1})$. Since
$S^{*}(\mathsf{Var}+\mathsf{Act}\times U_{n+1})\subseteq
S^{*}(\mathsf{Var}+\mathsf{Act}\times U)$ and $\epsilon_{U}$ agrees with
$\epsilon$ (up to $\equiv_{\mathsf{IN}}$), this defines a monotone
$B_{M}$-coalgebra structure on $U$. Where
$\iota:U\hookrightarrow\mathsf{Exp}$, we have
$\epsilon(\iota(e))=\epsilon(e)=B_{M}(\iota)\circ\epsilon_{U}(e)$. Thus,
$(U,\epsilon_{U})$ is a finite subcoalgebra of
$(\mathsf{Exp},\leq_{exp},\epsilon)$ containing $e$. ∎

###### Proof of Corollary 6.5.

The formal construction of $\phi:J\to{\mathsf{Prc}}$ can now be carried out by
choosing a finite subcoalgebra $U_{t}\subseteq J$ containing $t$ for each
$t\in J$ and setting $\phi(t)=\phi_{U_{t}}(t)$ where $\phi_{U_{t}}$ is the
unique solution to the system of equations associated with
$(U_{t},\leq_{!},\zeta_{U_{t}})$. Every homomorphism out of a locally finite
coalgebra is the union of its restrictions to finite subcoalgebras, so it
suffices to check that $\phi$ is well-defined and restricts to a coalgebra
homomorphism on each finite subcoalgebra.

To that end, notice that if $t\in U_{t_{1}}\cap U_{t_{2}}$ we can write
$\zeta(t)=p(\vec{\mathsf{v}},\langle\mathsf{a}_{i},s_{i}\rangle_{i\leq n})$
with $s_{i}\in U_{t_{1}}\cap U_{t_{2}}$, and similarly for each $s_{i}$ and so
on, so that there is a finite subcoalgebra $U\subseteq U_{t_{1}}\cap
U_{t_{2}}$ containing $t$. By uniqueness of solutions,
$\phi_{U_{t_{1}}}(t)\equiv\phi_{U}(t)\equiv\phi_{U_{t_{2}}}(t)$, so $\phi$ is
a well-defined coalgebra homomorphism. To see that $\phi$ is left-inverse to
$\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$, observe that
$\phi(\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor)=\phi_{\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor}(\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor)\equiv e$
follows from Theorem F.4 since the inclusion map $\phi[U_{\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor}]\hookrightarrow{\mathsf{Prc}}$ is the unique solution to
the finite subcoalgebra $\phi[U_{\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor}]$
of $({\mathsf{Prc}},\sqsubseteq,\bar{\epsilon})$. ∎

#### An aside: Least solutions without guardedness

There is another version of Theorem F.4 that does not require guardedness of
systems. The following proposition records this, but it should be noted that
we do not require this proposition anywhere else in the appendix.

######  Proposition F.8.

Every finite system of equations admits a least solution.

###### Proof.

The idea behind this proof is the same as the proof of Theorem F.4, but with a
different induction hypothesis/step. Let $X=\\{x_{1},\dots,x_{n}\\}$ and set
$e_{i}=s(x_{i})\in\mathsf{Exp}(X,\leq)$ for each $i\leq n$. We will show,
inductively on $n$, that (i) $s$ has a solution $\phi$, and (ii) for every
_pre_ solution $\psi:{(X,\leq)}\to{({\mathsf{Prc}},\sqsubseteq)}$ of $s$,
meaning that $\psi^{\\#}\circ s\sqsubseteq\psi$, we have
$\psi(x_{i})\sqsubseteq\psi(x_{i})$ for each $i\leq n$.

Again, the base case is easy: if $n=1$, then $\phi(x_{1})=\mu x_{1}~{}e_{1}$
is a solution. Furthermore, if
$e_{1}[\psi(x_{1})\mathbin{/}x_{1}]\sqsubseteq\psi(x_{1})$, then
$\phi(x_{1})\sqsubseteq\psi(x_{1})$ by the least fixed-point axiom of Fig. 3.

Now suppose that any guarded system with fewer than $n$ indeterminates has a
solution below every presolution. Since $X$ is finite, there is a minimal
element of $(X,\leq)$. Again, we take this to be the last of the indexed
indeterminates, $x_{n}$, and solve the system $s$ by first solving for
$x_{n}$.

To this end, let $f_{n}=\mu x_{n}~{}e_{n}$, and
$f_{i}=e_{i}[f_{j}\mathbin{/}x_{j}]_{j\leq n}$ for $i<n$. Then by monotonicity
of substitution, $s^{\prime}:((X,\leq)-x_{n})\to\mathsf{Exp}((X,\leq)-x_{n})$
defined $s^{\prime}(x_{i})=f_{i}$ for $i<n$ defines a monotone syntactic
system. By the induction hypothesis, there exists a solution
$\phi^{\prime}:((X,\leq)-x_{n})\to({\mathsf{Prc}},\sqsubseteq)$ that is below
every presolution. Let $g_{i}=\phi^{\prime}(x_{i})$ for $i<n$ and define
$g_{n}=f_{n}[g_{i}\mathbin{/}x_{i}]_{i<n}$. By assumption, $\phi^{\prime}$ is
monotone. If $x_{n}\leq x_{i}$, we know that $e_{n}\sqsubseteq e_{i}$, and so
by monotonicity of substitution

$\displaystyle g_{n}$
$\displaystyle=f_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle=\mu
x_{n}~{}e_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle\equiv
e_{n}[f_{n}\mathbin{/}x_{n}][g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle\equiv
e_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1},g_{n}\mathbin{/}x_{n}]$
$\displaystyle\sqsubseteq
e_{i}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1},g_{n}\mathbin{/}x_{n}]$
$\displaystyle\equiv g_{i}$

This establishes monotonicity of
$\phi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$, where $\phi(x_{i})=g_{i}$ for
$i\leq n$. We have $\phi(x_{i})\equiv e_{i}[g_{j}\mathbin{/}x_{j}]_{j\leq n}$
for each $i\leq n$, and therefore
$\phi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$ is a solution to $s$.

Now let $\psi:(X,\leq)\to({\mathsf{Prc}},\sqsubseteq)$ be any presolution to
$s$, and write $h_{i}=\psi(x_{i})$ for $i\leq n$. Then in particular,

$h_{n}\sqsupseteq
e_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1},h_{n}\mathbin{/}x_{n}]$

By the least fixed-point axioms of Fig. 3,

$h_{n}\sqsupseteq\mu
x_{n}~{}e_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1}]=f_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1}]$

It follows that
$\psi^{\prime}:((X,\leq)-x_{n})\to({\mathsf{Prc}},\sqsubseteq)$ defined
$\psi^{\prime}(x_{i})=h_{i}[f_{n}\mathbin{/}x_{n}]$ is a presolution to
$s^{\prime}$. By the induction hypothesis,
$\phi^{\prime}\sqsubseteq\psi^{\prime}$, or in other words $g_{i}\sqsubseteq
h_{i}$ for each $i<n$. By $\Sigma_{S}$-precongruence,

$\displaystyle h_{n}$ $\displaystyle\sqsupseteq\mu
x_{n}~{}e_{n}[h_{1}\mathbin{/}x_{1},\dots,h_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle\sqsupseteq\mu
x_{n}~{}e_{n}[g_{1}\mathbin{/}x_{1},\dots,g_{n-1}\mathbin{/}x_{n-1}]$
$\displaystyle=g_{n}$

Thus, $\phi\sqsubseteq\psi$, and consequently $\phi$ is a solution below every
presolution. ∎

##  Appendix G The small-step semantics of polystar expressions

Polystar expressions also carry an intuitive small-step semantics, given by an
$L_{M}$-coalgebra structure $(\mathsf{PExp},\leq_{\text{pxp}},\ell)$ where
$L_{M}=M(\\{\checkmark\\}+\mathsf{Act}\times\operatorname{Id})$. This is
outlined below.

ℓ(0) = 0 ℓ(1) = 1 ℓ(e +_σf) = σ(ℓ(e), ℓ(f)) ℓ(e f) = q(ℓ(f), ⟨a_1, e_1 f⟩, …,
⟨a_n, e_nf⟩) ℓ(a) = ⟨a, 1⟩ℓ(e^[p]) = lfp_x (p(q(x, ⟨a_1, e_1e^[p]⟩, …, ⟨a_n,
e_ne^[p]⟩), ✓)) Here, $\sigma\in I$; $e,e_{1},e_{2}\in\mathsf{PExp}$;
$\mathsf{a},\mathsf{a}_{i}\in\mathsf{Act}$; $p=p(x,y)\in S^{*}\\{x,y\\}$;
$\ell(e)=q(\checkmark,\langle\mathsf{a}_{1},e_{1}\rangle,\dots,\langle\mathsf{a}_{n},e_{n}\rangle)$.

##  Appendix H Proofs from Section 8

See 8.1

###### Proof.

Let $h:(X,\vartheta)\to(Y,\delta)$ be a $B_{N}$-coalgebra homomorphism such
that $h(x)=h(y)$. Then $h=D(h):(X,=,\vartheta)\to(Y,=,\delta)$, so $x=_{!}y$.
∎

See 8.2

###### Proof.

Suppose $M$ lifts $N$ and let $(X,\vartheta)$ be a $B_{N}$-coalgebra with
states $x,y\in X$. If $x\mathrel{\underline{\leftrightarrow}}y$, then
$x=_{!}y$ by Lemma 8.1. If $x=_{!}y$, let
$h:(X,=,\vartheta)\to(Y,\leq,\delta)$ be such that $h(x)=h(y)$. Then $h$ is an
$N$-coalgebra homomorphism, because $U(\delta):X\to UB_{M}(X,=)=B_{N}X$ and

$\delta\circ h=U(\delta\circ h)=U(B_{M}(h)\circ\vartheta)=UB_{M}(h)\circ
U(\vartheta)=B_{N}D(h)\circ\vartheta=B_{N}(h)\circ\vartheta$

It follows that $x\mathrel{\underline{\leftrightarrow}}y$.

Conversely, suppose that $x=_{!}y$ but not
$x\mathrel{\underline{\leftrightarrow}}y$. There is an
$h:(X,=,\vartheta)\to(Y,\leq,\delta)$ such that $h(x)=h(y)$, but it must be
the case that $U(h)=h$ fails to be a $B_{N}$-coalgebra homomorphism. However,
$UB_{M}(h)\circ\vartheta=U(B_{M}(h)\circ\vartheta)=U(\delta\circ
h)=U(\delta)\circ h$, so it must be the case that $UB_{M}(h)\neq
B_{N}(h)=B_{N}U(h)$. It follows that $M$ fails to lift $N$. ∎

Say that $(S,\mathsf{IN})$ _admits couplings_ if for any
$h:(X,\leq)\to(Y,\leq)$ and any $p(\vec{x}),q(\vec{y})\in M(X,\leq)$ such that
$p(h(\vec{x}))\equiv_{\mathsf{IN}}q(h(\vec{y}))$, there is an $h$-coupling $r$
of $p$ and $q$. The next lemma is in reference to Remark 8.6.

######  Lemma H.1.

$M$ weakly preserves pullbacks if and only if $(S,\mathsf{IN})$ admits
couplings.

###### Proof.

Obtain $k_{1}:(P,\leq)\to(X,\leq)$ and $k_{2}:(P,\leq)\to(Y,\leq)$ as the
pullback of $f_{1}:(X,\leq)\to(W,\leq)$ and $f_{2}:(Y,\leq)\to(W,\leq)$. Also
obtain $l_{1}:(Q,\leq)\to M(X,\leq)$ and $l_{2}:(Q,\leq)\to M(Y,\leq)$ as the
pullback of $M(f_{1}),M(f_{2})$. The statement that $M$ weakly preserves
pullbacks is equivalent to the statement that $M(P,\leq)$ always surjects onto
$(Q,\leq)$.

Now, $Q\cong\\{(p,q)\in M(X,\leq)\times M(X,\leq)\mid
M(f_{1})(p)=M(f_{2})(q)\\}$ and $P\cong\\{(x,y)\in X\mid
f_{1}(x)=f_{2}(y)\\}$. In other words, if $p=p(\vec{x})$ and $q=q(\vec{y})$,
$p(f_{1}(\vec{x}))\equiv_{\mathsf{IN}}q(f_{2}(\vec{y}))$. It follows that the
function $M(P,\leq)\to(Q,\leq)$ defined $r((u_{i},v_{i})_{i\leq
n})\mapsto(r(\vec{u}),r(\vec{v}))$ is monotone.

By [65, Theorem 8.6], $M$ preserves weak pullbacks if and only if there is a
$r((u_{i},v_{i})_{i\leq n})\in M(P,\leq)$ such that
$r(\vec{u})\equiv_{\mathsf{IN}}p$ and $r(\vec{v})\equiv_{\mathsf{IN}}q$ for
every $(p,q)\in Q$. That is, if and only if $(S,\mathsf{IN})$ admits
couplings. ∎

See 8.5

###### Proof.

We aim to show that for any pair $(x,y)\in X^{2}$ satisfying $x\leq_{!}y$,
there is an

$r(\vec{\mathsf{v}},\langle\mathsf{a}_{i},(x_{i},y_{i})\rangle_{i\leq n})\in
B_{M}(\leq_{!})$

such that
$\theta(x)\sqsubseteq_{\mathsf{IN}}r(\vec{\mathsf{v}},\langle\mathsf{a}_{i},x_{i}\rangle_{i\leq
n})$ and $r(\vec{\mathsf{v}},\langle\mathsf{a}_{i},x_{i}\rangle_{i\leq
n})\sqsubseteq_{\mathsf{IN}}\theta(y)$. To this end, let
$h:(X,=,\vartheta)\to(Y,\leq,\delta)$ such that $h(x)\leq h(y)$. Then

$B_{M}(h)\circ\vartheta(x)\equiv_{\mathsf{IN}}\delta\circ
h(x)\sqsubseteq_{\mathsf{IN}}\delta\circ
h(y)\equiv_{\mathsf{IN}}B_{M}(h)\circ\vartheta(y)$

by monotonicity. By assumption, there is a weak
$(\mathsf{Var}+\mathsf{Act}\times h)$-coupling
$r(\vec{\mathsf{v}},\langle\mathsf{a}_{i},(u_{i},v_{i})\rangle_{i\leq n})$ of
$\vartheta(x)$ with $\vartheta(y)$. That is, we have $h(u_{i})\leq h(v_{i})$
for each $i\leq n$, and
$\vartheta(x)\sqsubseteq_{\mathsf{IN}}r(\vec{\mathsf{v}},\langle\mathsf{a}_{i},u_{i}\rangle_{i\leq
n})$, and $r(\vec{\mathsf{v}},\langle\mathsf{a}_{i},v_{i}\rangle_{i\leq
n})\sqsubseteq_{\mathsf{IN}}\vartheta(y)$. Since $h(u_{i})\leq h(v_{i})$,
$u_{i}\leq_{!}v_{i}$ for each $i\leq n$ and $r\in B_{M}(\leq_{!})$ as desired.
∎

See 8.8

###### Proof.

Let $x$ and $y$ be states of $(X,\vartheta)$. It suffices to show that the
determinacy condition ensures that $x\sim y$ implies $x=_{!}y$. To this end,
let $R_{1},R_{2}\subseteq X^{2}$ be simulations witnessing $x\precsim y$ and
$y\precsim x$ respectively. Let $\leq$ be the reflexive-transitive closure of
$R_{1}\cup R_{2}$ and $Y=X/{\leq}$. Then the quotient map $h:(X,=)\to(Y,\leq)$
satisfies $h(x)\leq h(y)$ and $h(y)\leq h(x)$. Since $(S,\mathsf{IN})$ admits
weak $h$-couplings in both directions, by detemrinacy there is an $h$-coupling
$r(\vec{v},\langle\mathsf{a},(u_{i},v_{i})\rangle_{i\leq n})$ of $\theta(x)$
and $\theta(y)$.

Now let $R=\\{(u,v)\in X^{2}\mid h(u)=h(v)\\}$ and define $\rho:(R,=)\to
B_{M}(R,=)$ by choosing an $h$-coupling
$r_{u,v}(\vec{v},\langle\mathsf{a}_{i},(u_{i},v_{i})\rangle_{i\leq n})$ of
$\vartheta(u)$ with $\vartheta(v)$ and setting

$\rho(u,v)\equiv_{\mathsf{IN}}r_{u,v}(\vec{v},\langle\mathsf{a}_{i},(u_{i},v_{i})\rangle_{i\leq
n})$

Now,

$\displaystyle B_{M}(\pi_{1})\circ\rho(u,v)$
$\displaystyle\equiv_{\mathsf{IN}}B_{M}(\pi_{1})(r_{u,v}(\vec{v},\langle\mathsf{a}_{i},(u_{i},v_{i})\rangle_{i\leq
n}))$ $\displaystyle=r_{u,v}(\vec{v},\langle\mathsf{a}_{i},u_{i}\rangle_{i\leq
n})$ $\displaystyle\equiv_{\mathsf{IN}}\vartheta(u)$
$\displaystyle=\vartheta\circ\pi_{1}(u,v)$

for any $(u,v)\in R$, and similarly
$B_{M}(\pi_{2})\circ\rho(u,v)\equiv_{\mathsf{IN}}\vartheta(v)$. This tells us
that $(R,\rho)$ is a _bisimulation_ on $(X,\vartheta)$ containing $(x,y)$.
This implies that $x\mathrel{\underline{\leftrightarrow}}y$ [19], so by Lemma
8.1 we have $x=_{!}y$ as desired. ∎

##  Appendix I Ordered Convex Algebra

In this section, we give a proof of the monad presentation claimed in Example
3.4.

######  Lemma I.1.

The heavier-higher order is a partial order.

###### Proof.

The heavier-higher order is clearly reflexive and transitive. To see that it
is antisymmetric, let $\theta_{1}\leq^{hh}\theta_{2}\leq^{hh}\theta_{1}$. Then
in particular, where

$\operatorname{\uparrow}x:=\\{u\in X\mid x\leq u\\}$

we see that
$\theta_{1}(\operatorname{\uparrow}x)=\theta_{2}(\operatorname{\uparrow}x)$
for all $x\in X$. Since $\operatorname{supp}(\theta_{1})$ is finite, it has
maximal elements. Let $x_{0}$ be such an element of $X$, and observe that
$\theta_{1}(\operatorname{\uparrow}x_{0})=\theta_{1}(x_{0})$. We proceed by
induction on the number of elements of $\operatorname{supp}(\theta_{1})$.

Suppose $\operatorname{supp}(\theta_{1})=\\{x_{0}\\}$. Since
$\theta_{2}(\operatorname{\uparrow}x_{0})=\theta_{1}(\operatorname{\uparrow}x_{0})$,
$\theta_{2}(\operatorname{\uparrow}x_{0})>0$ and so
$\operatorname{supp}(\theta_{2})\cap\operatorname{\uparrow}x_{0}$ is nonempty.
Let $x_{1}$ be a maximal element of
$\operatorname{supp}(\theta_{2})\cap\operatorname{\uparrow}x_{0}$. Then
$x_{0}\leq x_{1}$ and
$\theta_{2}(\operatorname{\uparrow}x_{1})=\theta_{2}(x_{1})$. Hence,

$\theta_{2}(x_{1})=\theta_{2}(\operatorname{\uparrow}x_{1})=\theta_{1}(\operatorname{\uparrow}x_{1})=\theta_{1}(\operatorname{\uparrow}x_{0})=\theta_{1}(x_{0})$

Since this implies that $x_{1}\in\operatorname{supp}(\theta_{1})$,
$x_{0}=x_{1}$. It follows that $\theta_{1}(x_{0})=\theta_{2}(x_{0})$.

Now define $\theta_{i}^{\prime}(x)=\theta_{i}(x)$ when $x\neq x_{0}$ and
$\theta_{i}(x)=0$ otherwise, $i=1,2$. Since
$\theta_{i}={\theta_{i}(x_{0})\delta_{x_{0}}}+\theta_{i}^{\prime}$ for
$i=1,2$, by cancellativity of $\mathbf{P}$ we know that

$\theta_{1}(x_{0})\delta_{x_{0}}+\theta_{1}^{\prime}\leq^{hh}\theta_{2}(x_{0})\delta_{x_{0}}+\theta_{2}^{\prime}\leq^{hh}\theta_{1}(x_{0})\delta_{x_{0}}+\theta_{1}^{\prime}$

implies
$\theta_{1}^{\prime}\leq^{hh}\theta_{2}^{\prime}\leq^{hh}\theta_{1}^{\prime}$,
because $\theta_{1}(x_{0})=\theta_{2}(x_{0})$. It follows by induction that
$\theta_{1}^{\prime}=\theta_{2}^{\prime}$. Therefore $\theta_{1}=\theta_{2}$
as well. ∎

######  Lemma I.2.

For any monotone map $f:(X,\leq)\to(Y,\leq)$, the map
$f^{\bullet}:\mathcal{D}_{\omega}X\to\mathcal{D}_{\omega}Y$ is monotone wrt to
the heavier-higher order.

###### Proof.

Let $U\subseteq Y$ be an upper set of $(Y,\leq)$. Then $f^{-1}(U)$ is an upper
set of $(X,\leq)$. We have

$\displaystyle f^{\bullet}\theta_{1}(U)$ $\displaystyle=\sum_{u\in
U}f^{\bullet}\theta_{1}(u)=\sum_{u\in
U}\sum_{f(x)=u}\theta_{1}(x)=\sum_{f(x)\in U}\theta_{1}(x)\leq\sum_{f(x)\in
U}\theta_{2}(x)=f^{\bullet}\theta_{2}(U)$

∎

That $(\mathcal{D}_{\omega},\delta,\oplus)$ is the free convex algebra follows
directly from the following three facts.

Fact (1)

The transformation $\delta$ is monotone with respect to the heavier-higher
order on any given base partial order. That is, for any $(X,\leq)$,
$\delta:(X,{\leq})\to(\mathcal{D}_{\omega}X,{\leq^{hh}})$.

Fact (2)

$(\mathcal{D}_{\omega}X,\leq^{hh},\oplus)$ is an ordered convex algebra. It
suffices to see that given
$\theta_{1},\theta_{2},\varphi\in\mathcal{D}_{\omega}X$ and $r,s\in[0,1]$,

  * (i)

if $\theta_{1}\leq^{hh}\theta_{2}$, then
$\theta_{1}+\varphi\leq^{hh}\theta_{2}+\varphi$, and

  * (ii)

if $r\leq s$, then $p\cdot\varphi\leq^{hh}q\cdot\varphi$.

Fact (3)

For any ordered convex algebra $(Y,\leq,\beta)$ and any
$f:(X,\leq)\to(Y,\leq)$, the inductively specified convex algebra homomorphism
$f^{\beta}:(\mathcal{D}_{\omega},\rho)\to(Y,\beta)$ is monotone with respect
to the heavier-higher order, ie.
$f^{\beta}:(\mathcal{D}_{\omega}X,\leq^{hh},\rho)\to(Y,\leq,\beta)$.

We are going to argue for Fact (3), as it has a nontrivial proof.

###### Proof (of Fact (3))..

Let $\theta_{1}\leq^{hh}\theta_{2}$ in $\mathcal{D}_{\omega}(X,\leq)$, and
$f:(X,\leq)\to(Y,\leq)$ where $(Y,\leq,\beta)$ is a convex algebra. We proceed
by induction on $|\operatorname{supp}(\theta_{1})|$. If
$\operatorname{supp}(\theta_{1})=\emptyset$, then
$\theta_{1}=0\leq^{hh}\theta_{2}$.

For the induction step, let $z$ be any maximal element of
$\operatorname{supp}(\theta_{1})$ and define

$\theta_{i}^{\prime}(x)=\begin{cases}\theta_{i}(z)-\theta_{1}(z)&x=z\\\
\theta_{i}(x)&\text{o.w.}\end{cases}$

For any upper set $U$ containing $z$,
$\theta_{i}(U)=\theta_{1}(z)+\theta_{i}^{\prime}(U)$, so by assumption
$\theta_{1}(z)+\theta_{1}^{\prime}(U)\leq\theta_{1}(z)+\theta_{2}^{\prime}(U)$.
Since $(\mathbb{R},+)$ is cancellative,
$\theta_{1}^{\prime}(U)\leq\theta_{2}^{\prime}(U)$. For any upper set $U$ not
containing $z$, $\theta_{i}(U)=\theta_{i}^{\prime}(U)$, so by again,
$\theta_{1}^{\prime}(U)\leq\theta_{2}^{\prime}(U)$. It follows that
$\theta_{1}^{\prime}\leq^{hh}\theta_{2}^{\prime}$, so by induction
$f^{\beta}(\theta_{1}^{\prime})\leq f^{\beta}(\theta_{2}^{\prime})$. We
therefore have

$f^{\beta}(\theta_{1})=f^{\beta}(\theta_{1}(z)\cdot\delta_{z})+f^{\beta}(\theta_{1}^{\prime})\leq
f^{\beta}(\theta_{1}(z)\cdot\delta_{z})+f^{\beta}(\theta_{2}^{\prime})\leq
f^{\beta}(\theta_{1}(z)\cdot\delta_{z})+f^{\beta}(\theta_{2}^{\prime})=f^{\beta}(\theta_{2})$

This shows that $f^{\beta}$ is monotone. ∎