# Reduction of symplectic groupoids and quotients of quasi-Poisson manifolds

Daniel Álvarez  Instituto de Matemática Pura e Aplicada, Estrada Dona
Castorina, 110, Jardim Botânico, CEP 22460320, Rio de Janeiro, Brasil
<EMAIL_ADDRESS>
###### Abstract.

In this work we study the integrability of quotients of quasi-Poisson
manifolds. Our approach allows us to put several classical results about the
integrability of Poisson quotients in a common framework. By categorifying one
of the already known methods of reducing symplectic groupoids we also describe
double symplectic groupoids which integrate the recently introduced Poisson
groupoid structures on gauge groupoids.

###### Contents

  1. 1 Introduction
  2. 2 Preliminaries
    1. 2.1 Lie groupoids and Lie algebroids
    2. 2.2 Poisson structures, closed IM 2-forms and symplectic groupoids
  3. 3 Integrability of quotients of quasi-Poisson manifolds
    1. 3.0.1 Poisson structures and quasi-Poisson manifolds
    2. 3.0.2 The integrability criterion
    3. 3.0.3 Integrability of quotients of Poisson actions
    4. 3.0.4 Integrability of quotients of q-Poisson $G$-manifolds
  4. 4 Double symplectic groupoids and gauge Poisson groupoids
    1. 4.0.1 Double symplectic groupoids
    2. 4.1 Integrability of gauge Poisson groupoids in the complete case

##  1\. Introduction

One of the main tools in the study of Poisson manifolds is the concept of
symplectic groupoid, see [12, 23, 14, 15, 18] for some of its most exciting
applications. So a basic problem in Poisson geometry is the construction of
interesting examples of symplectic groupoids. Unlike finite-dimensional Lie
algebras, which always admit integrations to Lie groups, not every Poisson
manifold is “integrable” to a symplectic groupoid [45]. Although general
criteria for the integrability of Poisson manifolds (and Lie algebroids in
general) were established in [16, 17], in most cases, these conditions do not
easily lead to an explicit construction.

In this paper we address the problem of describing symplectic groupoids which
integrate Poisson manifolds obtained as quotients of Lie groupoid actions on
q-Poisson manifolds. The study of the integrability of quotient Poisson
structures began with [36], where it was established that the quotient of a
symplectic manifold $S$ by a Lie group action is integrable by performing
Marsden-Weinstein reduction on the fundamental groupoid of $S$. Subsequently,
it was proven in [21] that the quotient of an integrable Poisson manifold $S$
by a Lie group action by automorphisms is also integrable by a Marsden-
Weinstein quotient of the source-simply-connected integration of $S$. The work
in [22, 42] generalized this result for Poisson actions of Poisson groupoids
on integrable Poisson manifolds. In this work, we generalize these results
even further by considering Poisson quotients of quasi-Poisson (q-Poisson)
manifolds

The study of q-Poisson manifolds began with the finite-dimensional description
of Poisson structures on representation varieties provided in [3]. Later on,
it was realized that most of the known methods of Poisson reduction by
symmetries could be described in terms of an even broader notion of q-Poisson
manifold [39]. Roughly, a q-Poisson manifold (in the general sense of [39]) is
a manifold endowed with a suitable (global or infinitesimal) action and a
bilinear bracket on the space of smooth functions that fails to be Poisson in
a way controlled by the action; an important feature is that the orbit space
of such an action turns out to carry a genuine Poisson structure, provided it
is smooth. Let $(S,\pi)$ be a q-Poisson manifold for a Lie quasi-bialgebroid
$(A,\delta,\chi)$ such that the moment map $J:S\rightarrow M$ is a surjective
submersion. There is a canonical Lie algebroid structure on the conormal
bundle $C$ of the $A$-orbits, provided it is smooth. If the $A$-action on $S$
integrates to a $G$-action, where $G\rightrightarrows M$ is a Lie groupoid
integrating $A$, and if the $G$-action on $S$ is free and proper, then the
quotient $S/G$ inherits a canonical Poisson structure $\sigma$.

######  Theorem 1.1.

The Poisson manifold $(S/G,\sigma)$ is integrable if and only if the Lie
algebroid $C$ is integrable. Moreover, if $\mathcal{G}(C)$ is the source-
simply-connected integration of $C$, then there is a lifted $G$-action on
$\mathcal{G}(C)$ such that the orbit space $\mathcal{G}(C)/G$ is a symplectic
groupoid integrating $(S/G,\sigma)$.

Theorem 1.1 is a consequence of the integrability of Lie groupoid actions on
Lie algebroids established in [38]. We obtain some corollaries about Poisson
reduction such as the following. Let $G$ be a Poisson group acting freely and
properly by a Poisson action on a Poisson manifold $(S,\pi)$. Then the induced
Poisson structure on $\overline{S}=S/G$ is integrable if $S$ is integrable
[21, 22]. For the original q-Poisson $\mathfrak{g}$-manifolds of [3] we get a
completely analogous result. If $(S,\pi)$ is a q-Poisson $G$-manifold, then
there is a nonobvious but canonical Lie algebroid structure on $T^{*}S$ [26].
Theorem 1.1 implies that the Poisson structure induced on $\overline{S}=S/G$
is integrable if $T^{*}S$ is integrable. In both of these situations, the Lie
algebroid $C$ that appears in Theorem 1.1 controlling the integrability of the
quotient can be interpreted as the Lie algebroid of the level set
corresponding to the unit of a Lie group valued moment map as in [27] in the
former case and in the sense of [2] in the latter. This last observation is
related to the integration of Poisson structures on moduli spaces of flat
$G$-bundles that shall be studied in a companion paper, see [4].

Poisson actions also allow us to obtain Poisson quotients by considering the
action restricted to a coisotropic subgroup [41, 27]. In this context, the
integrability of the quotient can be proved only under the assumption that the
acting Poisson group is complete [22]. In this context, we have the following
result which can be seen as a simple categorification of the quotient
construction of [22].

######  Theorem 1.2.

Let $G$ be a complete Poisson group acting freely and properly on a Poisson
manifold $M$. If $M$ is integrable, then the gauge Poisson groupoid
$(M\times\overline{M})/G\rightrightarrows M/G$ is integrable by a double
symplectic groupoid.

This last result, together with an observation coming from [5] about the
symplectic leaves of Poisson groupoids, can be applied to an interesting
family of examples of gauge Poisson groupoids recently introduced by J.-H. Lu
and her collaborators thereby producing a number of new examples of symplectic
groupoids.

### Acknowledgments.

The author thanks CNPq for the financial support and H. Bursztyn for his
continuous advice and support.

##  2\. Preliminaries

###  2.1. Lie groupoids and Lie algebroids

A smooth groupoid $G$ over a manifold $M$, denoted $G\rightrightarrows M$, is
a groupoid object in the category of not necessarily Hausdorff smooth
manifolds such that its source map is a submersion. The structure maps of a
groupoid are its source, target, multiplication, unit map and inversion,
denoted respectively $\mathtt{s},\mathtt{t},\mathtt{m},\mathtt{u},\mathtt{i}$.
For the sake of brevity, we also denote $\mathtt{m}(a,b)$ by $ab$. A Lie
groupoid is a smooth groupoid such that its base and source-fibers are
Hausdorff manifolds, see [37, 20]. A Lie groupoid is _source-simply-connected_
if its source fibres are 1-connected.

_A left Lie groupoid action_ of a Lie groupoid $G\rightrightarrows M$ on a map
$J:S\rightarrow M$ is a smooth map $a:G_{\mathtt{s}}\times_{J}S\rightarrow S$
such that (1) $a(\mathtt{m}(g,h),x)=a(g,a(h,x))$ for all $g,h\in G$ and for
all $x\in S$ for which $a$ and $\mathtt{m}$ are defined and (2)
$a(\mathtt{u}(J(x)),x)=x$ for all $x\in M$, the fiber product
$G_{\mathtt{t}}\times_{J}G$ is denoted by $G\times_{M}S$. There is a Lie
groupoid structure on $G\times_{M}S$ over $S$ with the projection
$\text{pr}_{2}:G\times_{M}S\rightarrow S$ being the source map, $a$ being the
target map and the multiplication given by $(g,a(h,p))(h,p)=(gh,p)$. The Lie
groupoid $G\times_{M}S\rightrightarrows S$ thus obtained is called an action
groupoid. A Lie groupoid action as before is free if the associated action
groupoid has trivial isotropy groups; a Lie groupoid action is proper if the
map $(a,\text{pr}_{2}):G\times_{M}S\rightarrow S\times S$ is proper. If a Lie
groupoid is a Lie group, this recovers the usual notion of free and proper
actions.

A vector bundle $A$ over a manifold $M$ is a Lie algebroid if there exist: (1)
a bundle map $\mathtt{a}:A\rightarrow TM$ called the anchor and (2) a Lie
algebra structure $[\,,\,]$ on $\Gamma(A)$ such that the Leibniz rule holds

$[u,fv]=f[u,v]+\left(\mathcal{L}_{\mathtt{a}(u)}f\right)v,$

for all $u,v\in\Gamma(A)$ and $f\in C^{\infty}(M)$. See [24, 43] for the
definition of Lie algebroid morphism.

The Lie algebroid $A=A_{G}$ of a Lie groupoid $G\rightrightarrows B$ is the
vector bundle $A=\ker T\mathtt{s}|_{B}$ endowed with the restriction of
$T\mathtt{t}$ to $A$ as the anchor and with the bracket defined by means of
right invariant vector fields [37, 33]. A Lie groupoid morphism induces a Lie
algebroid morphism between the associated Lie algebroids, this construction
defines a functor called the Lie functor that we denote by Lie. A Lie
algebroid which is isomorphic to the tangent Lie algebroid of a Lie groupoid
is called integrable. If $A$ is an integrable Lie algebroid, we denote by
$\mathcal{G}(A)$ its source-simply-connected integration (which is unique up
to isomorphism).

A fundamental result relating Lie groupoids and Lie algebroids is Lie’s second
theorem. Let $\phi:A\rightarrow B$ be a Lie algebroid morphism between
integrable Lie algebroids. Then, for every Lie groupoid $K$ integrating $B$,
there exists a unique Lie groupoid morphism $\Phi:\mathcal{G}(A)\rightarrow K$
such that $\text{Lie}(\Phi)=\phi$ [38, 37].

###  2.2. Poisson structures, closed IM 2-forms and symplectic groupoids

A Poisson structure on a manifold $M$ is a bivector field
$\pi\in\Gamma(\wedge^{2}TM)$ such that $[\pi,\pi]=0$, where $[\,,\,]$ is the
Schouten bracket; with this kind of structure, $(M,\pi)$ is called a _Poisson
manifold_. There is a canonical Lie algebroid structure on the cotangent
bundle of a Poisson manifold in which the Lie bracket on $\Omega^{1}(M)$ is
given by

$\displaystyle[\alpha,\beta]=\mathcal{L}_{\pi^{\sharp}(\alpha)}\beta-\mathcal{L}_{\pi^{\sharp}(\beta)}\alpha-d\pi(\alpha,\beta),$

for all $\alpha,\beta\in\Omega^{1}(M)$, and the anchor is the map
$\pi^{\sharp}$ defined by $\alpha\mapsto i_{\alpha}\pi$; $T^{*}M$ is usually
called the cotangent Lie algebroid of $M$. A Poisson morphism
$J:(P,\pi_{P})\rightarrow(Q,\pi_{Q})$ between Poisson manifolds is a smooth
map that satisfies $\pi_{P}\sim_{J}\pi_{Q}$.

Let $A$ be a Lie algebroid over $M$. A closed IM 2-form on $A$ [10] is a
vector bundle morphism $\mu:A\rightarrow T^{*}M$ over the identity such that

(1)
$\displaystyle\langle\mu(v),\mathtt{a}(u)\rangle=-\langle\mu(u),\mathtt{a}(v)\rangle$
(2)
$\displaystyle\mu([u,v])=\mathcal{L}_{\mathtt{a}(u)}\mu(v)-i_{\mathtt{a}(v)}d\mu(u)$

for all $u,v\in\Gamma(A)$. In the case of a Poisson manifold $(M,\pi)$, the
identity on $T^{*}M$ is a closed IM 2-form. Closed IM 2-forms are the basic
infrastructure necessary for performing Poisson reduction as we shall see
below, see [11] for a general discussion. At the Lie groupoid level, a closed
IM 2-form induces a closed multiplicative 2-form: let $G\rightrightarrows M$
be a Lie groupoid and take $\omega\in\Omega^{2}(G)$, $\omega$ is called
multiplicative if
$\text{pr}_{1}^{*}\omega+\text{pr}_{2}^{*}\omega-\text{pr}_{3}^{*}\omega$
vanishes on the graph of the multiplication inside $G\times G\times{G}$. A Lie
groupoid $G\rightrightarrows B$ is a _symplectic groupoid_ [45, 25] if it is
endowed with a symplectic form which is multiplicative. If the cotangent Lie
algebroid of a Poisson manifold $M$ is integrable, we shall say that $M$ is
integrable. If $M$ is an integrable Poisson manifold, we denote by
$\Sigma(M)\rightrightarrows M$ its source-simply-connected integration which
naturally becomes a symplectic groupoid by integrating its canonical closed IM
2-form [10].

##  3\. Integrability of quotients of quasi-Poisson manifolds

The integrability of Poisson manifolds obtained by reduction has been studied
in [36, 21, 42, 22]. In this section we put some of the results contained in
those works in the broader context of q-Poisson manifolds.

####  3.0.1. Poisson structures and quasi-Poisson manifolds

######  Definition 3.1 ([40]).

A Lie quasi-bialgebroid is a Lie algebroid $A$ over $M$ endowed with a degree
one derivation $\delta:\Gamma(\wedge^{k}A)\rightarrow\Gamma(\wedge^{k+1}A)$
for all $k\in\mathbb{N}$ which is a derivation of the bracket on $A$,

$\delta([u,v])=[\delta(u),v]+(-1)^{p-1}[u,\delta(v)]$

for all $u\in\Gamma(\wedge^{p}A)$, $v\in\Gamma(\wedge^{\bullet}A)$ and
satisfies $\delta^{2}=[\chi,\,]$, where $\chi\in\Gamma(\wedge^{3}A)$ is such
that $\delta(\chi)=0$.

Since $\delta$ is a derivation, it is determined by its restriction to degree
0 and degree 1 where it is given respectively by a vector bundle map
$\mathtt{a}_{*}:A^{*}\rightarrow TM$ and a map
$\Gamma(A)\rightarrow\Gamma(\wedge^{2}A)$ called the cobracket.

######  Example 3.2.

A Lie bialgebroid $(A,A^{*})$ is a Lie quasi-bialgebroid $(A,\delta,\chi)$ in
which $\chi=0$ and hence the differential $\delta$ satisfies $\delta^{2}=0$
[35]. Since the dual of a differential which squares to zero is a Lie bracket,
a Lie bialgebroid consists of a pair of Lie algebroid structures on $A$ and
$A^{*}$ which are compatible in a suitable sense. A Lie bialgebra
$(\mathfrak{g},\mathfrak{g}^{*})$ is a Lie bialgebroid over a point [19].

######  Definition 3.3 ([39]).

A quasi-Poisson manifold (or a Hamiltonian space) for a Lie quasi-bialgebroid
$(A,\delta,\chi)$ on $M$ is given by an action $\rho:J^{*}A\rightarrow TS$ of
$A$ on a smooth map $J:S\rightarrow M$ and a bivector field $\pi$ on $S$ such
that:

$\displaystyle\frac{1}{2}[\pi,\pi]=\rho(\chi)$
$\displaystyle\mathcal{L}_{\rho(U)}\pi=\rho(\delta(U)),\quad\forall
U\in\Gamma(A),$ $\displaystyle\pi^{\sharp}J^{*}=\rho\circ\mathtt{a}^{*}_{*},$

where $\mathtt{a}_{*}:A^{*}\rightarrow TS$ is the component of $\delta$ in
degree zero as before.

######  Example 3.4.

An infinitesimal Poisson action $\rho:\mathfrak{g}\rightarrow TS$ of the
tangent Lie bialgebra $(\mathfrak{g},\mathfrak{g}^{*})$ of a Poisson group
[19, 27] can be expressed by saying that $(S,\pi,\rho)$ is a Hamiltonian space
for $(\mathfrak{g},\delta,0)$, where $\delta$ is the differential dual to the
bracket on $\mathfrak{g}^{*}$.

######  Example 3.5.

The original q-Poisson manifolds, which were introduced in [3], are a special
case of Definition 3.3. Consider a Lie algebra $\mathfrak{g}$ endowed with an
Ad-invariant symmetric nondegenerate bilinear form $B$. Then there is a Lie
quasi-bialgebra structure $(\mathfrak{g},\delta,\chi)$ on $\mathfrak{g}$ which
depends on $B$ and is determined by the splitting of
$\mathfrak{g}\oplus\mathfrak{g}$ as the sum of the diagonal Lie subalgebra and
the anti-diagonal [1, 3]. The q-Poisson manifolds corresponding to
$(\mathfrak{g},\delta,\chi)$ shall be called q-Poisson
$\mathfrak{g}$-manifolds in accordance to [3, 26].

The main feature of this notion is the following well known reduction
construction. Let $(S,\pi)$ be a quasi-Poisson manifold for a Lie quasi-
bialgebroid $(A,\delta,\chi)$. If the $A$-action induces a simple foliation on
$S$, then its leaf space $\overline{S}$ inherits a unique Poisson structure
$\overline{\pi}$ such that $\pi$ and $\overline{\pi}$ are $q$-related, where
$q:S\rightarrow\overline{S}$ is the projection. In fact, the cotangent Lie
algebroid of $\overline{S}$ can be described as the quotient of a Lie
algebroid over $S$.

######  Proposition 3.6.

If the $A$-action induces a regular foliation on $S$, then the conormal bundle
$C$ of the $A$-orbits is a Lie algebroid with the anchor defined by
$\alpha\mapsto\pi^{\sharp}(\alpha)$ and the Lie bracket

(3) $\displaystyle[\alpha,\beta]_{C}:=\mathcal{L}_{\pi^{\sharp}(\alpha)}\beta-
i_{\pi^{\sharp}(\beta)}d\alpha,$

for all $\alpha,\beta\in\Gamma(C)$.

###### Proof.

Take $U\in\Gamma(B)$, $\alpha\in\Gamma(C)$ and let $\beta\in\Omega^{1}(S)$ be
arbitrary. Then we have that

$\langle\beta,\mathcal{L}_{\rho(U)}(\pi^{\sharp}(\alpha))\rangle=\mathcal{L}_{\rho(U)}\langle\beta,\pi^{\sharp}(\alpha)\rangle-\langle\mathcal{L}_{\rho(U)}\beta,\pi^{\sharp}(\alpha)\rangle=\langle\rho(\delta(U)),\alpha\wedge\beta\rangle+\langle\beta,\pi^{\sharp}(\mathcal{L}_{\rho(U)}\alpha)\rangle,$

where we used the identity $\mathcal{L}_{\rho(U)}\pi=\rho(\delta(U))$ and the
fact that

$\mathcal{L}_{\rho(U)}(\pi(\alpha,\beta))=(\mathcal{L}_{\rho(U)}\pi)(\alpha,\beta)+\pi(\mathcal{L}_{\rho(U)}\alpha,\beta)+\pi(\alpha,\mathcal{L}_{\rho(U)}\beta).$

But $\langle\rho(\delta(U)),\alpha\wedge\beta\rangle=0$ since $\alpha$ lies in
the annihilator of $\rho(\Gamma(A))$. As a consequence,

(4)
$\displaystyle\mathcal{L}_{\rho(U)}\pi^{\sharp}(\alpha)=\pi^{\sharp}(\mathcal{L}_{\rho(U)}\alpha).$

Now we shall check that $[\alpha,\beta]_{C}\in\Gamma(C)$. Take
$U\in\Gamma(A)$, we have that

$\langle\mathcal{L}_{\pi^{\sharp}(\alpha)}\beta,\rho(U)\rangle=\langle
d(i_{\pi^{\sharp}(\alpha)}\beta)+i_{\pi^{\sharp}(\alpha)}d\beta,\rho(U)\rangle=\langle\beta,[\rho(U),\pi^{\sharp}(\alpha)]\rangle=-\langle\mathcal{L}_{\rho(U)}\alpha,\pi^{\sharp}(\beta)\rangle,$

where we used (4) in the last equality. On the other hand,

$\displaystyle\langle
i_{\pi^{\sharp}(\beta)}d\alpha,\rho(U)\rangle=d\alpha(\pi^{\sharp}(\beta),\rho(U))=-\mathcal{L}_{\rho(U)}\langle\alpha,\pi^{\sharp}(\beta)\rangle+\langle\alpha,\mathcal{L}_{\rho(U)}\pi^{\sharp}(\beta)\rangle.$

By combining the last two equations we get that

$\langle[\alpha,\beta]_{C},\rho(U)\rangle=\langle\alpha,\mathcal{L}_{\rho(U)}(\pi^{\sharp})(\beta)\rangle=(\mathcal{L}_{\rho(U)}\pi)(\alpha,\beta)$

and this last term is zero because $\mathcal{L}_{\rho(U)}\pi=\rho(\delta(U))$
is generated by vectors tangent to the $A$-orbits. Finally,

$\pi^{\sharp}([\alpha,\beta]_{C})=[\pi^{\sharp}(\alpha),\pi^{\sharp}(\beta)]-\frac{1}{2}i_{\alpha\wedge\beta}[\pi,\pi]=[\pi^{\sharp}(\alpha),\pi^{\sharp}(\beta)]-i_{\alpha\wedge\beta}\rho(\chi)=[\pi^{\sharp}(\alpha),\pi^{\sharp}(\beta)].$

So it follows that $[\,,\,]_{C}$ satisfies the Jacobi identity and hence it
endows $C$ with a Lie algebroid structure. ∎

######  Remark 3.7.

As we shall see next, the integrability of the quotient Poisson structure is
controlled by the integrability of this Lie algebroid structure on $C$. It is
immediate that the inclusion $C\hookrightarrow T^{*}S$ is a closed IM 2-form
on $C$, so we see that quasi-Poisson reduction fits within the general
framework of Poisson reduction described in [11].

A q-Poisson manifold $(S,\pi)$ for a Lie quasi-bialgebroid $(A,\delta,\chi)$
comes naturally equipped with a canonical action of $A$ on $C$ as in
Proposition 3.6 in the following sense. Let $J:S\rightarrow M$ be a surjective
submersion, let $A$ be a Lie algebroid over $M$ and let $C$ be a Lie algebroid
over $S$ such that $Tq\circ\mathtt{a}=0$, where $\mathtt{a}$ is the anchor of
$C$.

######  Definition 3.8 ([24, 38]).

An action of $A$ on a Lie algebroid $C$ over $S$ is an $A$-action on $J$ and a
Lie algebra morphism $\Gamma(A)\rightarrow\text{Der}(C)$ which is
$C^{\infty}(M)$-linear, where $\text{Der}(C)$ is the space of derivations of
$C$.

######  Lemma 3.9.

Let $(S,\pi)$ be a Hamiltonian space for a Lie quasi-bialgebroid
$(A,\delta,\chi)$ on $M$ with moment map $J:S\rightarrow M$. If $J$ is a
surjective submersion, then the map given by $U\mapsto\mathcal{L}_{\rho(U)}$
for all $U\in\Gamma(A)$ defines an infinitesimal action of $A$ on $C$.

###### Proof.

First of all, equation (4) implies that
$\mathcal{L}_{\rho(U)}[\alpha,\beta]_{C}=[\mathcal{L}_{\rho(U)}\alpha,\beta]_{C}+[\alpha,\mathcal{L}_{\rho(U)},\beta]_{C}$.
On the other hand, the equation
$\pi^{\sharp}J^{*}=\rho\circ\mathtt{a}^{*}_{*}$ implies that
$TJ\circ\pi^{\sharp}:C\rightarrow TM$ is the zero map. Since
$\mathcal{L}_{f\rho(U)}\alpha=f\mathcal{L}_{\rho(U)}\alpha$ by Cartan’s
formula, the map $\psi$ is $C^{\infty}(M)$-linear and so we are done. ∎

We are only interested in the situation in which the previous infinitesimal
action of $A$ on $C$ is integrable by a global action of the following kind.
Let $G\rightrightarrows M$ be a Lie groupoid acting on a surjective submersion
$J:S\rightarrow M$ and let $C$ be a Lie algebroid over $S$ such that
$TJ\circ\mathtt{a}=0$. In this situation we have an action of $C$ on the
projection $G\times_{M}S\rightarrow S$ given by $X\mapsto(0,\mathtt{a}(X))$
for all $X\in\Gamma(C)$. Hence, there is an action Lie algebroid structure on
$G\times_{M}C$ over $G\times_{M}S$. Let $p:C\rightarrow S$ be the vector
bundle projection.

######  Definition 3.10 ([38]).

An action of $G\rightrightarrows M$ on $C$ is a Lie groupoid action of $G$ on
$J\circ p:C\rightarrow S$ such that the structure maps of the action groupoid
$G\times_{M}C\rightrightarrows C$ are Lie algebroid morphisms over the
structure maps of the action groupoid $G\times_{M}S\rightrightarrows S$.

####  3.0.2. The integrability criterion

Let $(S,\pi)$ be a q-Poisson manifold for a Lie quasi-bialgebroid
$(A,\delta,\chi)$ such that the moment map $J:S\rightarrow M$ is a surjective
submersion and the $A$-action on $S$ induces a regular foliation. Suppose that
the $A$-action on $C$ integrates to a $G$-action as in Definition 3.10 and
that the $G$-action is free and proper so that the quotient $S/G$ is a smooth
manifold and it inherits a Poisson structure $\sigma$ with the property that
$Tq\circ\pi^{\sharp}\circ q^{*}=\sigma^{\sharp}$, where $q:S\rightarrow S/G$
is the quotient map.

######  Theorem 3.11.

The Poisson manifold $(S/G,\sigma)$ is integrable if and only if the Lie
algebroid $C$ is integrable. Moreover, if $\mathcal{G}(C)$ is the source-
simply-connected integration of $C$, then there is a lifted $G$-action on
$\mathcal{G}(C)$ such that the orbit space $\mathcal{G}(C)/G$ is a symplectic
groupoid integrating $(S/G,\sigma)$.

######  Remark 3.12.

The previous result generalizes [42, Thm 3.4.4], which regards only Poisson
groupoid actions.

The $G$-action on $\mathcal{G}(C)$ as in the previous theorem is compatible
with the groupoid structure in the following sense.

Let $K\rightrightarrows S$ and $G\rightrightarrows M$ be Lie groupoids and let
$J:S\rightarrow M$ be a surjective submersion such that
$J\circ\mathtt{s}=J\circ\mathtt{t}$.

######  Definition 3.13 ([24]).

An action of $G\rightrightarrows M$ on $K\rightrightarrows S$ is an action on
the map $J\circ\mathtt{s}=J\circ\mathtt{t}:K\rightarrow M$ which is a Lie
groupoid action $G\times_{M}K\rightarrow K$ such that it is a Lie groupoid
morphism with respect to the fiber product groupoid
$G\times_{M}K\rightrightarrows G\times_{M}S$.

Notice that when $M$ is a point, a $G$-action in the previous sense is a
$G$-action by automorphisms on $K$.

###### Proof of Theorem 3.11.

Suppose that $C$ is integrable.

Step 1: lift of the $G$-action to $\mathcal{G}(C)$. First of all, [38, Thm.
3.6] implies that the $G$-action on $C$ lifts to a $G$-action on
$\mathcal{G}(C)$. On the other hand, this lifted action is principal since it
is principal on the base and hence the quotient $\mathcal{G}(C)/G$ inherits a
unique Lie groupoid structure such that the projection map
$\mathcal{G}(C)\rightarrow\mathcal{G}(C)/G$ is a Lie groupoid morphism [38,
Lemma 2.1].

Step 2: existence of a canonical multiplicative 2-form on $\mathcal{G}(C)$.
Recall that the inclusion $\mu:C\hookrightarrow T^{*}S$ constitutes a closed
IM 2-form on $C$. Let $\lambda$ be the canonical 1-form on $T^{*}S$ and let us
denote $\Lambda_{\mu}=d(\mu^{*}\lambda)\in\Omega^{2}(C)$. Then
$\Lambda_{\mu}^{\flat}:TC\rightarrow T^{*}C$ is a Lie algebroid morphism which
lifts to a Lie groupoid morphism $\omega^{\flat}:T\mathcal{G}(C)\rightarrow
T^{*}\mathcal{G}(C)$ with the property that $\omega$ is a multiplicative
closed 2-form on $\mathcal{G}(C)$ [8].

Step 3: reduction of $\omega$ to a symplectic form on $\mathcal{G}(C)/G$. The
lifted $G$-action on $\mathcal{G}(C)$ is obtained as the integration
$\widetilde{\alpha}:G\times_{M}\mathcal{G}(C)\rightarrow\mathcal{G}(C)$ of the
Lie algebroid morphism $\alpha$, see the proof of [38, Thm. 3.6]. Since
$\widetilde{\alpha}$ is also an action,
$\Gamma:=G\times_{M}\mathcal{G}(C)\rightrightarrows\mathcal{G}(C)$ inherits an
action groupoid structure, where $\widetilde{\alpha}$ is its target map and
the projection
$\text{pr}_{2}:G\times_{M}\mathcal{G}(C)\rightarrow\mathcal{G}(C)$ is its
source. In order to prove that $\omega$ descends to a symplectic form on
$\mathcal{G}(C)/G$, we have to check that the $G$-orbits are tangent to
$\ker\omega$ and that
$\mathtt{t}_{\Gamma}^{*}\omega=\widetilde{\alpha}^{*}\omega=\mathtt{s}_{\Gamma}^{*}\omega=\text{pr}_{2}^{*}\omega$.

Step 4: the $G$-orbits are tangent to $\ker\omega$. Infinitesimally, the
$A$-action on $C$ lifts to $\mathcal{G}(C)$ as follows. Take $U\in\Gamma(A)$
of compact support. Since $\mathcal{L}_{\rho(U)}$ is a derivation of $C$ over
$\rho(U)$, it integrates to a 1-parameter family of automorphisms $\psi_{t}$
of $C$. Lie’s second theorem implies that $\psi_{t}$ lifts to a family of Lie
groupoid automorphisms $\Psi_{t}$ of $\mathcal{G}(C)$. The infinitesimal
generator of $\Psi_{t}$ is a multiplicative vector field
$\widetilde{U}\in\mathfrak{X}(\mathcal{G}(C))$, i.e. a vector field which is a
Lie groupoid morphism $\widetilde{U}:\mathcal{G}(C)\rightarrow
T\mathcal{G}(C)$. Since
$i_{\widetilde{U}}\omega:T\mathcal{G}(C)\rightarrow\mathbb{R}$ is a Lie
groupoid morphism, in order to prove that $i_{\widetilde{U}}\omega=0$ we just
have to check that its associated Lie algebroid morphism is zero. Let us
denote by $\mathcal{B}$ the distribution tangent to the $A$-orbits, by
construction, it is generated by the vector fields of the form
$\widetilde{U}$.

The Lie algebroid morphism
$\overline{\Lambda}_{\mu}:TC\oplus_{C}TC\rightarrow\mathbb{R}$ associated to
$\omega:T\mathcal{G}(C_{L})\oplus T\mathcal{G}(C)\rightarrow\mathbb{R}$ is
defined by the linear 2-form $\Lambda_{\mu}=\mu^{*}\omega_{\text{can}}$, where
$\omega_{\text{can}}$ is the canonical symplectic form on $T^{*}S$ [8]. On the
other hand, we have that $\widetilde{U}$ induces a Lie algebroid morphism
$U^{\prime}=C\rightarrow TC$ in the following way

$U^{\prime}(\alpha_{p})=T_{p}\alpha(U_{p})-\overline{\left(\mathcal{L}_{\rho(U)}\alpha\right)}_{p}\quad\forall
p\in S,$

where $\alpha\in\Gamma(C)$ and $\overline{\mathcal{L}_{\rho(U)}\alpha}_{p}$ is
the vertical tangent vector to $C$ at $\alpha_{p}$ associated to
$\left(\mathcal{L}_{\rho(U)}\alpha\right)_{p}$ [38]. So we have immediately
that $i_{U^{\prime}}\Lambda_{\mu}=0$ and hence $i_{\widetilde{U}}\omega=0$
which proves $\mathcal{B}\subset\ker\omega$.

On the other hand, we have that $\ker\omega_{\mathtt{t}(g)}\cap\ker
T_{\mathtt{t}(g)}\mathtt{s}=0$ since $\mu$ is injective and hence

(5) $\displaystyle\ker\omega_{g}\cap\ker
T_{g}\mathtt{s}\cong\ker\omega_{\mathtt{t}(g)}\cap\ker
T_{\mathtt{t}(g)}\mathtt{s}=0$

for all $g\in\mathcal{G}(C)$, [10, Lemma 3.1]. If $V\in\ker\omega_{g}$ and
$W\in T_{\mathtt{s}(g)}G$, then for (any) $X\in T_{g}\mathcal{G}(C)$
composable with $W$ we have that

$\omega_{\mathtt{s}(g)}(T\mathtt{s}(V),W)=\omega_{g}(V,T\mathtt{m}(W,X))-\omega_{g}(V,X)=0$

and so $T_{g}\mathtt{s}(v)\in\ker\omega_{\mathtt{s}(g)}$. But
$T_{g}\mathtt{s}$ restricted to $\ker\omega_{g}$ is injective by (5), so
$\dim\ker\omega_{g}\leq\dim\ker\omega_{\mathtt{s}(g)}=\dim B=\dim\mathcal{B}$.
Therefore, $\mathcal{B}=\ker\omega$.

Step 5: $\mathtt{t}_{\Gamma}^{*}\omega-\mathtt{s}_{\Gamma}^{*}\omega=0$. We
have to show that the linear 2-form corresponding to the multiplicative 2-form
$\mathtt{t}_{\Gamma}^{*}\omega-\mathtt{s}_{\Gamma}^{*}\omega$ on $\Gamma$
vanishes [8]. But this linear 2-form is nothing but
$d(\alpha^{*}\lambda-\text{pr}_{2}^{*}\lambda)\in\Omega^{2}(G\times_{M}C)$ and
we have that $\alpha^{*}\lambda-\text{pr}_{2}^{*}\lambda=0$. Therefore,
$\omega$ is $\Gamma$-basic and it descends to a multiplicative symplectic form
on the quotient $\mathcal{G}(C)/G$.

Finally, if $(S/G,\sigma)$ is integrable, then its pullback Dirac structure
$L$ along the projection map $S\rightarrow S/G$ is integrable [10]; $C$ can be
identified with a Lie subalgebroid of $L$ and hence it is also integrable
[37]. ∎

######  Remark 3.14.

A closer look at the $G$-action on $\mathcal{G}(C)$ reveals that it does not
identify points on the same $\mathtt{s}$-fiber, therefore, $\mathcal{G}(C)/G$
is also source-simply-connected and so the fact that it is symplectic also
follows from the integration of Lie bialgebroids in [34].

####  3.0.3. Integrability of quotients of Poisson actions

A Lie group is a Poisson group if it is endowed with a Poisson structure such
that the multiplication map is a Poisson morphism [19]. A Poisson action of a
Poisson group on a Poisson manifold is a Lie group action which is a Poisson
morphism [41].

######  Corollary 3.15.

Let $G$ be a Poisson group and suppose that there is a Poisson $G$-action on a
Poisson manifold $S$. Suppose $G$ acts freely and properly on $S$. If $S$ is
integrable, then the induced Poisson structure on the quotient $S/G$ is
integrable.

###### Proof.

In this situation, $C$ as in Theorem 3.11 is the conormal bundle of the
$G$-orbits on $S$ and it is a Lie subalgebroid of the cotangent Lie algebroid
of $S$. Therefore, $C$ is integrable if so is $S$ and hence the result follows
from Theorem 3.11. ∎

######  Remark 3.16.

Notice that, in principle, we can apply Theorem 3.11 even when $S$ is not
integrable by considering only the Lie subalgebroid $C\hookrightarrow T^{*}S$.
In the case that $G$ is complete, this result appears in [22].

Let us describe explicitly the integration of the quotient $S/G$ as in
Corollary 3.15 provided by Theorem 3.11. Let $\Sigma(S)\rightrightarrows S$ be
the source-simply-connected integration of $S$. There is a Poisson map
$\mu:\Sigma(S)\rightarrow G^{*}$ which is also a Lie groupoid morphism lifting
the Lie algebroid morphism given the dual of the action map
$T^{*}S\rightarrow\mathfrak{g}^{*}$. So there is an infinitesimal
$\mathfrak{g}$-action on $\Sigma(S)$ which is not complete in general unless
$G$ is complete [22]. Since the $\mathfrak{g}$-action is locally free, $\mu$
is a submersion and so $\mu^{-1}(1)\hookrightarrow\Sigma(S)$ is a Lie
subgroupoid integrating the Lie subalgebroid $C\hookrightarrow T^{*}S$. If we
consider $\mathcal{G}(C)$, Theorem 3.11 tells us that the
$\mathfrak{g}$-action on $\mathcal{G}(C)$ given by the composition of the
canonical morphism $\mathcal{G}(C)\rightarrow\mu^{-1}(1)$ with the inclusion
$\mu^{-1}(1)\hookrightarrow\Sigma(S)$ integrates to a $G$-action and that the
quotient $\mathcal{G}(C)/G$ is a symplectic groupoid integrating $S/G$ (in
fact, $\mathcal{G}(C)/G=\Sigma(S/G)$, see Remark 3.14).

####  3.0.4. Integrability of quotients of q-Poisson $G$-manifolds

If $(S,\pi)$ is a q-Poisson $\mathfrak{g}$-manifold, then there is a
nonobvious but canonical Lie algebroid structure on $T^{*}S$, see [26, Thm.
1]; we shall denote it by $(T^{*}S)_{\mathfrak{g}}$. It is immediate that $C$
as before is a Lie subalgebroid of $(T^{*}S)_{\mathfrak{g}}$ (provided the
$\mathfrak{g}$-action is locally free). For the sake of making the analogy
with the previous situation more evident, we shall also say in this case that
$S$ is integrable if $(T^{*}S)_{\mathfrak{g}}$ is. If the
$\mathfrak{g}$-action on $S$ is integrable to a $G$-action such that $\pi$ is
invariant, $(S,\pi)$ is called a q-Poisson $G$-manifold.

######  Corollary 3.17.

Let $(S,\pi)$ be a q-Poisson ${G}$-manifold. Then the Poisson structure
induced on $S/G$ is integrable if $S$ is integrable. ∎

Let us illustrate more precisely the integration provided of quotients of
q-Poisson $G$-manifolds provided by Theorem 3.11 and let us compare it with
the results of [26] about the integration of q-Poisson $G$-manifolds.

Let $(S,\pi)$ be a q-Poisson $G$-manifold [3]. Suppose that $G$ acts freely
and properly on $S$. We have that [26, Thm 1] states that the dual of the
action map $T^{*}S\rightarrow\mathfrak{g}^{*}$ composed with the isomorphism
$\mathfrak{g}\cong\mathfrak{g}^{*}$ induced by the bilinear form gives us a
Lie algebroid morphism $(T^{*}S)_{\mathfrak{g}}\rightarrow\mathfrak{g}$. If
$(T^{*}S)_{\mathfrak{g}}$ is integrable, then this morphism can be lifted to a
moment map $\Phi:\mathcal{G}(T^{*}S)_{\mathfrak{g}}\rightarrow G$ which makes
$\mathcal{G}(T^{*}S)_{\mathfrak{g}}$ into a q-Hamiltonian
$\mathfrak{g}$-manifold (groupoid), see [26, Thm 4]. If the
$\mathfrak{g}$-action is locally free on $S$ (and hence on
$\mathcal{G}(T^{*}S)_{\mathfrak{g}}$), we have that $\Phi^{-1}(1)$ is a Lie
groupoid. Indeed, [2, Remark 3.3] says that there is a 2-form
$\varpi\in\Omega^{2}(\mathfrak{g})$ such that, if we take a neighborhood $U$
of $1\in G$ covered diffeomorphically by a neighborhood of $0\in\mathfrak{g}$
using $\exp:\mathfrak{g}\rightarrow G$, then
$\Omega:=\omega-\Phi^{*}\log^{*}\varpi$ is symplectic on $\Phi^{-1}(U)$ and
$\mu:=\log\circ\Phi$ is a classical moment map for the $\mathfrak{g}$-action.
Since the $\mathfrak{g}$-action is locally free on $S$, it is also locally
free on $\mathcal{G}(T^{*}S)_{\mathfrak{g}}$. The usual property of moment
maps $(\ker T\mu)^{\Omega}=\mathfrak{g}_{\mathcal{M}}$ implies that $\mu$ is a
submersion on $\Phi^{-1}(U)$ and then so is $\Phi$. If we consider the source-
simply-connected integration $\widetilde{\Phi^{-1}(1)}$ of
$C=\text{Lie}(\Phi^{-1}(1))$, we have a $G$-action by automorphisms on
$\widetilde{\Phi^{-1}(1)}$. Theorem 3.11 implies that
$\widetilde{\Phi^{-1}(1)}/{G}$ is a symplectic groupoid which integrates the
Poisson structure on $S/G$.

######  Example 3.18.

The most important examples of q-Poisson $G$-manifolds are the spaces of
representations of fundamental groups of surfaces [2, 3]. For instance, the
q-Poisson $G$-manifold associated to an annulus is $G$ itself and the
integrability of the Lie algebroid structure on $(T^{*}G)_{\mathfrak{g}}$ is
automatic, being an action Lie algebroid [6]. The difficulty in dealing with
these spaces lies in the fact that the $G$-action on them is not free, see
[4].

##  4\. Double symplectic groupoids and gauge Poisson groupoids

In order to describe the following construction, we need to recall the
following construction. A Lie subgroup $H\subset G$ of a Poisson group is
coisotropic if it is coisotropic as a submanifold of $G$111Let $(M,\pi)$ be a
Poisson manifold. A submanifold $C$ of $M$ is coisotropic if
$\pi^{\sharp}(T^{\circ}C)\subset TC$, where $T^{\circ}C$ is the annihilator of
$TC$. ; if $G$ is connected, this is equivalent to the annihilator
$\mathfrak{h}^{\circ}\subset\mathfrak{g}^{*}$ being a Lie subalgebra. If a
Poisson group acts in a Poisson fashion on a Poisson manifold, then the
quotient of the manifold by a coisotropic subgroup is a Poisson manifold
again, provided it is smooth [41, Thm. 6].

Let $(G,\pi_{G})$ be a Poisson group acting in a Poisson fashion on a Poisson
manifold $(M,\pi_{M})$ If the $G$-action is free and proper, then $M/G$
inherits a unique Poisson structure such that the projection map is a Poisson
morphism $M\rightarrow M/G$ [41]. Now consider the Poisson manifold
$M\times\overline{M}$, which is the product $M\times M$ endowed with the
Poisson bivector $(\pi_{M},-\pi_{M})$. We have that the action of the Poisson
group $G\times\overline{G}=(G\times G,(\pi_{G},-\pi_{G}))$ on
$M\times\overline{M}$ is Poisson again and the diagonal subgroup
$G\hookrightarrow G\times\overline{G}$ is a coisotropic subgroup. Therefore,
the quotient by the diagonal action $(M\times\overline{M})/G$ is a Poisson
manifold again. For a manifold $M$, the associated _pair groupoid_ is $M\times
M\rightrightarrows M$ with source and target the projections on $M$, the
multiplication is $\mathtt{m}((x,y),(y,z))=(x,z)$, the unit map $M\rightarrow
M\times M$ is the diagonal inclusion and the inversion is given by
$(x,y)\mapsto(y,x)$. Since $G$ acts by automorphisms on $M\times
M\rightrightarrows M$, the quotient

(6) $\displaystyle((M\times\overline{M})/G,\Pi)\rightrightarrows M/G$

is Lie groupoid again, called a gauge groupoid [20]. It turns out that the
Poisson structure on this Lie groupoid is compatible with the groupoid
structure in the following sense.

######  Definition 4.1 ([44]).

A Poisson groupoid is a Lie groupoid $\mathcal{G}\rightrightarrows M$ with a
Poisson structure on $\mathcal{G}$ such that the graph of the multiplication
map is a coisotropic submanifold of
$\mathcal{G}\times\mathcal{G}\times\overline{\mathcal{G}}$, where
$\overline{\mathcal{G}}$ denotes $\mathcal{G}$ with the opposite Poisson
structure.

Poisson groups and symplectic groupoids (seen as Poisson manifolds) are
extreme examples of Poisson groupoids. The pair groupoid
$M\times\overline{M}\rightrightarrows M$ gives us another family of examples.
Since the projection map
$M\times\overline{M}\rightarrow((M\times\overline{M})/G,\Pi)$ is a Lie
groupoid morphism and a Poisson morphism, the bivector field $\Pi$ makes (6)
into a Poisson groupoid, this fact was first observed by J.-H. Lu and her
collaborators. Since we are dealing with Poisson groupoids, we can ask a more
refined integrability question about this gauge Poisson groupoid. Some of the
symplectic integrations of a Poisson groupoid may carry a double symplectic
groupoid structure.

####  4.0.1. Double symplectic groupoids

######  Definition 4.2 ([7, 31]).

A groupoid object in the category of topological groupoids is called a double
topological groupoid and it is denoted by a diagram of the following kind

$\textstyle{\mathcal{G}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{H\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{K\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{S,}$

where each of the sides represents a groupoid structure and the structure maps
of $\mathcal{G}$ over $H$ are groupoid morphisms with respect to
$\mathcal{G}\rightrightarrows K$ and $H\rightrightarrows S$. A double
topological groupoid as in the previous diagram is a double Lie groupoid if
the following conditions are met: (1) each of the side groupoids is a smooth
groupoid, (2) $H$ and $K$ are Lie groupoids over $S$, and (3) the double
source map
$(\mathtt{s}^{H},\mathtt{s}^{K}):\mathcal{G}\rightarrow{H}\times_{S}{K}$ is a
surjective submersion (the superindices $\quad{}^{H},\quad^{K}$ denote the
groupoid structures $\mathcal{G}\rightrightarrows H$,
$\mathcal{G}\rightrightarrows K$ respectively).

######  Definition 4.3 ([30]).

A double Lie groupoid $\mathcal{G}$ with sides $K$ and $H$ over $S$ is a
double symplectic groupoid if there is a symplectic structure on $\mathcal{G}$
making it into a symplectic groupoid over both $K$ and $H$.

In the previous definition, the Poisson structures induced on $K$ and on $H$
make them into Poisson groupoids over $S$, see [32]. If the Poisson structure
on a Poisson groupoid is integrable by a double symplectic groupoid, we say
that the Poisson groupoid is integrable.

###  4.1. Integrability of gauge Poisson groupoids in the complete case

Now we shall see that a gauge Poisson groupoid as in (6) is integrable by a
double symplectic groupoid if $G$ is complete.

######  Theorem 4.4.

Let $G$ be a complete Poisson group acting freely and properly on a Poisson
manifold $M$. If $M$ is integrable, then the gauge Poisson groupoid
$(M\times\overline{M})/G\rightrightarrows M/G$ is integrable by a double
symplectic groupoid.

###### Proof.

Let $G$ be a Poisson group acting freely and properly on a a Poisson manifold
$M$ by a Poisson action and suppose that $M$ is integrable. Let
$\Sigma(M)\rightrightarrows M$ be the source-simply-connected integration of
$M$. Then we have a Lie groupoid morphism $\mu:\Sigma(M)\rightarrow G^{*}$
which is a moment map for a Poisson $\mathfrak{g}$-action on $\Sigma(M)$ [9,
42]. In that case, $(\mu,\mu):\Sigma(M)\times\overline{\Sigma(M)}\rightarrow
G^{*}\times\overline{G^{*}}$ is also a Lie groupoid morphism and a moment map
for a $\mathfrak{g}\times\mathfrak{g}$-action. Then
$(\mu,\mu)^{-1}(G^{*}_{\Delta})$ is a double Lie groupoid with sides
$\Sigma(M)$ and $M\times\overline{M}$, where $G^{*}_{\Delta}\hookrightarrow
G^{*}\times\overline{G^{*}}$ is the diagonal inclusion. If $G$ is complete,
then the $\mathfrak{g}\times\mathfrak{g}$-action on
$\Sigma(M)\times\overline{\Sigma(M)}$ is already integrable by a $G\times
G$-action, see [22, Thm. 1]. So we can consider the diagonal action restricted
to $(\mu,\mu)^{-1}(G^{*}_{\Delta})$. We have that
$(\mu,\mu)^{-1}(G^{*}_{\Delta})/G\rightrightarrows(M\times\overline{M})/G$ is
a symplectic groupoid integrating the Poisson structure $\Pi$, see the proof
of [22, Thm. 3]. On the other hand, the diagonal $G$-action on
$\Sigma(M)\times\overline{\Sigma(M)}$ clearly preserves the pair groupoid
structure $\Sigma(M)\times\overline{\Sigma(M)}\rightrightarrows\Sigma(M)$, so
we have a double Lie groupoid:

$\textstyle{(\mu,\mu)^{-1}(G^{*}_{\Delta})/G\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\Sigma(M)/G\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(M\times\overline{M})/G\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{M/G.}$

Finally, the symplectic structure on $(\mu,\mu)^{-1}(G^{*}_{\Delta})/G$ is
also multiplicative with respect to
$(\mu,\mu)^{-1}(G^{*}_{\Delta})/G\rightrightarrows\Sigma(M)/G$, since this is
just a symplectic reduction of a pair symplectic groupoid. Therefore, we get a
double symplectic groupoid over the gauge Poisson groupoid (6) as desired. ∎

######  Remark 4.5.

We do not know if we can remove the completeness condition on $G$ in the
previous theorem. If we knew that the $\mathfrak{g}\times\mathfrak{g}$-action
on $\Sigma(M)\times\overline{\Sigma(M)}$ restricted to the diagonal
$\mathfrak{g}$ integrates to a $G$-action on $(\mu,\mu)^{-1}(G^{*}_{\Delta})$,
then we could conclude that the quotient $(\mu,\mu)^{-1}(G^{*}_{\Delta})/G$ is
a double symplectic groupoid integrating the gauge Poisson groupoid (6).
Unfortunately, we cannot adapt Theorem 1.1 to this situation since it only
tells us how to produce $G$-actions by automorphisms and, in the complete
case, the $G$-action on $(\mu,\mu)^{-1}(G^{*}_{\Delta})$ is twisted by the
moment map, see [22].

######  Remark 4.6.

As a consequence of [5, Proposition 7], we have that the
$(\mu,\mu)^{-1}(G^{*}_{\Delta})/G$-orbits of the units in $\Sigma(M)/G$ and in
$(M\times\overline{M})/G$ are symplectic groupoids themselves. So we get in
this way a number of nontrivial examples of symplectic groupoids. Let us
notice that the symplectic leaves of the units in
$(M\times\overline{M})/G\rightrightarrows M/G$ also give us symplectic
groupoids even when $M/G$ is not integrable [5, Proposition 12].

######  Remark 4.7.

The crucial fact in the proof of Theorem 4.4 is that
$(\mu,\mu):\Sigma(M)\times\Sigma(M)\rightarrow G^{*}\times G^{*}$ is a
morphism of double Poisson groupoids, where
$\Sigma(M)\times\overline{\Sigma(M)}$ is seen as a double symplectic groupoid
with sides $\Sigma(M)$ and $M\times\overline{M}$ and
$G^{*}\times\overline{G^{*}}\rightrightarrows G^{*}$ is seen as a Poisson
2-group [13]. So we could formulate and prove a more general result about the
integrability of quotients of Poisson groupoids by actions of coisotropic Lie
2-subgroups of Poisson 2-groups. Due to a certain lack of examples in this
generality, we limit ourselves to the current formulation.

The simplest examples of double symplectic groupoids associated to gauge
Poisson groupoids are the following.

######  Example 4.8.

Let $Q$ be a closed Poisson subgroup of a complete Poisson group $G$. Then the
quotient by the diagonal action by left translations
$(G\times\overline{G})/Q\rightrightarrows G/Q$ is a gauge Poisson groupoid.
Since $G$ is complete, its source-simply-connected integration is the action
groupoid $G^{*}\times G\rightrightarrows G$ associated to the dressing action
$(u,x)\mapsto{}^{u}g$, where $G^{*}$ is the 1-connected integration of
$\mathfrak{g}^{*}$. The lift of the $G$-action on $G$ by left translations to
$G^{*}\times G$ is given by $a\cdot(u,b)=({}^{a}u,a^{u}b)$, see [22, Example
3.12]. The moment map $\mu:G^{*}\times G\rightarrow G^{*}$ is the projection
on the first factor. Since $Q$ is a Poisson subgroup of $G$, the annihilator
$\mathfrak{q}^{\circ}\subset\mathfrak{g}^{*}$ is an ideal and so there is a
Lie group morphism $p:G^{*}\rightarrow Q^{*}$ integrating the projection
$\mathfrak{g}^{*}\rightarrow\mathfrak{q}^{*}\cong\mathfrak{g}^{*}/\mathfrak{q}^{\circ}$.
Then the moment map for the lifted $Q$-action to $G^{*}\times G$ is
$p\circ\mu:G^{*}\times G\rightarrow Q^{*}$. As a consequence of Theorem 4.4,
$(p\circ\mu,p\circ\mu)^{-1}(Q_{\Delta}^{*})/Q$ is a double symplectic groupoid
integrating the gauge Poisson groupoid
$(G\times\overline{G})/Q\rightrightarrows G/Q$.

More generally, we can do the following. Let $G$ be a Poisson group and let
$Q\hookrightarrow G$ be a closed Poisson subgroup. Suppose that there is a
(left) Poisson action of $Q$ on a Poisson manifold $Y$. Then the action
$(G\times Y)\times(Q\times\overline{Q})\rightarrow G\times Y$ given by
$(g,y,a,b)\mapsto(ga,b^{-1}y)$ is a Poisson action, where $\overline{Q}$
denotes $Q$ with the opposite Poisson structure. Since the diagonal subgroup
$Q_{\Delta}\hookrightarrow Q\times\overline{Q}$ is coisotropic, the associated
bundle $G\times_{Q}Y:=(G\times Y)/Q$ is a Poisson manifold. For instance, if
$Q_{i}\subset G$ is a closed Poisson subgroup for $i=1\dots n$, then the
quotient $G\times_{Q_{1}}\times\dots\times_{Q_{n-1}}G/Q_{n}$ is integrable,
see [29] for a detailed description of this family of examples. In order to
apply Theorem 4.4, we can take $M=G\times_{Q}\times\dots\times_{Q}G$ as
before. Now consider the residual $Q$-action on the last factor. If $Q$ is
complete, then Theorem 4.4 implies that
$(M\times\overline{M})/Q\rightrightarrows M/Q$ is integrable by a double
symplectic groupoid, see [28] for Poisson groupoids related to this example.

## References

  * [1] A. Alekseev and Y. Kosmann-Schwarzbach  “Manin pairs and moment maps”  In _Journal of Differential geometry_ 56.1 Lehigh University, 2000, pp. 133–165
  * [2] A. Alekseev, A. Malkin and E. Meinrenken  “Lie group valued moment maps”  In _Journal of Differential Geometry_ 48.3, 1998, pp. 445–495
  * [3] A. Alekseev, E. Meinrenken and Y. Kosmann-Schwarzbach  “Quasi-Poisson manifolds”  In _Canadian Journal of Mathematics_ 54, 2002, pp. 3–29
  * [4] D. Álvarez  “Integrability of quotients in Poisson and Dirac geometry”, 2019
  * [5] D. Álvarez  “Leaves of stacky Lie algebroids”  In _Comptes Rendus. Mathématique_ 358.2, 2020, pp. 217–226
  * [6] K. Behrend, P. Xu and B. Zhang  “Equivariant gerbes over compact simple Lie groups”  In _Comptes Rendus Mathématique_ , 2003
  * [7] R. Brown and K. C. H. Mackenzie  “Determination of a double Lie groupoid by its core diagram”  In _Journal of pure and applied algebra_ 80.3 Elsevier, 1992, pp. 237–272
  * [8] H. Bursztyn and A. Cabrera  “Multiplicative forms at the infinitesimal level”  In _Math. Annalen_ 353, 2012, pp. 663–705
  * [9] H. Bursztyn, A. Cabrera and M. Hoyo  “Vector bundles over Lie groupoids and algebroids”  In _Advances in Mathematics_ 290, 2016, pp. 163–207
  * [10] H. Bursztyn, M. Crainic, A. Weinstein and C. Zhu  “Integration of twisted Dirac brackets”  In _Duke Mathematical Journal_ 123.3 Duke University Press, 2004, pp. 549–607
  * [11] A. Cabrera and C. Ortiz  “Quotients of multiplicative forms and Poisson reduction”, 2020  URL: arXiv:2008.03416.
  * [12] A. Cattaneo and G. Felder  “Poisson sigma models and symplectic groupoids”  In _Quantization of singular symplectic quotients_ Springer, 2001, pp. 61–93
  * [13] Z. Chen, M. Stiénon and P. Xu  “Poisson 2-groups”  In _Journal of Differential Geometry_ 94.2, 2013, pp. 209–240
  * [14] M. Crainic  “Differentiable and algebroid cohomology, Van Est isomorphisms, and characteristic classes”  In _Comm. Math. Helvetici_ , 2003
  * [15] M. Crainic and R. L. Fernandes  “A geometric approach to Conn’s linearization theorem”  In _Annals of Mathematics_ 173.2, 2011, pp. 1121–1139
  * [16] M. Crainic and R. L. Fernandes  “Integrability of Lie brackets”  In _Annals of Mathematics_ JSTOR, 2003, pp. 575–620
  * [17] M. Crainic and R. L. Fernandes  “Integrability of Poisson brackets”  In _Journal of Differential Geometry_ 66.1 Lehigh University, 2004, pp. 71–137
  * [18] M. Crainic, R. L. Fernandes and D. Martínez  “Poisson manifolds of compact types (PMCT 1)”  In _Journal für die reine und angewandte Mathematik (Crelles Journal)_ De Gruyter, 2017
  * [19] V. G. Drinfeld  “Hamiltonian structures on Lie groups, Lie bialgebras and the geometric meaning of the classical Yang-Baxter equations”  In _Soviet Math. Dokl._ , 1983, pp. 68–71
  * [20] J. P. Dufour and N. T. Zung  “Poisson structures and their normal forms”  Birkhäuser, 2006
  * [21] R. L. Fernandes, J. P. Ortega and T. S. Ratiu  “The moment map in Poisson geometry”  In _American Journal of Mathematics_ 131.5, 2009, pp. 1261–1310
  * [22] R. L. Fernandes and D. Iglesias Ponte  “Integrability of Poisson-Lie group actions”  In _Letters in Mathematical Physics_ 90.1 Springer, 2009, pp. 137–159
  * [23] E. Hawkins  “A groupoid approach to quantization”  In _Journal of Symplectic Geometry_ 6.1, 2008, pp. 61–125
  * [24] P. J. Higgins and K. C. H. Mackenzie  “Algebraic constructions in the category of Lie algebroids”  In _Journal of Algebra_ 129.1 Elsevier, 1990, pp. 194–230
  * [25] M. V. Karasev  “Analogues of objects of the theory of Lie groups for nonlinear Poisson brackets”  In _Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya_ 50.3, 1986, pp. 508–538
  * [26] D. Li-Bland and P. Severa  “Quasi-Hamiltonian groupoids and multiplicative Manin pairs”  In _International Mathematics Research Notices_ Oxford University Press, 2011, pp. 2295–2350
  * [27] J.-H. Lu  “Multiplicative and affine Poisson structures on Lie groups”, 1990
  * [28] J.-H. Lu and V. Mouquin  “Double Bruhat cells and symplectic groupoids”  In _Transformation Groups_ 23, 2018, pp. 765–800
  * [29] J.-H. Lu and V. Mouquin  “Mixed product Poisson structures associated to Poisson Lie groups and Lie bialgebras”  In _International Mathematics Research Notices_ , 2017, pp. 5919–5976
  * [30] J.-H. Lu and A. Weinstein  “Poisson Lie groups, dressing transformations, and Bruhat decompositions”  In _Journal of Differential Geometry_ 31.2, 1990, pp. 501–526
  * [31] K. C. H. Mackenzie  “Double Lie algebroids and second-order geometry, I”  In _Advances in Mathematics_ 94.2, 1992, pp. 180–239
  * [32] K. C. H. Mackenzie  “Double Lie algebroids and second-order geometry, II”  In _Advances in Mathematics_ 154.1, 2000, pp. 46–75
  * [33] K. C. H. Mackenzie  “General theory of Lie groupoids and Lie algebroids”  Cambridge University Press, 2005
  * [34] K. C. H. Mackenzie and P. Xu  “Integration of Lie bialgebroids”  In _Topology_ 39.3 Elsevier, 2000, pp. 445–467
  * [35] K. C. H. Mackenzie and P. Xu  “Lie bialgebroids and Poisson groupoids”  In _Duke Mathematical Journal_ 73.2 Duke University Press, 1994, pp. 415–452
  * [36] K. Mikami and A. Weinstein  “Moments and reduction for symplectic groupoids”  In _Publ. Res. Inst. Math. Sci._ 24.1, 1988, pp. 121–140
  * [37] I. Moerdijk and J. Mrcun  “Introduction to foliations and Lie groupoids”  Cambridge University Press, 2003
  * [38] I. Moerdijk and J. Mrcun  “On integrability of infinitesimal actions”  In _American Journal of Mathematics_ 124.3, 2000, pp. 567–593
  * [39] D. Iglesias Ponte, C. Laurent-Gengoux and P. Xu  “Universal lifting theorem and quasi-Poisson groupoids”  In _Journal of the European Mathematical Society_ 14.3, 2012, pp. 681–731
  * [40] D. Roytenberg  “Courant algebroids, derived brackets and even symplectic supermanifolds”  In _arXiv preprint math/9910078_ , 1999
  * [41] M. A. Semenov-Tian-Shansky  “Dressing transformations and Poisson group actions”  In _Publications of the Research Institute for Mathematical Sciences_ 21.6 Research Institute forMathematical Sciences, 1985, pp. 1237–1260
  * [42] L. Stefanini  “On morphic actions and integrability of LA-groupoids”, 2008
  * [43] A. Y. Vaintrob  “Lie algebroids and homological vector fields”  In _Russian Mathematical Surveys_ 52.2, 1997, pp. 428–429
  * [44] A. Weinstein  “Coisotropic calculus and Poisson groupoids”  In _Journal of the Mathematical Society of Japan_ 40.4 一般社団法人 日本数学会, 1988, pp. 705–727
  * [45] A. Weinstein  “Symplectic groupoids and Poisson manifolds”  In _Bulletin of the American mathematical Society_ 16.1, 1987, pp. 101–104


\textsf{{wrlp}}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$

The proof rule if is sound by Lemma E.21.

$I\leq\left[{b}\right]\cdot X+\left[{\neg b}\right]\cdot Y$
$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(I\mid\xi\right)$ while $I\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$

The proof rule while is sound by Lemma E.25.

div $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{diverge}}\rrbracket\left(Y\mid\xi\right)$

The proof rule div is sound by Lemma C.25.

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

The proof rule p-choice is sound by Lemma E.31.

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

The proof rule atomic is sound by Lemma E.35.

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

The proof rule share is sound by Lemma E.40.

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

The proof rule concur is sound by Lemma E.45.

$X^{\prime}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(X\right)$
$Y^{\prime}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y\right)$ $C$ is
AST wrt $S$ $a\in\mathbb{R}_{\geq 0}$ superlin $a\cdot
X^{\prime}+Y^{\prime}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(a\cdot
X+Y\right)$

The proof rule superlin is sound by Lemma E.64.

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

The proof rule wlp-wrlp is sound by Lemma E.66.

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$
$\text{Write}(C)\cap\text{Vars}\,(Z)=\emptyset$ frame
$X\mathbin{{\star}}Z\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y\mathbin{{\star}}Z\mid\xi\right)$

The proof rule frame is sound by Lemma E.68.

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

The proof rule atom is sound by Lemma E.70.

$X\leq X^{\prime}$ $X^{\prime}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y^{\prime}\mid\xi\right)$
$Y^{\prime}\leq Y$ monotonic $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y\mid\xi\right)$

The proof rule monotonic is sound by Lemma E.1.

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $X^{\prime}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y^{\prime}\mid\xi\right)$ max
$\max\left\\{\,{X},\>{X^{\prime}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\max\left\\{\,{Q},\>{Q^{\prime}}\,\right\\}\mid\xi\right)$

The proof rule max is sound by Lemma E.72.

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $X^{\prime}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y^{\prime}\mid\xi\right)$ $\xi$ precise min
$\min\left\\{\,{X},\>{X^{\prime}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\min\left\\{\,{Y},\>{Y^{\prime}}\,\right\\}\mid\xi\right)$

The proof rule min is sound by Lemma E.74.

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $X^{\prime}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y^{\prime}\mid\xi\right)$ $\xi$ precise
$\text{Write}(C)\cap\text{Vars}\,(e)=\emptyset$ convex $e\cdot X+(1-e)\cdot
X^{\prime}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(e\cdot Y+(1-E)\cdot
Y^{\prime}\mid\xi\right)$

The proof rule convex is sound by Lemma E.86.

##  Appendix F Details on Examples

###  F.1 Additional Details on the Running Example

To recap, we are given the resource invariant
$\xi=\max\left\\{\,{\left[{r\mapsto
0}\right]},\>{\left[{r\mapsto-1}\right]}\,\right\\}$ and have already proven:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{0.5\mathbin{{\star}}1\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$
$\displaystyle\left.\begin{aligned} &\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{0.5\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\left\\{\,{\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}0}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}1}\,\right\\}\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\
\xi}\end{aligned}\quad\middle\|\quad\begin{aligned}
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\mathbin{{\star}}\xi}\\\
&y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}\,;\,\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}\mathbin{{\star}}\xi}\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\textnormal{{while}}\left(\,{y=-1}\,\right)\left\\{\,{y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}}\,\right\\}\,;\,\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{y=0}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\xi}\end{aligned}\right.$ $\displaystyle\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\
\vphantom{G^{\prime}}{1\mathbin{{\star}}\left[{y=0}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$

The mutation $\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}-1$ together
with the atom rule gives us the inequality

$0.5\mathbin{{\star}}\left[{r\mapsto\,{-}\,}\right]\leq\left[{r\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{r\mapsto-1}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}0.5\mathbin{{\star}}\max\left\\{\,{\left[{r\mapsto
0}\right]},\>{\left[{r\mapsto-1}\right]}\,\right\\})\leavevmode\nobreak\ .$

However, it is easy to verify that
$(\left[{r\mapsto-1}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}0.5\mathbin{{\star}}\max\left\\{\,{\left[{r\mapsto
0}\right]},\>{\left[{r\mapsto-1}\right]}\,\right\\})$ simplifies to $0.5$,
which results in the given lower bound.

For the probabilistic choice we have:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{0.5\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{0.5\cdot 1+0.5\cdot 0\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$
$\displaystyle\left\\{\,{\begin{aligned} &\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{1\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}0\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\
\xi}\end{aligned}}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{\begin{aligned}
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{0\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}1\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\end{aligned}}\,\right\\}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$

The right part is rather simple, as we can always lower bound anything by
zero. The left part holds since with $\left[{r\mapsto 0}\right]$ the mutation
is satisfied, however the value before mutating $r$ is unknown. We can lower
bound the resulting preexpectation
$1\mathbin{{\star}}\left[{r\mapsto\,{-}\,}\right]$ by
$1\mathbin{{\star}}\max\left\\{\,{\left[{r\mapsto-1}\right]},\>{\left[{r\mapsto
0}\right]}\,\right\\}$ and thus realise the resource invariant again. For the
loop invariant
$\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}$ we
have:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$
$\displaystyle y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$

The lookup operation here results in both $\left[{y=0}\right]$ and
$\left[{y=1}\right]$ to be evaluated to $1$ if $\left[{r\mapsto 0}\right]$ and
$\left[{r\mapsto-1}\right]$, respectively. Our resource invariant guarantees
this, thus we obtain the expectation $1$ and lower bound it by
$\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}$.
Lastly we check that it is indeed a loop invariant:

$\displaystyle\left[{y=-1}\right]\cdot\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}+\left[{y\neq-1}\right]\cdot\left[{y=0}\right]$
$\displaystyle=$ $\displaystyle\left[{y=-1}\right]+\left[{y=0}\right]$
$\displaystyle=$
$\displaystyle\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}$

###  F.2 Example: A Producer, a Consumer and a lossy Channel

Here we have the following program $C$:
$\displaystyle l\mathrel{\textnormal{{:=}}}0\,;\,$ $\displaystyle
y_{1},y_{2},y_{3}\mathrel{\textnormal{{:=}}}k\,;\,$
$\displaystyle\left.\begin{aligned} &\textnormal{{while}}\left(\,{y_{1}\geq
0}\,\right)\left\\{\right.\\\
&\quad\left\\{\,{x_{1}\mathrel{\textnormal{{:=}}}1}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{x_{1}\mathrel{\textnormal{{:=}}}2}\,\right\\}\,;\,\\\
&\quad\texttt{<}\,z_{1}+y_{1}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{1}\,;\,\\\
&\quad y_{1}\mathrel{\textnormal{{:=}}}y_{1}-1\\\
&\\}\end{aligned}\quad\middle\|\quad\left.\begin{aligned} &\\\\[-10.00002pt]
&\textnormal{{while}}\left(\,{y_{2}\geq 0}\,\right)\left\\{\right.\\\ &\quad
x_{2}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{1}+y_{2}\,\texttt{>}\,;\,\\\
&\quad\textnormal{{if}}\,\left(\,{x_{2}\neq 0}\,\right)\,\\{\\\
&\quad\quad\quad\\{\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{2}\\}\\\
&\quad\quad\mathrel{\left[\,p\,\right]}\\\
&\quad\quad\quad\\{\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}-1\\}\,;\,\\\
&\quad\quad y_{2}\mathrel{\textnormal{{:=}}}y_{2}-1\\\ &\quad\\}\\\ &\\}\\\
&\\\\[-10.00002pt] \end{aligned}\quad\middle\|\quad\begin{aligned}
&\textnormal{{while}}\left(\,{y_{3}\geq 0}\,\right)\left\\{\right.\\\ &\quad
x_{3}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\,;\,\\\
&\quad\textnormal{{if}}\,\left(\,{x_{3}\neq 0}\,\right)\,\\{\\\
&\quad\quad\textnormal{{if}}\,\left(\,{x_{3}\neq-1}\,\right)\,\\{l\mathrel{\textnormal{{:=}}}l+1\\}\,;\,\\\
&\quad\quad y_{3}\mathrel{\textnormal{{:=}}}y_{3}-1\\\ &\quad\\}\\\
&\\}\end{aligned}\right.\right.$
We use the resource invariant $\xi_{J}$ for a set $J$. The set $J$ encodes
which locations in the array starting from $z_{2}$ will have an error value of
$-1$ or a valid value of $1$ or $2$ after the channel inserts data into it. We
use a big separating multiplication to connect all the possible instantiations
using separating multiplication. That is, $\underset{}{\bigstar}\\{X\\}=X$ and
$\underset{}{\bigstar}(\\{X\\}\cup
A)=X\mathbin{{\star}}\underset{}{\bigstar}A$ for a non-empty and countable set
$A$. $\xi_{J}$ declares that all locations between $z_{1}$ and $z_{1}+k$ have
either value $0$, $1$ or $2$ and all locations between $z_{2}$ and $z_{2}+k$
have values $0$, $1$ or $2$ if the offset is in $J$ and $0$ or $-1$ if the
offset is not in $J$. The value $0$ is always possible for all locations
between $z_{i}$ and $z_{i}+k$ since we assume $0$ to be the initial value. We
connect the predicates declaring possible values for the location $z_{j}+i$
using a maximum, which acts as a qualitative disjunction here.

$\displaystyle\xi_{J}\quad=$
$\displaystyle\quad\left(\underset{i\in\\{0,\dots,k\\}}{\bigstar}\leavevmode\nobreak\
\leavevmode\nobreak\ \max\left\\{\,{\left[{z_{1}+i\mapsto
0}\right],\>\left[{z_{1}+i\mapsto 1}\right],\>\left[{z_{1}+i\mapsto
2}\right]}\,\right\\}\right)$ $\displaystyle\leavevmode\nobreak\
\mathbin{{\star}}\left(\underset{i\in\\{0,\dots,k\\}\cap
J}{\bigstar}\max\left\\{\,{\left[{z_{2}+i\mapsto
0}\right],\>\left[{z_{2}+i\mapsto 1}\right],\>\left[{z_{2}+i\mapsto
2}\right]}\,\right\\}\right)$ $\displaystyle\leavevmode\nobreak\
\mathbin{{\star}}\left(\underset{i\in\\{0,\dots,k\\}\setminus
J}{\bigstar}\max\left\\{\,{\left[{z_{2}+i\mapsto
0}\right],\>\left[{z_{2}+i\mapsto-1}\right]}\,\right\\}\right)\leavevmode\nobreak\
.$

We will leave out computations of inequalities $X\leq Y$ for the sake of
brevity and give an explanation instead. Since our representation of
expectations may grow in size, we use a curly bracket after the
$\fatslash\leavevmode\nobreak\ $ symbol to denote expectations which are too
long for one line. Our goal is to prove a lower bound on the probability that
$l=|J|$ is realised after termination. If $J$ contains numbers outside the
range between $0$ and $k$, we may as well replace $|J|$ with
$|J\cap\\{0,\dots,k\\}|$. We now prove an invariant for each of the three
subprograms.

For the producer $C_{1}$, we prove the invariant $I_{1}=1$ with respect to the
postexpectation $1$ and resource invariant $\xi_{J}$. This shows indeed that
the probability of safe execution of the loop is one and that our resource
invariant $\xi_{J}$ almost always holds.

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\left\\{\,{\begin{aligned} &\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{1\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{1\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}\\\
&x_{1}\mathrel{\textnormal{{:=}}}1\\\ &\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{x_{1}\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\xi_{J}}\end{aligned}}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{\begin{aligned}
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{2\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}\\\
&x_{1}\mathrel{\textnormal{{:=}}}2\\\ &\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{x_{1}\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\xi_{J}}\end{aligned}}\,\right\\}\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{x_{1}\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\texttt{<}\,z_{1}+y_{1}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{1}\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$ $\displaystyle
y_{1}\mathrel{\textnormal{{:=}}}y_{1}-1$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$

The inequality

$\left[{x_{1}\in\\{0,\dots,2\\}}\right]\mathbin{{\star}}\xi_{J}\leq\left[{z_{1}+y_{1}\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{z_{1}+y_{1}\mapsto
x_{1}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(1\mathbin{{\star}}\xi_{J}))$

resulting from the mutation
$\texttt{<}\,z_{1}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{1}$ together
with the atom rule holds because for $\left[{z_{1}+y_{1}\mapsto
x_{1}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(1\mathbin{{\star}}\xi_{J})$
to be non-zero, $x_{1}$ must coincide with $\xi_{J}$ – thus $x_{1}$ has to be
either $0$, $1$ or $2$. Furthermore, we have that $\left[{z_{1}+y_{1}\mapsto
i}\right]\leq\left[{z_{1}+y_{1}\mapsto\,{-}\,}\right]$ holds for every $i$,
and obtain by this that $i\in\\{0,\dots,2\\}$, with which we re-establish
$\xi_{J}$. We have $\left[{y_{1}\geq 0}\right]\cdot
1+\left[{y_{1}<0}\right]\cdot 1=1$ and therefore $1$ is a loop invariant.

For the channel $C_{2}$, we use the shorthand notation $P(y)$ to denote
cumulated probability mass and define it as

$\displaystyle P(y)\quad=\quad p^{|\\{0,\dots,y\\}\cap
J|}\cdot(1-p)^{|\\{0,\dots,y\\}\setminus J|}\leavevmode\nobreak\ .$

This shorthand notation gives us the probability that all data with offset $0$
up to $y$ are transferred according to $J$. That is, if an element should have
been transferred successfully, we multiply with $p$ and if not with $1-p$ for
every location up to $y_{2}$. We prove for the invariant $I_{2}=\left[{0\leq
y_{2}\leq k}\right]\cdot P(y_{2})+\left[{y_{2}<0}\right]$ with respect to the
postexpectation $1$ and resource invariant $\xi_{J}$:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\begin{aligned} &\left[{x_{2}\neq 0}\right]\cdot\left[{0\leq y_{2}\leq
k}\right]\cdot P(y_{2})\\\ &+\left[{x_{2}=0}\right]\cdot\left(\left[{0\leq
y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\right)\end{aligned}\leavevmode\nobreak\
\leavevmode\nobreak\ \stretchrel*{|}{\begin{aligned} &\left[{x_{2}\neq
0}\right]\cdot\left[{0\leq y_{2}\leq k}\right]\cdot P(y_{2})\\\
&+\left[{x_{2}=0}\right]\cdot\left(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\right)\end{aligned}}\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}\right.$ $\displaystyle
x_{2}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{1}+y_{2}\,\texttt{>}\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\begin{aligned} &\left[{x_{2}\neq 0}\right]\cdot\left[{0\leq y_{2}\leq
k}\right]\cdot P(y_{2}-1)\cdot(p\cdot\left[{y_{2}\in
J}\right]\cdot\left[{x_{2}\in\\{1,\dots,2\\}}\right]\\\
&\quad\quad+(1-p)\cdot\left[{y_{2}\not\in J}\right])\\\
&+\left[{x_{2}=0}\right]\cdot\left(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\right)\end{aligned}\leavevmode\nobreak\
\leavevmode\nobreak\ \stretchrel*{|}{\begin{aligned} &\left[{x_{2}\neq
0}\right]\cdot\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2}-1)\cdot(p\cdot\left[{y_{2}\in
J}\right]\cdot\left[{x_{2}\in\\{1,\dots,2\\}}\right]\\\
&\quad\quad+(1-p)\cdot\left[{y_{2}\not\in J}\right])\\\
&+\left[{x_{2}=0}\right]\cdot\left(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\right)\end{aligned}}\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}\right.$
$\displaystyle\textnormal{{if}}\,\left(\,{x_{2}\neq 0}\,\right)\,\\{$
$\displaystyle\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2}-1)\cdot\left(p\cdot\left[{y_{2}\in
J}\right]\cdot\left[{x_{2}\in\\{0,\dots,2\\}}\right]+(1-p)\cdot\left[{y_{2}\not\in
J}\right]\right)\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\\{$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2}-1)\right)\cdot\left[{y_{2}\in
J}\right]\cdot\left[{x_{2}\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left(\left[{1\leq y_{2}\leq k}\right]\cdot
P(y_{2}-1)+\left[{y_{2}=0}\right]\right)\cdot\left[{y_{2}\in
J}\right]\cdot\left[{x_{2}\in\\{0,\dots,2\\}}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{2}$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{1\leq y_{2}\leq k+1}\right]\cdot
P(y_{2}-1)+\left[{y_{2}<1}\right]\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\\}$ $\displaystyle\quad\mathrel{\left[\,p\,\right]}$
$\displaystyle\quad\quad\\{$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2}-1)\right)\cdot\left[{y_{2}\not\in J}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left(\left[{1\leq y_{2}\leq k}\right]\cdot
P(y_{2}-1)+\left[{y_{2}=0}\right]\right)\cdot\left[{y_{2}\not\in
J}\right]\leavevmode\nobreak\ \leavevmode\nobreak\ |\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}-1\,;\,$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{1\leq y_{2}\leq k+1}\right]\cdot
P(y_{2}-1)+\left[{y_{2}<1}\right]\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad\\}$ $\displaystyle\quad\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{\left[{1\leq y_{2}\leq
k+1}\right]\cdot P(y_{2}-1)+\left[{y_{2}<1}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{2}-1\leq k}\right]\cdot
P(y_{2}-1)+\left[{y_{2}-1<0}\right]\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$ $\displaystyle\quad
y_{2}\mathrel{\textnormal{{:=}}}y_{2}-1$
$\displaystyle\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$ $\displaystyle\\}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$

We explain some of the difficult inequalities in the previous proof. We start
with the inequality

$\displaystyle\leavevmode\nobreak\ \left(\left(\left[{1\leq y_{2}\leq
k}\right]\cdot
P(y_{2}-1)+\left[{y_{2}=0}\right]\right)\cdot\left[{y_{2}\not\in
J}\right]\right)\mathbin{{\star}}\xi_{J}$ $\displaystyle\leq$
$\displaystyle\leavevmode\nobreak\
\left[{z_{2}+y_{2}\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{z_{2}+y_{2}\mapsto-1}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\left(\left[{1\leq
y_{2}\leq k+1}\right]\cdot
P(y_{2}-1)+\left[{y_{2}<1}\right]\right)\mathbin{{\star}}\xi_{J}$

resulting from the mutation
$\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}-1$ together
with the atom rule. This inequality holds since for the part
$\left[{z_{2}+y_{2}\mapsto-1}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\dots$
to be non-zero, we require $y_{2}\not\in J$ due to $\xi_{J}$. We lower bound
all evaluations where $y_{2}<0$ by $0$ as we can not infer any information
about these locations from $\xi_{J}$. Afterwards, we can lower bound
$\left[{z_{2}+y_{2}\mapsto\,{-}\,}\right]$ by $\left[{z_{2}+y_{2}\mapsto
i}\right]$ for every $i$ and thus re-establish $\xi_{J}$.

Next we have the inequality

$\displaystyle\leavevmode\nobreak\ \left(\left(\left[{1\leq y_{2}\leq
k}\right]\cdot P(y_{2}-1)+\left[{y_{2}=0}\right]\right)\cdot\left[{y_{2}\in
J}\right]\cdot\left[{x_{2}\in\\{0,\dots,2\\}}\right]\right)\mathbin{{\star}}\xi_{J}$
$\displaystyle\leq$ $\displaystyle\leavevmode\nobreak\
\left[{z_{2}+y_{2}\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{z_{2}+y_{2}\mapsto
x_{2}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\left(\left[{1\leq
y_{2}\leq k+1}\right]\cdot
P(y_{2}-1)+\left[{y_{2}<1}\right]\right)\mathbin{{\star}}\xi_{J}$

resulting from the mutation
$\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{2}$ together
with the atom rule. Here we assume that the location $y_{2}$ is in $J$ and
obtain that $x_{2}\in\\{0,\dots,2\\}$. We lower bound any outcome of $y_{2}$
not in $J$ by $0$ because we already know that we will eventually set the term
to $0$ due to the previous lookup. Next we establish $\xi_{J}$ back from lower
bounding $\left[{z_{2}+y_{2}\mapsto\,{-}\,}\right]$.

We have the inequality

$\displaystyle\leavevmode\nobreak\ \left[{x_{2}\neq 0}\right]\cdot\left[{0\leq
y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{x_{2}=0}\right]\cdot\left(\left[{0\leq y_{2}\leq
k}\right]\cdot P(y_{2})+\left[{y_{2}<0}\right]\right)\mathbin{{\star}}\xi$
$\displaystyle\leq$
$\displaystyle\sup_{v\in\mathbb{Z}}\left[{z_{1}+y_{2}\mapsto
v}\right]\mathbin{{\star}}(\left[{z_{1}+y_{2}\mapsto
v}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle\leavevmode\nobreak\ (\left[{v\neq 0}\right]\cdot\left[{0\leq
y_{2}\leq k}\right]\cdot P(y_{2}-1)\cdot(p\cdot\left[{y_{2}\in
J}\right]\cdot\left[{v\in\\{1,\dots,2\\}}\right]+(1-p)\cdot\left[{y_{2}\not\in
J}\right])$ $\displaystyle\leavevmode\nobreak\
+\left[{v=0}\right]\cdot\left(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right]\right))\mathbin{{\star}}\xi)$

resulting from the lookup
$x_{2}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{1}+y_{2}\,\texttt{>}$ together
with the atom rule. We will consider both cases separately. Let us assume that
$v$ is not $0$. Then either $y_{2}$ is in $J$ and $v$ is either $1$ or $2$ to
make $p\cdot\left[{y_{2}\in J}\right]\cdot\left[{v\in\\{1,\dots,2\\}}\right]$
not zero, or $y_{2}$ is not in $J$. Then, however, $v$ needs to be $-1$,
because else $\xi_{J}$ will evaluate to zero. Both cases can then be used to
turn $P(y_{2}-1)$ into $P(y_{2})$. In both cases, we can also use
$\left[{z_{1}+y_{2}\mapsto v}\right]$ to re-establish the resource invariant
$\xi_{J}$. If, on the other side, $v$ is $0$, we do not get any new
information, but also do not need to update $P(y_{2})$, and directly re-
establish the resource invariant $\xi_{J}$.

Due to

$\displaystyle\leavevmode\nobreak\ \left[{y_{2}\geq
0}\right]\cdot(\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right])+\left[{y_{2}<0}\right]\cdot 1$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \left[{0\leq y_{2}\leq
k}\right]\cdot P(y_{2})+\left[{y_{2}<0}\right]$

we establish the loop invariant with respect to postexpectation $1$.

For the consumer $C_{3}$ we require a loop invariant that checks if $l$ indeed
matches the size of the set $J$. We prove the loop invariant
$I_{3}=\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{y_{3}+l=|J\cap\\{0,\dots,y_{3}\\}|}\right]$ with respect
to the postexpectation $\left[{l=|J|}\right]$ and the resource invariant
$\xi_{J}$:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle
x_{3}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{2}+y_{3}\,\texttt{>}\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\begin{aligned} &\quad\left[{x_{3}=-1}\right]\cdot\left[{1\leq
y_{3}\leq k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]\\\
&+\left[{x_{3}=-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]\\\
&+\left[{x_{3}\neq 0}\right]\cdot\left[{x_{3}\neq-1}\right]\cdot\left[{1\leq
y_{3}\leq k+1}\right]\cdot\left[{l+1=|J\cap\\{y_{3},\dots,k\\}|}\right])\\\
&+\left[{x_{3}\neq
0}\right]\cdot\left[{x_{3}\neq-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l+1=|J|}\right]\\\
&+\left[{x_{3}=0}\right]\cdot\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]\\\
&+\left[{x_{3}=0}\right]\cdot\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right]\end{aligned}\leavevmode\nobreak\
\leavevmode\nobreak\ \stretchrel*{|}{\begin{aligned}
&\quad\left[{x_{3}=-1}\right]\cdot\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]\\\
&+\left[{x_{3}=-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]\\\
&+\left[{x_{3}\neq 0}\right]\cdot\left[{x_{3}\neq-1}\right]\cdot\left[{1\leq
y_{3}\leq k+1}\right]\cdot\left[{l+1=|J\cap\\{y_{3},\dots,k\\}|}\right])\\\
&+\left[{x_{3}\neq
0}\right]\cdot\left[{x_{3}\neq-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l+1=|J|}\right]\\\
&+\left[{x_{3}=0}\right]\cdot\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]\\\
&+\left[{x_{3}=0}\right]\cdot\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right]\end{aligned}}\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}\right.$
$\displaystyle\textnormal{{if}}\,\left(\,{x_{3}\neq 0}\,\right)\,\\{$
$\displaystyle\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\begin{aligned} &\quad\left[{x_{3}=-1}\right]\cdot\left[{1\leq
y_{3}\leq k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]\\\
&+\left[{x_{3}=-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]\\\
&+\left[{x_{3}\neq-1}\right]\cdot\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l+1=|J\cap\\{y_{3},\dots,k\\}|}\right]\\\
&+\left[{x_{3}\neq-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l+1=|J|}\right]\end{aligned}\leavevmode\nobreak\
\leavevmode\nobreak\ \stretchrel*{|}{\begin{aligned}
&\quad\left[{x_{3}=-1}\right]\cdot\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]\\\
&+\left[{x_{3}=-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]\\\
&+\left[{x_{3}\neq-1}\right]\cdot\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l+1=|J\cap\\{y_{3},\dots,k\\}|}\right]\\\
&+\left[{x_{3}\neq-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l+1=|J|}\right]\end{aligned}}\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}\right.$
$\displaystyle\quad\textnormal{{if}}\,\left(\,{x_{3}\neq-1}\,\right)\,\\{$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l+1=|J\cap\\{y_{3},\dots,k\\}|}\right]+\left[{y_{3}<1}\right]\cdot\left[{l+1=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\quad l\mathrel{\textnormal{{:=}}}l+1$
$\displaystyle\quad\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]+\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\\}\,;\,$ $\displaystyle\quad\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]+\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{3}-1\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]+\left[{y_{3}-1<0}\right]\cdot\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\quad y_{3}\mathrel{\textnormal{{:=}}}y_{3}-1$
$\displaystyle\quad\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\\}$ $\displaystyle\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$

Here we will take a closer look at the inequality

$\displaystyle\leavevmode\nobreak\ (\left[{1\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]+\left[{y_{3}=0}\right]\cdot\left[{l=|J\cap\\{1,\dots,k\\}|}\right])\mathbin{{\star}}\xi_{J}$
$\displaystyle\leq$ $\displaystyle\leavevmode\nobreak\
\sup_{v\in\mathbb{Z}}\left[{z_{2}+y_{2}\mapsto
v}\right]\mathbin{{\star}}(\left[{z_{2}+y_{2}\mapsto
v}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle\quad(\left[{v=-1}\right]\cdot\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l=|J\cap\\{y_{3},\dots,k\\}|}\right]$
$\displaystyle+\left[{v=-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l=|J|}\right]$
$\displaystyle+\left[{v\neq
0}\right]\cdot\left[{v\neq-1}\right]\cdot\left[{1\leq y_{3}\leq
k+1}\right]\cdot\left[{l+1=|J\cap\\{y_{3},\dots,k\\}|}\right])$
$\displaystyle+\left[{v\neq
0}\right]\cdot\left[{v\neq-1}\right]\cdot\left[{y_{3}<1}\right]\cdot\left[{l+1=|J|}\right]$
$\displaystyle+\left[{v=0}\right]\cdot\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]$
$\displaystyle+\left[{v=0}\right]\cdot\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right])\mathbin{{\star}}\xi_{J})$

due to the lookup
$x_{3}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{2}+y_{2}\,\texttt{>}$ together
with the atom rule. We consider all cases separately.

  * •

First, let $v$ be $-1$

    * –

If moreover $y_{3}$ is between $1$ and $k+1$, then we can directly lower bound
the case that $y_{3}$ is $k+1$ by zero as $\xi_{J}$ does not have carry
information for this location. Because $v$ is $-1$, we know that $y_{3}$ is
not in $J$ due to $\xi_{J}$. Thus, we also have that
$|J\cap\\{y_{3}+1,\dots,k\\}|=|J\cap\\{y_{3},\dots,k\\}|$.

    * –

If $y_{3}$ is below $1$, the same reasoning holds, with the difference that we
lower bound the expectation for every value of $y_{3}$ below $0$ as zero and
consider only the case where $y_{3}$ is $0$.

  * •

In the case that $v$ is neither $0$ nor $-1$, we first observe that only $1$
and $2$ are valid values, because $\xi_{J}$ does not allow any other value for
$y_{3}$ between $0$ and $k$.

  * •

In the cases where $v$ is either $k+1$ or below $0$, we just lower bound the
formula by zero. However, for the latter cases we have
$|J\cap\\{y_{3}+1,\dots,k\\}|+1=|J\cap\\{y_{3},\dots,k\\}|$.

  * •

Lastly, in the case that $v$ is $0$, the expression already matches the target
lower bound, but again, we lower bound the formula by zero if $y_{3}$ has a
value below $0$.

Moreover, we have

$\displaystyle\leavevmode\nobreak\ \left[{y_{3}\geq
0}\right]\cdot(\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right])$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\ \left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k|\\}}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right]$

and thus established a loop invariant with respect to postexpectation
$\left[{l=|J|}\right]$.

Now we can combine all three results

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{P(k)\cdot\left[{0\leq k}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq k}\right]\cdot
P(k)+\left[{k<0}\right]\cdot\left[{0=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle l\mathrel{\textnormal{{:=}}}0\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq k}\right]\cdot\left[{l=0}\right]\cdot
P(k)+\left[{k<0}\right]\cdot\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\begin{aligned} &\leavevmode\nobreak\ 1\\\
\mathbin{{\star}}&\leavevmode\nobreak\ (\left[{0\leq k}\right]\cdot
P(k)+\left[{k<0}\right])\\\ \mathbin{{\star}}&\leavevmode\nobreak\
(\left[{0\leq
k}\right]\cdot\left[{l=|J\cap\\{k+1,\dots,k\\}|}\right]+\left[{k<0}\right]\cdot\left[{l=|J|}\right])\end{aligned}\leavevmode\nobreak\
\leavevmode\nobreak\ \stretchrel*{|}{\begin{aligned} &\leavevmode\nobreak\
1\\\ \mathbin{{\star}}&\leavevmode\nobreak\ (\left[{0\leq k}\right]\cdot
P(k)+\left[{k<0}\right])\\\ \mathbin{{\star}}&\leavevmode\nobreak\
(\left[{0\leq
k}\right]\cdot\left[{l=|J\cap\\{k+1,\dots,k\\}|}\right]+\left[{k<0}\right]\cdot\left[{l=|J|}\right])\end{aligned}}\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}\right.$ $\displaystyle
y_{1},y_{2},y_{3}\mathrel{\textnormal{{:=}}}k\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\begin{aligned} &\leavevmode\nobreak\ 1\\\
\mathbin{{\star}}&\leavevmode\nobreak\ (\left[{0\leq y_{2}\leq k}\right]\cdot
P(y_{2})+\left[{y_{2}<0}\right])\\\ \mathbin{{\star}}&\leavevmode\nobreak\
(\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right])\end{aligned}\leavevmode\nobreak\
\leavevmode\nobreak\ \stretchrel*{|}{\begin{aligned} &\leavevmode\nobreak\
1\\\ \mathbin{{\star}}&\leavevmode\nobreak\ (\left[{0\leq y_{2}\leq
k}\right]\cdot P(y_{2})+\left[{y_{2}<0}\right])\\\
\mathbin{{\star}}&\leavevmode\nobreak\ (\left[{0\leq y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{y_{3}+1,\dots,k\\}|}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right])\end{aligned}}\leavevmode\nobreak\
\leavevmode\nobreak\ \xi_{J}\right.$
$\displaystyle\left.C_{1}\;\middle\|\;\left.C_{2}\;\middle\|\;C_{3}\right.\right.$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\mathbin{{\star}}1\mathbin{{\star}}\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$

and we have for the whole program $C$ and a set of schedulers
$S\subseteq\mathbb{S}$:

$\displaystyle\leavevmode\nobreak\ (P(k)\cdot\left[{0\leq
k}\right])\leq\textsf{{wrlp}}\llbracket
C\rrbracket\left(\left[{l=|J|}\right]\mid\xi_{J}\right)$ implies
$\displaystyle\leavevmode\nobreak\ (P(k)\cdot\left[{0\leq
k}\right])\mathbin{{\star}}\xi_{J}\leq\textsf{{wrlp}}\llbracket
C\rrbracket\left(\left[{l=|J|}\right]\mathbin{{\star}}\xi_{J}\mid\left[{\textsf{{{emp}}}}\right]\right)$
(share) implies $\displaystyle\leavevmode\nobreak\ (P(k)\cdot\left[{0\leq
k}\right])\mathbin{{\star}}\xi_{J}\leq\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\left[{l=|J|}\right]\mathbin{{\star}}\xi_{J}\right)$ (wlp-
wrlp)

We can use this to prove the lower bound of probabilities for even more
elaborated postconditions if we have a set of schedulers
$S\subseteq\mathbb{S}$ such that $C$ is almost surely terminating with respect
to $S$. One of these is the probability that at least half of the messages are
sent successfully, i.e., the probability of the postexpectation
$\left[{k+1\geq l\geq\frac{k+1}{2}}\right]$ – or equivalently
$\sum_{\frac{k+1}{2}\leq j\leq k+1}\left[{l=j}\right]$. For this, we use the
resource invariant $\xi_{j}=\max_{J\subseteq\\{0,\dots,k\\},|J|=j}\xi_{J}$
where $\xi_{J}$ is defined as previous. Although we call $\xi_{j}$ a resource
invariant, we never prove that it is a resource invariant. We only prove that
$\xi_{J}$ is a resource invariant. We can now compute:

$\displaystyle\leavevmode\nobreak\ \textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\left[{l=|J|}\right]\mathbin{{\star}}\xi_{J}\right)\geq(P(k)\cdot\left[{0\leq
k}\right])\mathbin{{\star}}\xi_{J}$ implies $\displaystyle\leavevmode\nobreak\
\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\max_{J\subseteq\\{0,\dots,k\\},|J|=j}\left[{l=|J|}\right]\mathbin{{\star}}\xi_{J}\right)\geq\max_{J\subseteq\\{0,\dots,k\\},|J|=j}(P(k)\cdot\left[{0\leq
k}\right])\mathbin{{\star}}\xi_{J}$ (max) implies
$\displaystyle\leavevmode\nobreak\ \textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\left[{l=j}\right]\mathbin{{\star}}\xi_{j}\right)\geq(p^{j}\cdot(1-p)^{k-j+1}\cdot\left[{0\leq
k}\right])\mathbin{{\star}}\xi_{j}$ (Definition of $\xi_{j}$) implies
$\displaystyle\leavevmode\nobreak\ \textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\sum_{\frac{k+1}{2}\leq j\leq
k+1}\left[{l=j}\right]\mathbin{{\star}}\xi_{j}\right)\geq\sum_{\frac{k+1}{2}\leq
j\leq k+1}(p^{j}\cdot(1-p)^{k-j+1}\cdot\left[{0\leq
k}\right])\mathbin{{\star}}\xi_{j}$ (Superlinearity) implies
$\displaystyle\leavevmode\nobreak\ \textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\left[{k+1\geq
l\geq\frac{k+1}{2}}\right]\mathbin{{\star}}\xi_{j}\right)$
$\displaystyle\qquad\geq\left(\sum_{\frac{k+1}{2}\leq j\leq
k+1}p^{j}\cdot(1-p)^{k-j+1}\cdot\left[{0\leq
k}\right]\right)\mathbin{{\star}}\xi_{j}$ ($\xi_{j}$ is precise and
$\left[{k+1\geq l\geq\frac{k+1}{2}}\right]$ as above)

We could drop the resource invariant $\xi_{j}$ inside $\textsf{{wlp}}^{S}$ due
to monotonicity of $\textsf{{wlp}}^{S}$, for which we do not provide a proof.
However, this shows that we can use superlinearity to partition a big problem
in smaller problems and afterwards reason about these smaller problems with
the help of easier resource invariants, as it is standard in probability
theory.