We show that $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$ is
${Pol\/}(\mathcal{C})$-saturated. Since ${Pol\/}(\mathcal{C})$ is a
quotienting lattice, we already know from Lemma 5.20 that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$ contains
$\mathcal{P}_{\mathit{triv}}[\alpha,\rho]$ and is closed under downset and
multiplication. Thus, we may focus on proving that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$ satisfies
${Pol\/}(\mathcal{C})$-closure. Consider an idempotent
$(e,f)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$. We show that,

$(e,f\cdot\rho([e]_{\mathcal{C}})\cdot
f)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$

By definition of $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$, this means
proving that $f\cdot\rho([e]_{\mathcal{C}})\cdot
f\in\mathcal{I}_{{Pol\/}(\mathcal{C})}[\alpha^{-1}(e),\rho]$. We fix an
arbitrary optimal ${Pol\/}(\mathcal{C})$-cover $\mathbf{K}$ of
$\alpha^{-1}(e)$ and show that $f\cdot\rho([e]_{\mathcal{C}})\cdot
f\in\mathcal{I}[\rho](\mathbf{K})$. We rely on the generic stratification of
${Pol\/}(\mathcal{C})$ defined in Section 4 (which we may use since
$\mathcal{C}$ is a finite quotienting Boolean algebra). Recall that the strata
are denoted by $Pol_{k}(\mathcal{C})$ and the associated canonical preorders
by $\leqslant_{k}$. By definition $\mathbf{K}$ is a finite set of languages in
${Pol\/}(\mathcal{C})$. Therefore, there exists some stratum $k\in{\rm
Nature}$ such that all languages in $\mathbf{K}$ belong to
$Pol_{k}(\mathcal{C})$. Consequently, we have
$\mathcal{I}_{Pol_{k}(\mathcal{C})}[\alpha^{-1}(e),\rho]\subseteq\mathcal{I}[\rho](\mathbf{K})$
and it now suffices to show that $f\cdot\rho([e]_{\mathcal{C}})\cdot
f\in\mathcal{I}_{Pol_{k}(\mathcal{C})}[\alpha^{-1}(e),\rho]$. By Lemma 5.15,
we have to exhibit $w\in\alpha^{-1}(e)$ and $K\subseteq A^{*}$ such that
$w\leqslant_{k}K$ and $f\cdot\rho([e]_{\mathcal{C}})\cdot f\leq\rho(K)$. This
is what we do.

We first use our hypothesis that
$(e,f)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$ to define $w$ and
$K$. This implies that
$f\in\mathcal{I}_{{Pol\/}(\mathcal{C})}[\alpha^{-1}(e),\rho]$ and we get
$f\in\mathcal{I}_{Pol_{k}(\mathcal{C})}[\alpha^{-1}(e),\rho]$ by Fact 5.12.
Therefore, Lemma 5.15 yields $v\in\alpha^{-1}(e)$ and $H\subseteq A^{*}$ such
that $v\leqslant_{k}H$ and $f\leq\rho(H)$. Let $p\in{\rm Nature}$ be the
period of $\mathcal{C}$ (see Fact 4.10) and $\ell=p2^{k+1}$. We define,

$w=v^{\ell}$

Clearly, $w\in\alpha^{-1}(e)$ since $v\in\alpha^{-1}(e)$ and $e\in M$ is
idempotent. Finally, we let,

$K=H^{\ell}\cdot[e]_{\mathcal{C}}\cdot H^{\ell}$

By definition of $K$ and since $\rho$ is a multiplicative rating map,

$(\rho(H))^{\ell}\cdot\rho([e]_{\mathcal{C}})\cdot(\rho(H))^{\ell}=\rho(K)$

Moreover, since $f\leq\rho(H)$ by hypothesis and $f$ is idempotent, we obtain,

$f\cdot\rho([e]_{\mathcal{C}})\cdot f\leq\rho(K)$

It remains to show that $w\leqslant_{k}K$. The proof is based on Lemma 4.12.
Consider $u\in K$. We show that $w\leqslant_{k}u$. This will imply that
$w\leqslant_{k}K$. By definition, we have
$K=H^{\ell}\cdot[e]_{\mathcal{C}}\cdot H^{\ell}$ and by hypothesis, we have
$v\leqslant_{k}H$. Thus, since $u\in K$ and $\leqslant_{k}$ is compatible with
concatenation (see Lemma 2.9), we obtain that there exists some
$x\in[e]_{\mathcal{C}}$ such that,

$v^{\ell}\cdot x\cdot v^{\ell}\leqslant_{k}u$

Therefore, it now suffices to show that $w\leqslant_{k}v^{\ell}\cdot x\cdot
v^{\ell}$. It will then be immediate from transitivity that $w\leqslant_{k}u$
as desired. Recall that $p$ denotes the period of $\mathcal{C}$ and
$\ell=p2^{k+1}$. Since $v\in\alpha^{-1}(e)$ and $e$ is an idempotent of $M$,
we have $v^{p}\in\alpha^{-1}(e)\subseteq[e]_{\mathcal{C}}$. Thus, $x$ and
$v^{p}$ belong to the same $\sim_{\mathcal{C}}$-class: $[e]_{\mathcal{C}}$. We
get $v^{p}\sim_{\mathcal{C}}x$ and Lemma 4.12 yields that

$v^{\ell}\leqslant_{k}v^{\ell}\cdot x\cdot v^{\ell}$

Since $w=v^{\ell}$ by definition this is exactly the desired property which
concludes the proof.

###  6.4. Completeness

We turn to completeness. Recall that we have a $\mathcal{C}$-compatible
morphism $\alpha:A^{*}\to M$ and a multiplicative rating map
$\rho:2^{A^{*}}\to R$. Consider $S\subseteq M\times R$ which is
${Pol\/}(\mathcal{C})$-saturated. Our objective is to prove that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]\subseteq S$.

We present a generic construction which builds ${Pol\/}(\mathcal{C})$-covers
$\mathbf{K}_{s}$ of $\alpha^{-1}(s)$ for all $s\in M$ such that for any
$K\in\mathbf{K}_{s}$, we have $(s,\rho(K))\in S$. By definition of
$\mathcal{I}[\rho](\mathbf{K}_{s})$ and since $S$ is closed under downset, (it
is ${Pol\/}(\mathcal{C})$-saturated), this will imply,

$\mathcal{I}[\rho](\mathbf{K}_{s})\subseteq\\{r\mid(s,r)\in S\\}$

Thus, since
$\mathcal{I}_{{Pol\/}(\mathcal{C})}[\alpha^{-1}(s),\rho]\subseteq\mathcal{I}[\rho](\mathbf{K}_{s})$
by definition of ${Pol\/}(\mathcal{C})$-optimal $\rho$-imprints, we shall
obtain,

$\mathcal{I}_{{Pol\/}(\mathcal{C})}[\alpha^{-1}(s),\rho]\subseteq\\{r\mid(s,r)\in
S\\}$

Finally, by definition of $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$,
we shall obtain the desired inclusion:
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]\subseteq S$ (recall that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]=\\{(s,r)\mid
r\in\mathcal{I}_{{Pol\/}(\mathcal{C})}[\alpha^{-1}(s),\rho]\\}$).

######  Remark 6.7.

This construction yields a generic method for building optimal
${Pol\/}(\mathcal{C})$-covers of the sets $\alpha^{-1}(s)$ for $s\in M$.
Indeed, we may apply it in the special case when
$S=\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$ since we already showed
above that $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\alpha,\rho]$ is
${Pol\/}(\mathcal{C})$-saturated. In this case, we get
${Pol\/}(\mathcal{C})$-covers $\mathbf{K}_{s}$ of $\alpha^{-1}(s)$ for all
$s\in M$ such that
$\mathcal{I}[\rho](\mathbf{K}_{s})=\mathcal{I}_{{Pol\/}(\mathcal{C})}[\alpha^{-1}(s),\rho]$.

The construction is based on the factorization forest theorem of Simon which
we presented in Section 4. Recall that for any $s\in M$ and $h,m\in{\rm
Nature}$, we write $F^{\alpha}(s,h,m)$ for the language of all words in
$\alpha^{-1}(s)$ which admit an $\alpha$-factorization forest of height at
most $h$ and idempotent height at most $m$. We use the following proposition.

######  Proposition 6.8.

Let $s\in M$ and $h,m\in{\rm Nature}$. There exists a
${Pol\/}(\mathcal{C})$-cover $\mathbf{K}$ of $F^{\alpha}(s,h,m)$ such that for
any $K\in\mathbf{K}$, we have $(s,\rho(K))\in S$.

Before proving the proposition, we use it to finish the proof of Theorem 6.5.
Consider $s\in M$. Our objective is to build a ${Pol\/}(\mathcal{C})$-cover
$\mathbf{K}_{s}$ of $\alpha^{-1}(s)$ such that,

$(s,\rho(K))\in S\quad\text{for all $K\in\mathbf{K}_{s}$}$

Let $h=m=3|M|-1$. We obtain from the factorization forest theorem (i.e.
Theorem 4.5) that $\alpha^{-1}(s)=F^{\alpha}(s,h,m)$. Thus, Proposition 6.8
yields the desired ${Pol\/}(\mathcal{C})$-cover $\mathbf{K}_{s}$ of
$\alpha^{-1}(s)$ such that for any $K\in\mathbf{K}_{s}$, we have
$(s,\rho(K))\in S$.

It remains to prove Proposition 6.8. Let $h,m\in{\rm Nature}$ and $s\in M$.
Our objective is to build a ${Pol\/}(\mathcal{C})$-cover $\mathbf{K}$ of
$F^{\alpha}(s,h,m)$ which satisfies the following property:

$\text{For all $K\in\mathbf{K}$,}\quad(s,\rho(K))\in S$ (1)

The construction is an induction on $h$. We start by considering the base
case: $h=0$.

######  Remark 6.9.

The proof is actually independent from the idempotent height $m$: this
parameter is only useful for the $PBPol(\mathcal{C})$ proof which we present
in Section 8. We are forced to make it apparent because we intend to use Lemma
6.2 whose statement is designed to accommodate both ${Pol\/}(\mathcal{C})$ and
$PBPol(\mathcal{C})$.

####  6.4.1. Base case: Leaves

Assume that $h=0$. It follows that all words in $F^{\alpha}(s,0,m)$ are either
empty or made of a single letter $a\in A$. We distinguish two cases depending
on whether $s=1_{M}$ or not. If $s\neq 1_{M}$, we define,

$\mathbf{K}=\\{[\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}\mid
a\in A\text{ and }\alpha(a)=s\\}$

Otherwise, $s=1_{M}$ and we define,

$\mathbf{K}=\\{[\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}\mid
a\in A\text{ and }\alpha(a)=s\\}\cup\\{[\varepsilon]_{\mathcal{C}}\\}$

Clearly, all languages in $\mathbf{K}$ belong to ${Pol\/}(\mathcal{C})$ (they
are marked concatenations of the language
$[\varepsilon]_{\mathcal{C}}\in\mathcal{C}$ with itself). Moreover, it is also
immediate that $\mathbf{K}$ is a cover of $F^{\alpha}(s,0,m)$. Indeed, a word
$w\in F^{\alpha}(s,0,m)$ is either empty or a single letter and $\alpha(w)=s$.
Thus, if $w=\varepsilon$, we have $w\in[\varepsilon]_{\mathcal{C}}$ and if
$w=a\in A$, we have
$w\in[\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}$.

It remains to show that $\mathbf{K}$ satisfies (1). Given $K\in\mathbf{K}$, we
have to show that $(s,\rho(K))\in S$. By definition of $\mathbf{K}$ this is an
immediate consequence of the following lemma.

######  Lemma 6.10.

We have $(1_{M},\rho([\varepsilon]_{\mathcal{C}}))\in S$. Moreover, given any
letter $a\in A$, we have
$(\alpha(a),\rho([\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}))\in
S$.

###### Proof.

We begin with the first property:
$(1_{M},\rho([\varepsilon]_{\mathcal{C}}))\in S$. By definition, we know that
$(1_{M},\rho(\varepsilon))=(\alpha(\varepsilon),\rho(\varepsilon))\in\mathcal{P}_{\mathit{triv}}[\alpha,\rho]$.
Therefore, since $S$ is ${Pol\/}(\mathcal{C})$-saturated, we have
$(1_{M},\rho(\varepsilon))\in S$. Moreover, $(1_{M},\rho(\varepsilon))$ is
clearly a pair of idempotents. Therefore, since $S$ is
${Pol\/}(\mathcal{C})$-saturated, we get from ${Pol\/}(\mathcal{C})$-closure
that,

$(1_{M},\rho([1_{M}]_{\mathcal{C}}))=(1_{M},\rho(\varepsilon)\cdot\rho([1_{M}]_{\mathcal{C}})\cdot\rho(\varepsilon))\in
S$

Since $\varepsilon\in\alpha^{-1}(1_{M})\subseteq[1_{M}]_{\mathcal{C}}$, we
have $[\varepsilon]_{\mathcal{C}}=[1_{M}]_{\mathcal{C}}$ and we get
$(1_{M},\rho([\varepsilon]_{\mathcal{C}}))\in S$ as desired.

It remains to prove that given $a\in A$, we have
$(\alpha(a),\rho([\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}))\in
S$. By definition, we have
$(\alpha(a),\rho(a))\in\mathcal{P}_{\mathit{triv}}[\alpha,\rho]$. Hence,
$(\alpha(a),\rho(a))\in S$ since $S$ is ${Pol\/}(\mathcal{C})$-saturated.
Since $(1_{M},\rho([\varepsilon]_{\mathcal{C}}))\in S$, it now follows from
closure under multiplication that,

$(1_{M}\cdot\alpha(a)\cdot
1_{M},\rho([\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}))\in S$

We get as desired that
$(\alpha(a),\rho([\varepsilon]_{\mathcal{C}}a[\varepsilon]_{\mathcal{C}}))\in
S$. ∎

####  6.4.2. Inductive case

We now assume that $h\geq 1$. Recall that our objective is to build a
${Pol\/}(\mathcal{C})$-cover $\mathbf{K}$ of $F^{\alpha}(s,h,m)$ which
satisfies (1). We decompose $F^{\alpha}(s,h,m)$ as the union of three
languages that we cover independently. Recall that $F^{\alpha}_{B}(s,h,m)$
(resp. $F^{\alpha}_{I}(s,h,m)$) denotes the language of all words in
$\alpha^{-1}(s)$ admitting an $\alpha$-factorization forest of height of at
most $h$, of idempotent height at most $m$ and whose root is a _binary node_
(resp. _idempotent node_). The construction is based on the two following
lemmas.

######  Lemma 6.11.

There exists a ${Pol\/}(\mathcal{C})$-cover $\mathbf{K}_{B}$ of
$F^{\alpha}_{B}(s,h,m)$ such that for all $K\in\mathbf{K}_{B}$, we have
$(s,\rho(K))\in S$.

######  Lemma 6.12.

There exists a ${Pol\/}(\mathcal{C})$-cover $\mathbf{K}_{I}$ of
$F^{\alpha}_{I}(s,h,m)$ such that for all $K\in\mathbf{K}_{I}$, we have
$(s,\rho(K))\in S$.

Before we show these two results, let us use them to finish the inductive
case. Let $\mathbf{K}_{B}$ and $\mathbf{K}_{I}$ be as defined in the two above
lemmas. Fact 4.4 yields the following:

$F^{\alpha}(s,h,m)=F^{\alpha}_{B}(s,h,m)\cup F^{\alpha}_{I}(s,h,m)\cup
F^{\alpha}(s,0,0)$

Since $h\geq 1$, we obtain from induction on $h$ that we have a
${Pol\/}(\mathcal{C})$-cover $\mathbf{K}^{\prime}$ of $F^{\alpha}(s,0,0)$ such
that for all $K\in\mathbf{K}$, we have $(s,\rho(K))\in S$. Thus, it suffices
to define
$\mathbf{K}=\mathbf{K}_{B}\cup\mathbf{K}_{I}\cup\mathbf{K}^{\prime}$. By
definition, we know that $\mathbf{K}$ is a ${Pol\/}(\mathcal{C})$-cover of
$F^{\alpha}(s,h,m)$ which satisfies (1) as desired. It remains to prove the
two lemmas.

Proof of Lemma 6.11. Using induction we obtain that for all $t\in M$, there
exists a ${Pol\/}(\mathcal{C})$-cover $\mathbf{U}_{t}$ of
$F^{\alpha}(t,h-1,m)$ such that for any $U\in\mathbf{U}_{t}$, we have
$(t,\rho(U))\in S$. We use these new ${Pol\/}(\mathcal{C})$-covers
$\mathbf{U}_{t}$ to build the desired $\mathbf{K}_{B}$. We define,

$\mathbf{K}_{B}=\\{K_{1}K_{2}\mid\text{there exist $t_{1},t_{2}\in M$ such
that $s=t_{1}t_{2}$, $K_{1}\in\mathbf{U}_{t_{1}}$ and
$K_{2}\in\mathbf{U}_{t_{2}}$}\\}$

We need to verify that $\mathbf{K}_{B}$ satisfies the desired properties. We
start by proving that it is a ${Pol\/}(\mathcal{C})$-cover of
$F_{B}^{\alpha}(s,h,m)$. Clearly, all languages in $\mathbf{K}_{B}$ belong to
${Pol\/}(\mathcal{C})$ (this follows from Theorem 3.2 since they are all
concatenations of two languages in ${Pol\/}(\mathcal{C})$). Hence, it suffices
to verify that $\mathbf{K}_{B}$ is a cover of $F_{B}^{\alpha}(s,h,m)$. Let
$w\in F_{B}^{\alpha}(s,h,m)$, we exhibit $K\in\mathbf{K}_{B}$ such that $w\in
K$. By definition, $w$ is the root label of some $\alpha$-factorization forest
of height at most $h$, of idempotent height at most $m$ and whose root is a
binary node. This exactly says that $w$ admits a decomposition $w=w_{1}w_{2}$
with $w_{1}\in F^{\alpha}(\alpha(w_{1}),h-1,m)$, $w_{2}\in
F^{\alpha}(\alpha(w_{2}),h-1,m)$. Since $\mathbf{U}_{\alpha(w_{1})}$ and
$\mathbf{U}_{\alpha(w_{2})}$ are covers of $F^{\alpha}(\alpha(w_{1}),h-1,m)$
and $F^{\alpha}(\alpha(w_{2}),h-1,m)$ respectively, there exist
$K_{1}\in\mathbf{U}_{\alpha(w_{1})}$ and $K_{2}\in\mathbf{U}_{\alpha(w_{2})}$
such that $w_{1}\in K_{1}$ and $w_{2}\in K_{2}$. Thus, $w=w_{1}w_{2}\in
K_{1}K_{2}$ which is an element of $\mathbf{K}_{B}$ by definition since
$\alpha(w_{1})\alpha(w_{2})=\alpha(w)=s$.

It remains to verify that for any $K\in\mathbf{K}_{B}$, we have
$(s,\rho(K))\in S$. By construction, $K=K_{1}K_{2}$ where
$K_{1}\in\mathbf{U}_{t_{1}}$ and $K_{2}\in\mathbf{U}_{t_{2}}$ for
$t_{1},t_{2}\in M$ such that $s=t_{1}t_{2}$. Moreover, we know that
$(t_{1},\rho(K_{1}))\in S$ and $(t_{2},\rho(K_{2}))\in S$ by definition of
$\mathbf{U}_{t_{1}}$ and $\mathbf{U}_{t_{2}}$. Therefore, since $S$ is
${Pol\/}(\mathcal{C})$-saturated, we obtain from closure under multiplication
that $(s,\rho(K))=(t_{1}t_{2},\rho(K_{1}K_{2}))\in S$.

Proof of Lemma 6.12. Recall that our objective here is to construct a
${Pol\/}(\mathcal{C})$-cover $\mathbf{K}_{I}$ of $F^{\alpha}_{I}(s,h,m)$ such
that for all $K\in\mathbf{K}_{I}$, we have $(s,\rho(K))\in S$. Observe that we
may assume without loss of generality that $s$ is an idempotent of $M$.
Indeed, otherwise we have $F^{\alpha}_{I}(s,h,m)=\emptyset$ and we may simply
choose $\mathbf{K}_{I}=\emptyset$. We shall write $s=e\in M$ to underline the
fact that $s$ is idempotent: we have to cover $F^{\alpha}_{I}(e,h,m)$. This is
where we use Lemma 6.2. Applying it requires a cover $\mathbf{U}$ of
$F^{\alpha}(e,h-1,m-1)$ and a language $V$ which contains $\alpha^{-1}(e)$.
Let us first define these objects.

We build $\mathbf{U}$ by induction. More precisely, it is immediate from
induction on the height $h$ that there exists a ${Pol\/}(\mathcal{C})$-cover
$\mathbf{U}$ of $F^{\alpha}(e,h-1,m-1)$ such that for any $U\in\mathbf{U}$, we
have $(e,\rho(U))\in S$. Furthermore, use $[e]_{\mathcal{C}}$ as the language
$V$ (note that $[e]_{\mathcal{C}}$ contains $\alpha^{-1}(e)$ by definition of
$\mathcal{C}$-compatible morphisms).

We now have everything we need for applying Lemma 6.2. We obtain a cover
$\mathbf{K}_{I}$ of $F^{\alpha}_{I}(e,h,m)$ such that any $K\in\mathbf{K}_{I}$
is a concatenation $K=K_{1}\cdots K_{n}$ where each $K_{i}$ is of one of the
two following kinds:

  1. (1)

$K_{i}$ is a language in $\mathbf{U}$, or,

  2. (2)

$K_{i}=U_{1}\cdots U_{\ell}[e]_{\mathcal{C}}U^{\prime}_{1}\cdots
U^{\prime}_{\ell^{\prime}}$ where
$U_{1},\dots,U_{\ell},U^{\prime}_{1},\dots,U^{\prime}_{\ell^{\prime}}\in\mathbf{U}$
and there exists an _idempotent_ $f\in R$ such that $\rho(U_{1}\cdots
U_{\ell})=\rho(U^{\prime}_{1}\cdots U^{\prime}_{\ell^{\prime}})=f$.

Clearly, any $K\in\mathbf{K}_{I}$ belongs to ${Pol\/}(\mathcal{C})$: this
follows from Theorem 3.2 since it is a concatenation of languages in
${Pol\/}(\mathcal{C})$ by definition
($[e]_{\mathcal{C}}\in\mathcal{C}\subseteq{Pol\/}(\mathcal{C})$ by Lemma 2.8
since it is $\sim_{\mathcal{C}}$-class). Therefore, $\mathbf{K}_{I}$ is a
${Pol\/}(\mathcal{C})$-cover of $F^{\alpha}_{I}(e,h,m)$. It remains to prove
that for any $K\in\mathbf{K}_{I}$, we have $(e,\rho(K))\in S$. We need the
following fact which is proved using ${Pol\/}(\mathcal{C})$-closure.

######  Fact 6.13.

Consider an idempotent $f\in R$ such that $f=\rho(U_{1}\cdots U_{\ell})$ with
$U_{1},\dots,U_{\ell}\in\mathbf{U}$. Then, we have
$(e,f\cdot\rho([e]_{\mathcal{C}})\cdot f)\in S$.

###### Proof.

By definition of $\mathbf{U}$, we know that $(e,\rho(U_{i}))\in S$ for all
$i\leq\ell$. Therefore, since $S$ is ${Pol\/}(\mathcal{C})$-saturated and $e$
is idempotent, closure under multiplication yields that,

$(e,f)=(e^{\ell},\rho(U_{1}\cdots U_{\ell}))\in S$

Since $(e,f)$ is an idempotent, we get from ${Pol\/}(\mathcal{C})$-closure
that $(e,f\cdot\rho([e]_{\mathcal{C}})\cdot f)\in S$. ∎

We may now prove that $(e,\rho(K))\in S$ for any $K\in\mathbf{K}_{I}$.
Consider $K\in\mathbf{K}_{I}$. By definition $K=K_{1}\cdots K_{n}$ where all
languages $K_{i}$ are as described in the two items above. Clearly,
$(e,\rho(K_{i}))\in S$ for any $i\leq n$. If $K_{i}$ is as described in the
first item ($K_{i}\in\mathbf{U}$), this is by definition of $\mathbf{U}$.
Otherwise, $K_{i}$ is as described in the second item and this is by Fact
6.13. Therefore, since $S$ is ${Pol\/}(\mathcal{C})$-saturated and $e$ is
idempotent, we obtain from closure under multiplication that,

$(e,\rho(K))=(e^{n},\rho(K_{1})\cdots\rho(K_{n}))\in S$

This concludes the argument for Lemma 6.12.

##  7\. Covering for $PBPol(\mathcal{C})$

We now turn to our main result: $PBPol(\mathcal{C})$-covering is decidable for
any finite quotienting Boolean algebra $\mathcal{C}$. Again, our approach is
based on optimal imprints: we present an effective characterization of
$PBPol(\mathcal{C})$-optimal pointed imprints. For the sake of avoiding
clutter, we shall assume that $\mathcal{C}$ is fixed for the section.

This characterization is more involved than the one we already obtained for
${Pol\/}(\mathcal{C})$. First, it applies to a more restricted class of
multiplicative rating maps. Specifically, we present a characterization of
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ which holds when
$\alpha:A^{*}\to M$ is a $\mathcal{C}$-compatible morphism and $\rho$ is a
_nice $\mathcal{C}$-compatible_ multiplicative rating map. In other words, we
now need $\rho$ to be nice and $\mathcal{C}$-compatible (which was not the
case for ${Pol\/}(\mathcal{C})$).

######  Remark 7.1.

Of course, having a characterization restricted to this special case is enough
to obtain the desired $PBPol(\mathcal{C})$-covering algorithm by Proposition
5.18. However, the fact that we now require $\rho$ to be nice (which was not
the case for ${Pol\/}(\mathcal{C})$) is significant. This explains why the
arguments of this paper do not extend to higher levels in concatenation
hierarchies. The proof of our characterization for $PBPol(\mathcal{C})$ relies
heavily on the fact that we have a characterization for ${Pol\/}(\mathcal{C})$
which holds for all multiplicative rating maps.

A second point is that our characterization of $PBPol(\mathcal{C})$-optimal
pointed imprints actually involves two distinct objects:

  * •

As desired, it describes $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$, the
$PBPol(\mathcal{C})$-optimal $\alpha$-pointed $\rho$-imprint.

  * •

It also describes a second object:
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$, which is the
${Pol\/}(\mathcal{C})$-optimal $\beta$-pointed $\tau$-imprint where $\beta$ is
the canonical morphism associated to $\rho$ (i.e. its restriction to $A^{*}$),
and $\tau$ is an auxiliary multiplicative rating map built from $\alpha$ and
$\rho$.

The key idea here is that our descriptions of
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ and
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ are mutually dependent.
Reformulated from an algorithmic point of view, this means that we get a least
fixpoint procedure which computes
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ and
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ simultaneously (although
$\tau$ is not nice and can only be used implicitly in the algorithm).

######  Remark 7.2.

The presence of this second object
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ explains why we shall need to
reuse our characterization of ${Pol\/}(\mathcal{C})$-optimal pointed imprints
(i.e. Theorem 6.5). In particular, the multiplicative rating map $\tau$ will
not be nice. Hence, it will be important that Theorem 6.5 holds for all
multiplicative rating maps.

The section is organized as follows. First, we explain how the auxiliary
multiplicative rating map $\tau$ is defined from $\alpha$ and $\rho$. Then, we
present our characterization of $PBPol(\mathcal{C})$-optimal pointed imprints.
Finally, we concentrate on proving our characterization (note that we postpone
the difficult direction of this proof to the next section).

###  7.1. Auxiliary multiplicative rating map

Let $\mathcal{D}$ be a quotienting lattice which is _closed under
concatenation_. Consider a multiplicative rating map $\rho:2^{A^{*}}\to R$ and
a morphism $\alpha:A^{*}\to M$. We build a new multiplicative rating map
$\tau^{\mathcal{D}}_{\alpha,\rho}:2^{A^{*}}\to 2^{M\times R}$ (which we shall
often simply write “$\tau$” when $\alpha$, $\rho$ and $\mathcal{D}$ are clear
from the context). We shall later use this definition in the special case when
$\mathcal{D}=PBPol(\mathcal{C})$. This makes sense since we showed that
$PBPol(\mathcal{C})$ is a quotienting lattice closed under concatenation in
Theorem 3.2. Let us first explain why the set $2^{M\times R}$ is a hemiring.

Since $2^{M\times R}$ is a set of subsets, it is an idempotent commutative
monoid for union. Thus, we simply use union as our addition (the neutral
element is $\emptyset$ and the order is inclusion). It remains to define our
multiplication. Given $T_{1},T_{2}\in 2^{M\times R}$, we define,

$T_{1}\cdot T_{2}=\\{(s_{1}s_{2},r)\mid\text{there exists $(s_{1},r_{1})\in
T_{1}$ and $(s_{2},r_{2})\in T_{2}$ such that $r\leq r_{1}r_{2}$}\\}$

One may verify that this is indeed a semigroup multiplication which
distributes over the addition (i.e. union) and that $\emptyset$ (the neutral
element for union) is a zero. It follows that $2^{M\times R}$ is an idempotent
hemiring.

######  Remark 7.3.

Our multiplication is not the most immediate one: $T_{1}\cdot T_{2}$ is not
the set of all multiplications between elements of $T_{1}$ and $T_{2}$. It
contains more elements: we make sure that $T_{1}\cdot T_{2}$ is closed under
downset (if $(s,r)\in T_{1}\cdot T_{2}$ and $r^{\prime}\leq r$, then
$(s,r^{\prime})\in T_{1}\cdot T_{2}$). We shall need this for proving that
$\tau^{\mathcal{D}}_{\alpha,\rho}:2^{A^{*}}\to 2^{M\times R}$ is a
multiplicative rating map.

Observe that for this multiplication, $2^{M\times R}$ is a hemiring but not a
semiring. There exists no neutral element for multiplication since a set $T\in
2^{M\times R}$ which is not closed under downset cannot be equal to any
multiplication.

We are now ready to define our new multiplicative rating map
$\tau^{\mathcal{D}}_{\alpha,\rho}:2^{A^{*}}\to 2^{M\times R}$. We use the
following definition:

$\begin{array}[]{llll}\tau^{\mathcal{D}}_{\alpha,\rho}:&2^{A^{*}}&\to&2^{M\times
R}\\\ &K&\mapsto&\\{(s,r)\in M\times
R\mid\text{$r\in\mathcal{I}_{\mathcal{D}}[K\cap\alpha^{-1}(s),\rho]$}\\}\end{array}$

Let us verify that $\tau^{\mathcal{D}}_{\alpha,\rho}$ is indeed a
multiplicative rating map. Note that it is important here that $\mathcal{D}$
is a quotienting lattice closed under concatenation.

######  Lemma 7.4.

The map $\tau^{\mathcal{D}}_{\alpha,\rho}$ is a multiplicative rating map.

###### Proof.

We have to show that $\tau^{\mathcal{D}}_{\alpha,\rho}$ is a hemiring
morphism. Let us first consider addition (which is union for both $2^{A^{*}}$
and $2^{M\times R}$). Clearly
$\tau^{\mathcal{D}}_{\alpha,\rho}(\emptyset)=\emptyset$. Indeed,

$\tau^{\mathcal{D}}_{\alpha,\rho}(\emptyset)=\\{(s,r)\in M\times R\mid
r\in\mathcal{I}_{\mathcal{D}}[\emptyset,\rho]\\}=\\{(s,r)\in M\times R\mid
r\in\emptyset\\}=\emptyset$

We now show that for any $K_{1},K_{2}\subseteq A^{*}$, we have
$\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}\cup
K_{2})=\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cup\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$.
We start with the right to left inclusion. Let
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cup\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$
and by symmetry, assume that
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})$. It follows that
$r\in\mathcal{I}_{\mathcal{D}}[K_{1}\cap\alpha^{-1}(s),\rho]$. Since
$K_{1}\cap\alpha^{-1}(s)\subseteq(K_{1}\cup K_{2})\cap\alpha^{-1}(s)$, it then
follows from Fact 5.13 that $r\in\mathcal{I}_{\mathcal{D}}[(K_{1}\cup
K_{2})\cap\alpha^{-1}(s),\rho]$ which exactly says that
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}\cup K_{2})$. It remains to
treat the left to right inclusion. Let
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}\cup K_{2})$. By definition,
$r\in\mathcal{I}_{\mathcal{D}}[(K_{1}\cup K_{2})\cap\alpha^{-1}(s),\rho]$.
Consider optimal $\mathcal{D}$-covers (for $\rho$)
$\mathbf{U}_{1},\mathbf{U}_{2}$ of $(K_{1}\cap\alpha^{-1}(s))$ and
$(K_{2}\cap\alpha^{-1}(s))$ respectively. By definition,
$\mathbf{U}_{1}\cup\mathbf{U}_{2}$ is a $\mathcal{D}$-cover of $(K_{1}\cup
K_{2})\cap\alpha^{-1}(s)$. Thus, we have $\mathcal{I}_{\mathcal{D}}[(K_{1}\cup
K_{2})\cap\alpha^{-1}(s),\rho]\subseteq\mathcal{I}[\rho](\mathbf{U}_{1}\cup\mathbf{U}_{2})$
and we obtain $r\in\mathcal{I}[\rho](\mathbf{U}_{1}\cup\mathbf{U}_{2})$.
Therefore, there exists $U\in\mathbf{U}_{1}\cup\mathbf{U}_{2}$ such that
$r\leq\rho(U)$. By symmetry assume that $U\in\mathbf{U}_{1}$, we show that
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})$ (when $U\in\mathbf{U}_{2}$,
one may show that $(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$). By
definition, we have $r\in\mathcal{I}[\rho](\mathbf{U}_{1})$ and since
$\mathbf{U}_{1}$ is an optimal $\mathcal{D}$-cover of
$K_{1}\cap\alpha^{-1}(s)$, we know that
$\mathcal{I}[\rho](\mathbf{U}_{1})=\mathcal{I}_{\mathcal{D}}[K_{1}\cap\alpha^{-1}(s),\rho]$.
Thus, $r\in\mathcal{I}_{\mathcal{D}}[K_{1}\cap\alpha^{-1}(s),\rho]$ which
exactly means that $(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})$.

This concludes the proof for addition. We turn to multiplication. We show that
$\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}K_{2})=\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cdot\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$.
We start with the inclusion
$\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cdot\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})\subseteq\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}K_{2})$.
Let
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cdot\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$.
Thus, we have $(s_{1},r_{1})\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})$ and
$(s_{2},r_{2})\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$ such that
$s=s_{1}s_{2}$ and $r\leq r_{1}r_{2}$. By definition of
$\tau^{\mathcal{D}}_{\alpha,\rho}$, we have
$r_{1}\in\mathcal{I}_{\mathcal{D}}[K_{1}\cap\alpha^{-1}(s_{1}),\rho]$ and
$r_{2}\in\mathcal{I}_{\mathcal{D}}[K_{2}\cap\alpha^{-1}(s_{2}),\rho]$. Since
$\mathcal{D}$ is a quotienting lattice, the following result is immediate from
Lemma 5.14,

$r_{1}r_{2}\in\mathcal{I}_{\mathcal{D}}[(K_{1}\cap\alpha^{-1}(s_{1}))\cdot(K_{2}\cap\alpha^{-1}(s_{2})),\rho]$

Observe that
$(K_{1}\cap\alpha^{-1}(s_{1}))\cdot(K_{2}\cap\alpha^{-1}(s_{2}))\subseteq
K_{1}K_{2}\cap\alpha^{-1}(s_{1})\alpha^{-1}(s_{2})$. Moreover, since $\alpha$
is a morphism, we have
$\alpha^{-1}(s_{1})\alpha^{-1}(s_{2})\subseteq\alpha^{-1}(s_{1}s_{2})$.
Altogether, this means that we have
$(K_{1}\cap\alpha^{-1}(s_{1}))\cdot(K_{2}\cap\alpha^{-1}(s_{2}))\subseteq
K_{1}K_{2}\cap\alpha^{-1}(s_{1}s_{2})$. Therefore, we then obtain from Fact
5.13 that
$r_{1}r_{2}\in\mathcal{I}_{\mathcal{D}}[K_{1}K_{2}\cap\alpha^{-1}(s_{1}s_{2}),\rho]$.
Thus, we also have
$r\in\mathcal{I}_{\mathcal{D}}[K_{1}K_{2}\cap\alpha^{-1}(s_{1}s_{2}),\rho]$ by
definition of imprints since $r\leq r_{1}r_{2}$. It follows that
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}K_{2})$ by definition of
$\tau^{\mathcal{D}}_{\alpha,\rho}$.

We finish with the converse inclusion. Let
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1}K_{2})$. By definition, we have
$r\in\mathcal{I}_{\mathcal{D}}[K_{1}K_{2}\cap\alpha^{-1}(s),\rho]$. For any
$t\in M$ and $i\in\\{1,2\\}$, we define $\mathbf{U}_{i,t}$ as an optimal
$\mathcal{D}$-cover of $K_{i}\cap\alpha^{-1}(t)$. Consider the following
finite set of languages $\mathbf{U}$,

$\mathbf{U}=\\{U_{1}U_{2}\mid\text{there exists $s_{1},s_{2}\in M$ s.t.
$s_{1}s_{2}=s$, $U_{1}\in\mathbf{U}_{1,s_{1}}$ and
$U_{2}\in\mathbf{U}_{2,s_{2}}$}\\}$

Observe that $\mathbf{U}$ is a $\mathcal{D}$-cover of
$K_{1}K_{2}\cap\alpha^{-1}(s)$. Clearly all languages in $\mathbf{U}$ belong
to $\mathcal{D}$ since $\mathcal{D}$ is closed under concatenation by
hypothesis. Let us show that $\mathbf{U}$ is a cover of
$K_{1}K_{2}\cap\alpha^{-1}(s)$. Consider $w\in K_{1}K_{2}\cap\alpha^{-1}(s)$,
we exhibit $U\in\mathbf{U}$ such that $w\in U$. Since $w\in K_{1}K_{2}$, we
have $w=w_{1}w_{2}$ with $w_{1}\in K_{1}$ and $w_{2}\in K_{2}$. Let
$s_{1}=\alpha(w_{1})$ and $s_{2}=\alpha(w_{2})$. Altogether, this means that
$w_{1}\in K_{1}\cap\alpha^{-1}(s_{1})$ and $w_{2}\in
K_{2}\cap\alpha^{-1}(s_{2})$. Therefore, we have
$U_{1}\in\mathbf{U}_{1,s_{1}}$ and $U_{2}\in\mathbf{U}_{2,s_{2}}$ such that
$w_{1}\in U_{1}$ and $w_{2}\in U_{2}$. This yields $w\in U_{1}U_{2}$. Finally,
$s_{1}s_{2}=\alpha(w)=s$ which yields that $U_{1}U_{2}\in\mathbf{U}$ by
definition.

We may now finish the argument and show that
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cdot\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$.
Recall that
$r\in\mathcal{I}_{\mathcal{D}}[K_{1}K_{2}\cap\alpha^{-1}(s),\rho]$. Thus,
since $\mathbf{U}$ is a $\mathcal{D}$-cover of $K_{1}K_{2}\cap\alpha^{-1}(s)$,
we have $r\in\mathcal{I}[\rho](\mathbf{U})$. It follows that there exists
$U\in\mathbf{U}$ such that $r\leq\rho(U)$. By definition of $\mathbf{U}$,
$U=U_{1}U_{2}$ with $U_{1}\in\mathbf{U}_{1,s_{1}}$ and
$U_{2}\in\mathbf{U}_{2,s_{2}}$ where $s_{1},s_{2}\in M$ satisfy
$s_{1}s_{2}=s$. Let $r_{1}=\rho(U_{1})$ and $r_{2}=\rho(U_{2})$. Since
$\mathbf{U}_{1,s_{1}}$ and $\mathbf{U}_{2,s_{2}}$ are optimal
$\mathcal{D}$-covers of $K_{1}\cap\alpha^{-1}(s_{1})$ and
$K_{2}\cap\alpha^{-1}(s_{2})$ respectively, we have
$r_{1}\in\mathcal{I}_{\mathcal{D}}[K_{1}\cap\alpha^{-1}(s_{1}),\rho]$ and
$r_{2}\in\mathcal{I}_{\mathcal{D}}[K_{2}\cap\alpha^{-1}(s_{2}),\rho]$. It
follows that $(s_{1},r_{1})\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})$ and
$(s_{2},r_{2})\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$. Since
$r\leq\rho(U)=\rho(U_{1})\cdot\rho(U_{2})=r_{1}r_{2}$, it follows by
definition of our multiplication that
$(s,r)\in\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cdot\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$
which concludes the proof (note that we used the hypothesis that
$\tau^{\mathcal{D}}_{\alpha,\rho}(K_{1})\cdot\tau^{\mathcal{D}}_{\alpha,\rho}(K_{2})$
is closed under downset by definition). ∎

######  Remark 7.5.

An important point is that $\tau^{\mathcal{D}}_{\alpha,\rho}$ is not nice in
general even when $\rho$ itself is nice. Moreover, given a (regular) language
$K\subseteq A^{*}$, computing its image $\tau^{\mathcal{D}}_{\alpha,\rho}(K)$
is a difficult task: one needs to compute all $\mathcal{D}$-optimal
$\rho$-imprints $\mathcal{I}_{\mathcal{D}}[K\cap\alpha^{-1}(s),\rho]$ for
$s\in M$.

Let us provide an example in which $\tau^{\mathcal{D}}_{\alpha,\rho}$ is not
nice. Consider the class $\mathcal{D}$ which contains all finite languages and
$A^{*}$. One may verify that $\mathcal{D}$ is a quotienting lattice. Moreover,
we let $M=\\{1_{M}\\}$ as the trivial monoid and $\alpha:A^{*}\to M$ as the
only possible morphism. Finally, let $N=\\{1_{N},s\\}$ be the monoid whose
multiplication is defined by $ss=1_{N}$ (and $1_{N}$ is a neutral element).
Clearly, $2^{N}$ is a finite hemiring: the addition is union and the
multiplication is obtained by lifting the one of $N$. We let
$\rho:2^{A^{*}}\to 2^{N}$ as the nice multiplicative rating map defined by
$\rho(a)=\rho(b)=\\{s\\}$ (for every language $K$, $1_{N}\in\rho(K)$ if $K$
contains a word of even length and $s\in\rho(K)$ if $K$ contains a word of odd
length). We show that in this case the multiplicative rating map
$\tau^{\mathcal{D}}_{\alpha,\rho}$ is not nice. By definition, for every
$K\subseteq A^{*}$, we have,

$\tau^{\mathcal{D}}_{\alpha,\rho}(K)=\\{(1_{M},r)\mid\text{$r\in\mathcal{I}_{\mathcal{D}}[K,\rho]$}\\}$

Since the only infinite language in $\mathcal{D}$ is $A^{*}$, a
$\mathcal{D}$-cover of $A^{*}$ must contain it. Hence, since
$\rho(A^{*})=\\{1_{N},s\\}$, we have
$\mathcal{I}_{\mathcal{D}}[A^{*},\rho]=\\{\emptyset,\\{1_{N}\\},\\{s\\},\\{1_{N},s\\}\\}$.
However, given some word $w\in A^{*}$, since $\\{w\\}\in\mathcal{D}$, it is
simple to verify that,

$\mathcal{I}_{\mathcal{D}}[\\{w\\},\rho]=\left\\{\begin{array}[]{ll}\\{\emptyset,\\{1_{N}\\}\\}&\text{if
$w$ has even length}\\\ \\{\emptyset,\\{s\\}\\}&\text{if $w$ has odd
length}\end{array}\right.$

Altogether, it follows that,

$\bigcup_{w\in
A^{*}}\tau^{\mathcal{D}}_{\alpha,\rho}(w)=\\{(1_{M},\emptyset),(1_{M},\\{1_{N}\\}),(1_{M},\\{s\\})\\}\neq\tau^{\mathcal{D}}_{\alpha,\rho}(A^{*})$

Therefore, $\tau^{\mathcal{D}}_{\alpha,\rho}$ is not nice.

######  Remark 7.6.

We use these definitions in the case when $\mathcal{D}=PBPol(\mathcal{C})$ and
consider the multiplicative rating map
$\tau=\tau^{PBPol(\mathcal{C})}_{\alpha,\rho}$. We intend to consider
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$, the
${Pol\/}(\mathcal{C})$-optimal $\beta$-pointed $\tau$-imprint (where $\beta$
is the canonical morphism associated to $\rho$ but this is unimportant for the
moment). Since we proved a characterization of ${Pol\/}(\mathcal{C})$-optimal
pointed imprints (Theorem 6.5), we already have a lot of information on
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$. However, what we cannot do
is use this characterization to directly compute
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ from $\alpha$ and $\rho$.
Indeed, implementing the third operation (${Pol\/}(\mathcal{C})$-closure),
requires evaluating $\tau(V)$ when $V$ is some $\sim_{\mathcal{C}}$-class.

The main consequence of these observations is that we never manipulate
$\tau^{\mathcal{D}}_{\alpha,\rho}$ in algorithms. It is only an object that we
shall use when proving the correction of our characterization of
$PBPol(\mathcal{C})$-optimal pointed imprints.

###  7.2. Characterization

We now turn to our characterization of $PBPol(\mathcal{C})$-optimal pointed
imprints. Let $\alpha:A^{*}\to M$ be a $\mathcal{C}$-compatible morphism and
$\rho:2^{A^{*}}\to R$ be a $\mathcal{C}$-compatible multiplicative rating map.
We define a notion of _$PBPol(\mathcal{C})$ -saturated subset of $M\times R$_.
Our theorem then states that when $\rho$ is nice, the least such subset is
exactly $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$, the
$PBPol(\mathcal{C})$-optimal $\alpha$-pointed imprint on $\rho$.

######  Remark 7.7.

We do not need the hypothesis that $\rho$ is nice to define
$PBPol(\mathcal{C})$-saturated subsets of $M\times R$: the definition makes
sense for any $\mathcal{C}$-compatible multiplicative rating map. However, we
shall need this hypothesis to prove that the least one is
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$.

######  Remark 7.8.

Since $\alpha$ is $\mathcal{C}$-compatible, for any $s\in M$,
$[s]_{\mathcal{C}}$, is well-defined as a $\sim_{\mathcal{C}}$-class
containing $\alpha^{-1}(s)$. Moreover, since $\rho$ is
$\mathcal{C}$-compatible, for any $r\in R$, $[r]_{\mathcal{C}}$ is well-
defined as a $\sim_{\mathcal{C}}$-class such that for any $w\in A^{*}$
satisfying $r=\rho(w)$, we have $w\in[r]_{\mathcal{C}}$.

As announced, it turns out that our characterization simultaneously describes
two sets. The first one is
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq M\times R$: this is
the set that we want to compute. The second one is
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq R\times 2^{M\times
R}$ (where $\beta:A^{*}\to R_{A^{*}}$ is the canonical morphism associated to
$\rho$ and $\tau:2^{A^{*}}\to 2^{M\times R}$ is the multiplicative rating map
$\tau^{PBPol(\mathcal{C})}_{\alpha,\rho}$ built from $PBPol(\mathcal{C})$,
$\rho$ and $\alpha$): this is an auxiliary object needed for the computation.
This is reflected in the definition of $PBPol(\mathcal{C})$-saturated objects:
it describes the properties satisfied by these two sets. More precisely, the
definition applies to pairs $(S,\mathcal{T})$ where $S\subseteq M\times R$ and
$\mathcal{T}\subseteq R\times 2^{M\times R}$.

######  Remark 7.9.

We use the multiplication on $2^{M\times R}$ defined at the beginning of the
section. It is not the most natural one. Given $T_{1},T_{2}\in 2^{M\times R}$,
their multiplication is,

$T_{1}\cdot T_{2}=\\{(s_{1}s_{2},r)\mid\text{there exists $(s_{1},r_{1})\in
T_{1}$ and $(s_{2},r_{2})\in T_{2}$ such that $r\leq r_{1}r_{2}$}\\}$

Given a pair $(S,\mathcal{T})$ with $S\subseteq M\times R$ and
$\mathcal{T}\subseteq R\times 2^{M\times R}$ we say that $(S,\mathcal{T})$ is
$PBPol(\mathcal{C})$-saturated (for $\alpha$ and $\rho$) when the following
conditions are satisfied:

  * •

The set $S$ contains $\mathcal{P}_{\mathit{triv}}[\alpha,\rho]$ and is closed
under the following operations:

    1. (1)

Downset: If $(s,r)\in S$ and $r^{\prime}\leq r$, then $(s,r^{\prime})\in S$.

    2. (2)

Multiplication: for any $(s_{1},r_{1}),(s_{2},r_{2})\in S$, we have
$(s_{1}s_{2},r_{1}r_{2})\in S$.

    3. (3)

$PBPol(\mathcal{C})$-closure. For any $(r,T)\in\mathcal{T}$ and any idempotent
$(e,f)\in T\subseteq M\times R$,

$(e,f\cdot(r+\rho(\varepsilon))\cdot f)\in S$

  * •

For any $w\in A^{*}$, if $r=\rho(w)$ and $s=\alpha(w)$, then
$(r,\\{(s,r^{\prime})\mid r^{\prime}\leq r\\})\in\mathcal{T}$. Moreover,
$\mathcal{T}$ is closed under the following operations:

    1. (4)

Downset: If $(r,T)\in\mathcal{T}$ and $T^{\prime}\subseteq T$, then
$(r,T^{\prime})\in\mathcal{T}$.

    2. (5)

Multiplication: For any $(r_{1},T_{1}),(r_{2},T_{2})\in\mathcal{T}$, we have
$(r_{1}r_{2},T_{1}T_{2})\in\mathcal{T}$.

    3. (6)

Nested closure. For any idempotent $(f,E)\in\mathcal{T}$,

$(f,E\cdot T\cdot E)\in\mathcal{T}\quad\text{where $T=\\{(s,r)\in
S\mid[f]_{\mathcal{C}}=[s]_{\mathcal{C}}\\}$}$

######  Remark 7.10.

Observe that the conditions on $S$ and $\mathcal{T}$ are mutually dependent.
On one hand, the $PBPol(\mathcal{C})$-closure operation generates elements of
$S$ from elements of $\mathcal{T}$. On the other hand, nested closure does the
opposite, it builds element of $\mathcal{T}$ from those in $S$.

Finally, we say that a subset $S\subseteq M\times R$ is
$PBPol(\mathcal{C})$-saturated (for $\alpha$ and $\rho$), when there exists
another subset $\mathcal{T}\subseteq R\times 2^{M\times R}$ such that the pair
$(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated.

We may now state the main theorem of this section. It turns out that when
$\rho$ is nice, the least $PBPol(\mathcal{C})$-saturated subset of $M\times R$
is $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$.

######  Theorem 7.11 (Characterization of $PBPol(\mathcal{C})$-optimal
imprints).

Let $\alpha:A^{*}\to M$ be a $\mathcal{C}$-compatible morphism and
$\rho:2^{A^{*}}\to R$ a nice $\mathcal{C}$-compatible multiplicative rating
map. Then, $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ is the least
$PBPol(\mathcal{C})$-saturated subset of $M\times R$.

By definition, of $PBPol(\mathcal{C})$-saturated sets Theorem 7.11 yields a
least fixpoint algorithm for computing the set
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ from a
$\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a nice
$\mathcal{C}$-compatible multiplicative rating map $\rho 2^{A^{*}}\to R$. Let
us briefly explain how to proceed.

One may compute the least pair $(S,\mathcal{T})$ with $S\subseteq M\times R$
and $\mathcal{T}\subseteq R\times 2^{M\times R}$ which is
$PBPol(\mathcal{C})$-saturated. We use a least fixpoint procedure which starts
from the pair
$(\mathcal{P}_{\mathit{triv}}[\alpha,\rho],\mathcal{T}^{\prime})$ where
$\mathcal{T}^{\prime}$ contains all pairs $(r,\\{(s,r^{\prime})\mid
r^{\prime}\leq r\\})$ where $r=\rho(w)$ and $s=\alpha(w)$ for some $w\in
A^{*}$. Then, we saturate this starting pair with the six operations in the
definition which can clearly be implemented. Once we have this least
$PBPol(\mathcal{C})$-saturated pair $(S,\mathcal{T})$ in hand, we obtain from
Theorem 7.11 that $S$ is exactly the desired set
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$.

######  Remark 7.12.

Theorem 7.11 does not describe the least subset $\mathcal{T}\subseteq R\times
2^{M\times R}$ such that the pair
$(\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho],\mathcal{T})$ is
$PBPol(\mathcal{C})$-saturated (which we also compute with our least fixpoint
procedure). This is because, we are mainly interested in
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$: $\mathcal{T}$ is only an
auxiliary object that is required for the computation. However, a byproduct of
our proof is that $\mathcal{T}$ is exactly
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ where $\beta:A^{*}\to
R_{A^{*}}$ is the canonical morphism which is associated to $\rho$ and
$\tau:2^{A^{*}}\to 2^{M\times R}$ is the multiplicative rating map
$\tau^{PBPol(\mathcal{C})}_{\alpha,\rho}$.

######  Remark 7.13.

The hypothesis that $\rho$ is nice in Theorem 7.11 is mandatory: the statement
does not hold for arbitrary multiplicative rating maps. This fact is rather
intuitive. One may verify from its definition that the least
$PBPol(\mathcal{C})$-saturated subset of $M\times R$ may only contain pairs
$(s,r)$ where the element $r\in R$ is built by summing and multiplying
elements of the form $\rho(w)\in R$ (i.e. images of singletons). Thus,
considering $PBPol(\mathcal{C})$-saturated subsets only makes sense when the
multiplicative rating map $\rho$ is characterized by the images of singletons:
this is exactly the definition of nice multiplicative rating maps.

We complete the characterization by stating the desired corollary. It is now
immediate from Proposition 5.18 that $PBPol(\mathcal{C})$-covering is
decidable.

######  Corollary 7.14.

Let $\mathcal{C}$ be a finite quotienting Boolean algebra. Then,
$PBPol(\mathcal{C})$-covering is decidable.

We turn to the proof of Theorem 7.11. In this section, we concentrate on the
“easy” direction which corresponds to soundness of the least fixpoint
procedure: for $\alpha:A^{*}\to M$ and $\rho:2^{A^{*}}\to R$ satisfying the
conditions of the theorem, we show that
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq M\times R$ is indeed
$PBPol(\mathcal{C})$-saturated. The converse direction (i.e. that
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ is the least such subset of
$M\times R$) requires more work and we postpone it to the next section.

###  7.3. Soundness

We fix a $\mathcal{C}$-compatible morphism $\alpha:A^{*}\to M$ and a nice
$\mathcal{C}$-compatible multiplicative rating map $\rho:2^{A^{*}}\to R$ for
the proof. We show that $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ is
$PBPol(\mathcal{C})$-saturated.

######  Remark 7.15.

We do not use the hypothesis that $\rho$ is nice here. This is only needed for
the other direction of the proof.

By definition, we first need to choose a subset $\mathcal{T}\subseteq R\times
2^{M\times R}$ and then prove that the pair
$(\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho],\mathcal{T})$ is
$PBPol(\mathcal{C})$-saturated. Let $\beta:A^{*}\to R_{A^{*}}$ be the
canonical morphism which is associated to $\alpha$ (recall that
$R_{A^{*}}\subseteq R$ is the monoid $R_{A^{*}}=\\{\rho(w)\mid w\in
A^{*}\\}$). Note that $\beta$ is $\mathcal{C}$-compatible by Fact 5.8.
Moreover, we let $\tau:2^{A^{*}}\to 2^{M\times R}$ as the multiplicative
rating map $\tau^{PBPol(\mathcal{C})}_{\alpha,\rho}$:

$\begin{array}[]{llll}\tau:&2^{A^{*}}&\to&2^{M\times R}\\\
&K&\mapsto&\\{(s,r)\in M\times
R\mid\text{$r\in\mathcal{I}_{PBPol(\mathcal{C})}[K\cap\alpha^{-1}(s),\rho]$}\\}\end{array}$

Consider the set $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq
R_{A^{*}}\times 2^{M\times R}\subseteq R\times 2^{M\times R}$. As expected, we
prove that,

The pair
$(\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho],\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau])$
is $PBPol(\mathcal{C})$-saturated

Since ${Pol\/}(\mathcal{C})$ and $PBPol(\mathcal{C})$ are both quotienting
lattices, we already know from Lemma 5.20 that
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ contains
$\mathcal{P}_{\mathit{triv}}[\alpha,\rho]$ and is closed under downset and
multiplication. Moreover, we know that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ is closed under downset and
multiplication. Therefore, we may concentrate on proving the three following
properties:

  1. (1)

For any $w\in A^{*}$, if $r=\rho(w)$ and $s=\alpha(w)$, then
$(r,\\{(s,r^{\prime})\mid r^{\prime}\leq
r\\})\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$.

  2. (2)

$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ satisfies nested closure
(i.e. Operation (6)).

  3. (3)

$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ satisfies
$PBPol(\mathcal{C})$-closure (i.e. Operation (3)).

#### First property

Consider $w\in A^{*}$, $r=\rho(w)$ and $s=\alpha(w)$. We have to show that the
pair $(r,\\{(s,r^{\prime})\mid r^{\prime}\leq r\\})$ belongs to
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$.

Since $\beta(w)=\rho(w)$ (this is the definition of $\beta$), we have
$r=\beta(w)$. We show that,

$\\{(s,r^{\prime})\mid r^{\prime}\leq r\\}\subseteq\tau(w)$

By definition, it will follow that $(r,\\{(s,r^{\prime})\mid r^{\prime}\leq
r\\})\in\mathcal{P}_{\mathit{triv}}[\beta,\tau]$ which concludes the proof
since
$\mathcal{P}_{\mathit{triv}}[\beta,\tau]\subseteq\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$
by Lemma 5.20.

Let $r^{\prime}\leq r$, we have to show that $(s,r^{\prime})\in\tau(w)$, i.e.
$r^{\prime}\in\mathcal{I}_{PBPol(\mathcal{C})}[\\{w\\}\cap\alpha^{-1}(s),\rho]$
by definition of $\tau$. Since $s=\alpha(w)$, it is immediate that we have
$\\{w\\}\cap\alpha^{-1}(s)=\\{w\\}$. Therefore, we need to show that
$r^{\prime}\in\mathcal{I}_{PBPol(\mathcal{C})}[\\{w\\},\rho]$. This is
immediate: any cover $\mathbf{K}$ of $\\{w\\}$ must contain a language $K$
such that $w\in K$ which implies that
$r^{\prime}\in\mathcal{I}[\rho](\mathbf{K})$ since $r^{\prime}\leq r=\rho(w)$.
This is in particular true for optimal $PBPol(\mathcal{C})$-covers of
$\\{w\\}$ which yields
$r^{\prime}\in\mathcal{I}_{PBPol(\mathcal{C})}[\\{w\\},\rho]$.

#### Second property

We prove that nested closure is satisfied. Consider an idempotent
$(f,E)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq R\times
2^{M\times R}$. We have to show that,

$(f,E\cdot T\cdot
E)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\quad\text{where
$T=\\{(s,r)\in\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\mid[f]_{\mathcal{C}}=[s]_{\mathcal{C}}\\}$}$

We use Theorem 6.5, our characterization of ${Pol\/}(\mathcal{C})$-optimal
pointed imprints. It states that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ is
${Pol\/}(\mathcal{C})$-saturated (for $\tau$). In particular, it satisfies
${Pol\/}(\mathcal{C})$-closure which yields,

$(f,E\cdot\tau([f]_{\mathcal{C}})\cdot
E)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$

Therefore, it suffices to show that $T=\tau([f]_{\mathcal{C}})$ to conclude
the proof. This is what we do. By definition of $\tau$, we know that,

$\tau([f]_{\mathcal{C}})=\\{(s,r)\in M\times
R\mid\text{$r\in\mathcal{I}_{PBPol(\mathcal{C})}[[f]_{\mathcal{C}}\cap\alpha^{-1}(s),\rho]$}\\}$

Since $\alpha:A^{*}\to M$ is $\mathcal{C}$-compatible, we know that any
$\alpha^{-1}(s)$ is included in the $\sim_{\mathcal{C}}$-class
$[s]_{\mathcal{C}}$. Therefore, the intersection
$[f]_{\mathcal{C}}\cap\alpha^{-1}(s)$ is either equal to $\alpha^{-1}(s)$
(when $[f]_{\mathcal{C}}=[s]_{\mathcal{C}}$) or empty (when
$[f]_{\mathcal{C}}\neq[s]_{\mathcal{C}}$). In the latter case,
$\mathcal{I}_{PBPol(\mathcal{C})}[[f]_{\mathcal{C}}\cap\alpha^{-1}(s),\rho]$
is empty. Therefore, we obtain that,

$\tau([f]_{\mathcal{C}})=\\{(s,r)\in M\times
R\mid\text{$[f]_{\mathcal{C}}=[s]_{\mathcal{C}}$ and
$r\in\mathcal{I}_{PBPol(\mathcal{C})}[\alpha^{-1}(s),\rho]$}\\}$

Moreover, we have $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]=\\{(s,r)\in
M\times
R\mid\text{$r\in\mathcal{I}_{PBPol(\mathcal{C})}[\alpha^{-1}(s),\rho]$}\\}$ by
definition. Therefore, this can be reformulated as,

$\tau([f]_{\mathcal{C}})=\\{(s,r)\in\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\mid[f]_{\mathcal{C}}=[s]_{\mathcal{C}}\\}=T$

This concludes the proof.

#### Third property

We show that $PBPol(\mathcal{C})$-closure is satisfied. Consider a pair
$(r,T)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq R\times
2^{M\times R}$. Moreover, let $(e,f)\in T\subseteq M\times R$ be an
idempotent. We have to show that,

$(e,f\cdot(r+\rho(\varepsilon))\cdot
f)\in\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$

This requires more work. We shall need the following simple fact. Recall that
given a quotienting lattice $\mathcal{D}$, we write
${co\/}\textup{-}\mathcal{D}$ for the quotienting lattice containing all
complements of languages in $\mathcal{D}$.

######  Fact 7.16.

There exists a finite quotienting lattice
$\mathcal{D}\subseteq{Pol\/}(\mathcal{C})$ such that,

$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]=\mathcal{P}_{{Pol\/}({co\/}\textup{-}\mathcal{D})}[\alpha,\rho]$

###### Proof.

For all $s\in M$, let $\mathbf{K}_{s}$ be an optimal
$PBPol(\mathcal{C})$-cover of $\alpha^{-1}(s)$ (for $\rho$). Recall that we
showed in Lemma 3.6 that
$PBPol(\mathcal{C})={Pol\/}({co\/}\textup{-}{Pol\/}(\mathcal{C}))$. Thus,
since there are finitely many languages in the sets $\mathbf{K}_{s}$ for $s\in
M$, there exists some $k\in{\rm Nature}$ such that all these languages belong
to ${Pol\/}({co\/}\textup{-}Pol_{k}(\mathcal{C}))$. Here,
$Pol_{k}(\mathcal{C})$ denotes a stratum in our stratification of
${Pol\/}(\mathcal{C})$ into finite quotienting lattices (see Section 4 for
details). It now suffices to choose $\mathcal{D}=Pol_{k}(\mathcal{C})$. ∎

In view of Fact 7.16, it now suffices to show that,

$(e,f\cdot(r+\rho(\varepsilon))\cdot
f)\in\mathcal{P}_{{Pol\/}({co\/}\textup{-}\mathcal{D})}[\alpha,\rho]$

By definition, this amounts to proving that $f\cdot(r+\rho(\varepsilon))\cdot
f\in\mathcal{I}_{{Pol\/}({co\/}\textup{-}\mathcal{D})}[\alpha^{-1}(e),\rho]$.
We fix an arbitrary optimal ${Pol\/}({co\/}\textup{-}\mathcal{D})$-cover
$\mathbf{K}$ of $\alpha^{-1}(e)$ and show that
$f\cdot(r+\rho(\varepsilon))\cdot f\in\mathcal{I}[\rho](\mathbf{K})$. Since
${co\/}\textup{-}\mathcal{D}$ is a finite quotienting lattice, we have a
stratification of ${Pol\/}({co\/}\textup{-}\mathcal{D})$ which we introduced
in Section 4. Recall that the strata are denoted by
$Pol_{k}({co\/}\textup{-}\mathcal{D})$ and the associated canonical preorder
relations by $\leqslant_{k}$. Since $\mathbf{K}$ is a finite set of languages
in ${Pol\/}({co\/}\textup{-}\mathcal{D})$, we have a stratum $k\in{\rm
Nature}$ such that all languages in $\mathbf{K}$ belong to
$Pol_{k}({co\/}\textup{-}\mathcal{D})$. Consequently, we have
$\mathcal{I}_{Pol_{k}({co\/}\textup{-}\mathcal{D})}[\alpha^{-1}(e),\rho]\subseteq\mathcal{I}[\rho](\mathbf{K})$
and it now suffices to show that $f\cdot(r+\rho(\varepsilon))\cdot
f\in\mathcal{I}_{Pol_{k}({co\/}\textup{-}\mathcal{D})}[\alpha^{-1}(e),\rho]$.
By Lemma 5.15, we have to exhibit $w\in\alpha^{-1}(e)$ and $K\subseteq A^{*}$
such that $w\leqslant_{k}K$ and $f\cdot(r+\rho(\varepsilon))\cdot
f\leq\rho(K)$. This is what we do.

We first use our hypotheses that
$(r,T)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ and $(e,f)\in T$ to
introduce a few objects that we need to define $w$ and $K$. We do so in the
following lemma. Recall that $\leqslant_{\mathcal{D}}$ denotes the canonical
preorder associated to the finite quotienting lattice $\mathcal{D}$ (which is
compatible with word concatenation by Lemma 2.9).

######  Lemma 7.17.

There exists $u,v\in A^{*}$ and $H\subseteq A^{*}$ satisfying the following
conditions:

  * •

$\rho(u)=r$, $\alpha(v)=e$ and $f\leq\rho(H)$.

  * •

$u\leqslant_{\mathcal{D}}v$ and $v\leqslant_{k}H$.

###### Proof.

We first define $u,v\in A^{*}$ and $H\subseteq A^{*}$. Since
$(r,T)\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]$ and
$\mathcal{D}\subseteq{Pol\/}(\mathcal{C})$ it follows from Fact 5.12 that
$(r,T)\in\mathcal{P}_{\mathcal{D}}[\beta,\tau]$. This implies that
$T\in\mathcal{I}_{\mathcal{D}}[\beta^{-1}(r),\tau]$. Therefore, Lemma 5.15
yields $u\in\beta^{-1}(r)$ and $L\subseteq A^{*}$ such that
$T\subseteq\tau(L)$ and $u\leqslant_{\mathcal{D}}L$. Moreover, since $(e,f)\in
T\subseteq\tau(L)$, we obtain by definition of $\tau$ that,

$f\in\mathcal{I}_{PBPol(\mathcal{C})}[L\cap\alpha^{-1}(e),\rho]$

Since $\mathcal{D}\subseteq{Pol\/}(\mathcal{C})$, we have
$Pol_{k}({co\/}\textup{-}\mathcal{D})\subseteq{Pol\/}({co\/}\textup{-}\mathcal{D})\subseteq
PBPol(\mathcal{C})$. Therefore, it follows from Fact 5.12 that
$f\in\mathcal{I}_{Pol_{k}({co\/}\textup{-}\mathcal{D})}[L\cap\alpha^{-1}(e),\rho]$.
Using Lemma 5.15, this yields $v\in L\cap\alpha^{-1}(e)$ and $H\subseteq
A^{*}$ such that $v\leqslant_{k}H$ and $f\leq\rho(H)$.

Let us verify that $u,v\in A^{*}$ and $H\subseteq A^{*}$ satisfy the
conditions described in the lemma. We have $\rho(u)=r$ since
$u\in\beta^{-1}(r)$ which means that $\rho(u)=\beta(u)=r$. Moreover,
$\alpha(v)=e$, $f\leq\rho(H)$ and $v\leqslant_{k}H$ hold by definition of $v$
and $H$. Finally, $u\leqslant_{\mathcal{D}}v$ holds since $v\in L$ and we have
$u\leqslant_{\mathcal{D}}L$. ∎

We are now ready to define the appropriate $w\in\alpha^{-1}(e)$ and
$K\subseteq A^{*}$ such that $w\leqslant_{k}K$ and
$f\cdot(r+\rho(\varepsilon))\cdot f\leq\rho(K)$. We fix $u,v\in A^{*}$ and
$H\subseteq A^{*}$ as defined in Lemma 7.17. Let $p\geq 1$ be the period of
${co\/}\textup{-}\mathcal{D}$ (see Fact 4.10 for the definition) and
$\ell=p\times 2^{k+1}$. We define,

$w=v^{\ell}\quad\text{and}\quad K=H^{\ell+p-1}uH^{\ell}\cup H^{\ell}$

Clearly, $w\in\alpha^{-1}(e)$ since $\alpha(v)=e$ and $e$ is an idempotent of
$M$. It remains to show that $w\leqslant_{k}K$ and
$f\cdot(r+\rho(\varepsilon))\cdot f\leq\rho(K)$. We start with the latter. By
definition and since $\rho$ is a multiplicative rating map,

$\begin{array}[]{lll}\rho(K)&=&(\rho(H))^{\ell+p-1}\cdot\rho(u)\cdot(\rho(H))^{\ell}+(\rho(H))^{\ell}\\\
&=&(\rho(H))^{\ell+p-1}\cdot\rho(u)\cdot(\rho(H))^{\ell}+(\rho(H))^{\ell-1}\cdot\rho(\varepsilon)\cdot\rho(H)\end{array}$

By definition in Lemma 7.17, we have $\rho(u)=r$ and $f\leq\rho(H)$. Thus,
since $f$ is idempotent, we obtain as desired that,

$f\cdot(r+\rho(\varepsilon))\cdot f=f\cdot\rho(u)\cdot
f+f\cdot\rho(\varepsilon)\cdot f\leq\rho(K)$

We finish with the proof that $w\leqslant_{k}K$. Let $x\in K$, we show that
$w\leqslant_{k}x$. By definition, we have $K=H^{\ell+p-1}uH^{\ell}\cup
H^{\ell}$. Moreover, we know that $v\leqslant_{k}H$ by definition in Lemma
7.17. Thus, since $x\in K$ and $\leqslant_{k}$ is compatible with
concatenation (see Lemma 2.9), we obtain that one of the two following
properties hold:

  * •

$v^{\ell}\leqslant_{k}x$ (when $x\in H^{\ell}$) or,

  * •

$v^{\ell+p-1}\cdot u\cdot v^{\ell}\leqslant_{k}x$ (when $x\in
H^{\ell+p-1}uH^{\ell}$).

Thus, by transitivity, it suffices to show that $w\leqslant_{k}v^{\ell}$ and
$w\leqslant_{k}v^{\ell+p-1}\cdot u\cdot v^{\ell}$. The former is immediate: we
have $w=v^{\ell}$ by definition.

It remains to show that $w\leqslant_{k}v^{\ell+p-1}\cdot u\cdot v^{\ell}$.
Recall that $\leqslant_{k}$ is the canonical preorder of
$Pol_{k}({co\/}\textup{-}\mathcal{D})$. By definition in Lemma 7.17, we have
$u\leqslant_{\mathcal{D}}v$. Moreover, since $\leqslant_{\mathcal{D}}$ is
compatible with concatenation, this implies
$v^{p-1}u\leqslant_{\mathcal{D}}v^{p}$. It follows that
$v^{p}\leqslant_{{co\/}\textup{-}\mathcal{D}}v^{p-1}u$. Indeed,
$v^{p-1}u\leqslant_{\mathcal{D}}v^{p}$ means that for any $L\in\mathcal{D}$,
we have $v^{p-1}u\in L\Rightarrow v^{p}\in L$. The contrapositive then states
that for any $L\in\mathcal{D}$, we have $v^{p}\not\in L\Rightarrow
v^{p-1}u\not\in L$. Finally, since the languages of
${co\/}\textup{-}\mathcal{D}$ are the complements of those in $\mathcal{D}$,
it follows that for all $L\in{co\/}\textup{-}\mathcal{D}$, we have $v^{p}\in
L\Rightarrow v^{p-1}u\in L$, i.e.
$v^{p}\leqslant_{{co\/}\textup{-}\mathcal{D}}v^{p-1}u$. Therefore, since
$w=v^{\ell}$ and $\ell=p2^{k+1}$ where $p$ is the period of
${co\/}\textup{-}\mathcal{D}$, we obtain as desired that
$w\leqslant_{k}v^{\ell}\cdot v^{p-1}u\cdot v^{\ell}$ from Lemma 4.12.

##  8\. Completeness in Theorem 7.11

This last section is devoted to proving the difficult direction in Theorem
7.11. It corresponds to completeness in the least fixpoint algorithm for
$PBPol(\mathcal{C})$-covering.

We let $\alpha:A^{*}\to M$ as a $\mathcal{C}$-compatible morphism and
$\rho:2^{A^{*}}\to R$ as a nice $\mathcal{C}$-compatible multiplicative rating
map. Recall that Theorem 7.11 states that
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$ is the smallest
$PBPol(\mathcal{C})$-saturated subset of $M\times R$. We have already showed
in the previous section that $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$
is $PBPol(\mathcal{C})$-saturated (this was the soundness proof). Therefore,
it remains to show that it is the smallest such subset. This is the purpose of
this section.

Thus, we fix some arbitrary $PBPol(\mathcal{C})$-saturated subset $S$ of
$M\times R$ and prove that it includes
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$. That is, we show,

$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$

The argument is more involved than what we did for ${Pol\/}(\mathcal{C})$ in
Section 6. Indeed, the definition of $PBPol(\mathcal{C})$-saturated sets is
involved and this is reflected in our argument.

We write $\beta:A^{*}\to R_{A^{*}}$ for the canonical morphism associated to
$\rho$ (which is $\mathcal{C}$-compatible by Fact 5.8). Moreover, we write
$\tau:2^{A^{*}}\to 2^{M\times R}$ for the multiplicative rating map
$\tau^{PBPol(\mathcal{C})}_{\alpha,\rho}$:

$\begin{array}[]{llll}\tau:&2^{A^{*}}&\to&2^{M\times R}\\\
&K&\mapsto&\\{(s,r)\in M\times
R\mid\text{$r\in\mathcal{I}_{PBPol(\mathcal{C})}[K\cap\alpha^{-1}(s),\rho]$}\\}\end{array}$

Since $S$ is $PBPol(\mathcal{C})$-saturated, the definition yields a subset
$\mathcal{T}\subseteq R\times 2^{M\times R}$ such that the pair
$(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated. We actually prove the two
following inclusions,

$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq
S\quad\text{and}\quad\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq\mathcal{T}$

Of course, the difficulty is that these two properties are mutually dependent.
This is not surprising since the conditions which make $S$ and $\mathcal{T}$
$PBPol(\mathcal{C})$-saturated are mutually dependent themselves. We cope with
this problem by following three steps:

  1. (1)

Step 1: ${Pol\/}(\mathcal{C})$ argument: First, we investigate the set
$\mathcal{T}$. Let us point out that we do not yet show that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq\mathcal{T}$: getting
this inclusion requires information on the set $S$ and we do not have any at
this point. Instead, we cope with this problem by introducing a new
multiplicative rating map $\gamma:2^{A^{*}}\to 2^{M\times R}$ which is
intuitively a weaker variant of $\tau$ parametrized by the set $S$ (for any
$K$, $\gamma(K)$ is a restriction of the set $\tau(K)\subseteq M\times R$
which depends on $S$). The main result of this step is as follows:

$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]\subseteq\mathcal{T}$

The key idea is that the definition of $\gamma$ depends on $S$. Therefore,
later in the proof, whenever we exhibit new elements in $S$, this
simultaneously proves the existence of new elements in
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]$. Consequently, the above
inclusion yields that these new elements belong to $\mathcal{T}$ as well (and
we may use them to exhibit even more elements in $S$). This is based on
Theorem 6.5 (our characterization of ${Pol\/}(\mathcal{C})$-optimal pointed
imprints): we apply it to the multiplicative rating map $\gamma$.

  2. (2)

Step 2: a finite quotienting Boolean algebra
$\mathcal{D}\subseteq{BPol\/}(\mathcal{C})$: This step reexamines the results
obtained in Step 1. We use our new multiplicative rating map $\gamma$ to
define a key object of the proof: a finite quotienting Boolean algebra
$\mathcal{D}\subseteq{BPol\/}(\mathcal{C})$. Intuitively, $\mathcal{D}$ is
designed to contain any language involved in an optimal
${Pol\/}(\mathcal{C})$-cover of $\beta^{-1}(r)$ for $\gamma$ where $r\in
R_{A^{*}}$.

  3. (3)

Step 3: $PBPol(\mathcal{C})$-argument: This step uses all preliminary results
that we have obtained in the previous ones to finally prove the desired
property:

$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$

###  8.1. Step 1: ${Pol\/}(\mathcal{C})$ argument

We start by defining the auxiliary multiplicative rating map
$\gamma:2^{A^{*}}\to 2^{M\times R}$ that we announced above. Then, we use
Theorem 6.5 to prove that,

$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]\subseteq\mathcal{T}$

As we explained, $\gamma$ is designed as a weaker variant of $\tau$
parametrized by the set $S\subseteq M\times R$. We use this new object to cope
with the fact that we do not yet have enough information on $S$ to prove
directly that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq\mathcal{T}$. The
definition is based on the notion of good languages which we present now.

Good languages. Given some language $G\subseteq A^{*}$, we shall say that $G$
is _good_ when the two following conditions are satisfied:

  * •

$G$ is closed under infixes: for any $u,v_{1},v_{2}\in A^{*}$, if
$v_{1}uv_{2}\in G$, then $u\in G$.

  * •

$\tau(G)\subseteq S$.

Note that we already know at least one simple good language: the empty one
($\emptyset$) which trivially satisfies both conditions.

######  Remark 8.1.

Our ultimate goal in the proof is to prove that
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$. Thus, since
$\tau(A^{*})=\\{(s,r)\mid
r\in\mathcal{I}_{PBPol(\mathcal{C})}[\alpha^{-1}(s),\rho]\\}=\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]$
by definition, this means that the universal language $A^{*}$ is good.
However, we do not know this yet. While this will be implicit, a key point in
later steps of the proof is that it exhibits more and more elements within
$S$. Therefore, we shall obtain increasingly large good languages until we
prove that $A^{*}$ itself is good.

We shall need the following fact which is used for combining two good
languages into a single larger one.

######  Fact 1.

Let $G_{1},G_{2}$ be good languages. Then $G_{1}G_{2}\cup G_{1}\cup G_{2}$ is
a good language as well.

######  Proof 8.2.

Clearly, $G_{1}G_{2}\cup G_{1}\cup G_{2}$ is closed under infixes since this
was the case for both $G_{1}$ and $G_{2}$. Hence, we may concentrate on the
second property in the definition of good languages. Since $\tau$ is a
multiplicative rating map, we have,

$\tau(G_{1}G_{2}\cup G_{1}\cup
G_{2})=\tau(G_{1})\cdot\tau(G_{2})\cup\tau(G_{1})\cup\tau(G_{2})$

We already know that $\tau(G_{1})\subseteq S$ and $\tau(G_{2})\subseteq S$
since $G_{1},G_{2}$ are good. Thus, it suffices to verify that
$\tau(G_{1})\cdot\tau(G_{2})\subseteq S$. By definition,
$(s,r)\in\tau(G_{1})\cdot\tau(G_{2})$ satisfies $s=s_{1}s_{2}$ and $r\leq
r_{1}r_{2}$ for $(s_{1},r_{1})\in\tau(G_{1})\subseteq S$ and
$(s_{2},r_{2})\in\tau(G_{2})\subseteq S$. Since $S$ is
$PBPol(\mathcal{C})$-saturated, it is closed under downset and multiplication
which yields $(s,r)\in S$.

Definition of $\gamma$. We now use good languages to introduce our new
multiplicative rating map $\gamma:2^{A^{*}}\to 2^{M\times R}$. As we
explained, it is defined from $\tau$. Recall that $2^{M\times R}$ is a finite
hemiring which we already used as the evaluation set for $\tau$. In
particular, recall that it uses a special multiplication which we defined
above. We define,

$\begin{array}[]{llll}\gamma:&2^{A^{*}}&\to&2^{M\times R}\\\
&K&\mapsto&\\{(s,r)\mid\text{$(s,r)\in\tau(K\cap G)$ for some good language
$G$}\\}\end{array}$

Note that the definition of $\gamma$ depends on $S\subseteq M\times R$ since
this set constrains which languages are good.

######  Remark 8.3.

This new map $\gamma$ is strongly related to $\tau$. An apparent connection is
that for any $K\subseteq A^{*}$, we have $\gamma(K)\subseteq\tau(K)$. Indeed,
given $(s,r)\in\gamma(K)$, we have $(s,r)\in\tau(K\cap G)$ for some good
language $G$. Moreover, we know that $\tau(K\cap G)\subseteq\tau(K)$ since
$K\cap G\subseteq K$. Thus, we get that $(s,r)\in\tau(K)$. However, the
connection between $\gamma$ and $\tau$ is in fact much stronger. Since we
shall later obtain that $A^{*}$ is good (see Remark 8.1), the converse
inclusion holds as well: $\gamma(K)\subseteq\tau(K)$. Thus, $\gamma$ and
$\tau$ are actually the same object. Unfortunately, this is an information
that we are not able to use. Indeed, we only obtain it at the end of our
proof: the fact that $A^{*}$ is good follows from our end goal
($\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$).

Another way to explain the situation is as follows. We need to use $\gamma$
since we are not able to prove the inclusion
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\tau]\subseteq\mathcal{T}$ directly.
However, it turns out that when we shall finally obtain
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$ (the proof relies
on the inclusion
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]\subseteq\mathcal{T}$), we
will also realize that $\gamma$ was $\tau$ all along.

Before we can use $\gamma$, we first need to verify that it is indeed a
multiplicative rating map. We do so in the next lemma (this is a consequence
of the fact that $\tau$ is a multiplicative rating map itself).

######  Lemma 8.4.

The map $\gamma$ is a multiplicative rating map.

######  Proof 8.5.

We need to prove that $\gamma$ is a hemiring morphism. We start by proving
that it is a monoid morphism for addition. Clearly,
$\gamma(\emptyset)=\emptyset$. Indeed,

$\gamma(\emptyset)=\\{(s,r)\mid\text{$(s,r)\in\tau(\emptyset)$}\\}=\emptyset$

We now show that for any $K_{1},K_{2}\subseteq A^{*}$, we have
$\gamma(K_{1}\cup K_{2})=\gamma(K_{1})\cup\gamma(K_{2})$. Assume first that
$(s,r)\in\gamma(K_{1})\cup\gamma(K_{2})$. By symmetry assume that
$(s,r)\in\gamma(K_{1})$. By definition, we have a good language $G$ such that
$(s,r)\in\tau(K_{1}\cap G)$. Thus, since $K_{1}\cap G\subseteq(K_{1}\cup
K_{2})\cap G$, we get $(s,r)\in\tau((K_{1}\cup K_{2})\cap G)$ which means that
$(s,r)\in\gamma(K_{1}\cup K_{2})$ as desired. Conversely, assume that
$(s,r)\in\gamma(K_{1}\cup K_{2})$. By definition, there exists a good language
$G$ such that $(s,r)\in\tau((K_{1}\cup K_{2})\cap G)$. Thus, since $\tau$ is a
morphism itself, we have $(s,r)\in\tau(K_{1}\cap G)\cup\tau(K_{2}\cap G)$ and
it follows that $(s,r)\in\gamma(K_{1})\cup\gamma(K_{2})$.

We now show that $\gamma$ is a semigroup morphism for multiplication. Let
$K_{1},K_{2}\subseteq A^{*}$. We show that
$\gamma(K_{1}K_{2})=\gamma(K_{1})\cdot\gamma(K_{2})$. Assume first that
$(s,r)\in\gamma(K_{1})\cdot\gamma(K_{2})$. Thus, by definition of our
multiplication on $2^{M\times R}$, we have $(s_{1},r_{1})\in\gamma(K_{1})$ and
$(s_{2},r_{2})\in\gamma(K_{2})$ such that $s=s_{1}s_{2}$ and $r\leq
r_{1}r_{2}$. It then follows from the definition of $\gamma$ that there exist
two good languages $G_{1},G_{2}$ such that,

$(s_{1},r_{1})\in\tau(K_{1}\cap
G_{1})\quad\text{and}\quad(s_{2},r_{2})\in\tau(K_{2}\cap G_{2})$

Since we already know that $\tau$ is multiplicative, it follows that
$(s,r)\in\tau((K_{1}\cap G_{1})(K_{2}\cap G_{2}))$. Moreover, because
$(K_{1}\cap G_{1})(K_{2}\cap G_{2})\subseteq K_{1}K_{2}\cap(G_{1}G_{2}\cup
G_{1}\cup G_{2})$, we get $(s,r)\in\tau(K_{1}K_{2}\cap(G_{1}G_{2}\cup
G_{1}\cup G_{2}))$. Finally, since we know that $G_{1}G_{2}\cup G_{1}\cup
G_{2}$ is good by Fact 1, it follows that $(s,r)\in\gamma(K_{1}K_{2})$ by
definition of $\gamma$.

We finish with the converse inclusion. Let $(s,r)\in\gamma(K_{1}K_{2})$. By
definition, we get a good language $G$ such that $(s,r)\in\tau(K_{1}K_{2}\cap
G)$. Since $G$ is closed under infixes (by definition of good languages), it
is simple to verify that $K_{1}K_{2}\cap G\subseteq(K_{1}\cap G)(K_{2}\cap
G)$. Thus, it follows that,

$(s,r)\in\tau((K_{1}\cap G)(K_{2}\cap G))=\tau(K_{1}\cap G)\cdot\tau(K_{2}\cap
G)$

Therefore, we have $(s_{1},r_{1})\in\tau(K_{1}\cap G)$ and
$(s_{2},r_{2})\in\tau(K_{2}\cap G)$ such that $s=s_{1}s_{2}$ and $r\leq
r_{1}r_{2}$. By definition, $(s_{1},r_{1})\in\gamma(K_{1})$ and
$(s_{2},r_{2})\in\gamma(K_{2})$. Thus, we obtain that,
$(s,r)\in\gamma(K_{1})\cdot\gamma(K_{2})$.

We turn to the main result in Step 1. Using Theorem 6.5 (i.e. our
characterization of ${Pol\/}(\mathcal{C})$ optimal pointed imprints) we prove
that $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]$ is included in
$\mathcal{T}$. Recall that $\mathcal{T}\subseteq R\times 2^{M\times R}$ is a
set such that the pair $(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated
(for $\rho$).

######  Proposition 8.6.

We have
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]\subseteq\mathcal{T}$.

######  Proof 8.7.

We know that $\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]$ is the least
${Pol\/}(\mathcal{C})$-saturated subset of $R_{A^{*}}\times 2^{M\times R}$
(for $\gamma$) by Theorem 6.5. Thus, it suffices to show that $\mathcal{T}$ is
${Pol\/}(\mathcal{C})$-saturated for $\gamma$. It will then be immediate that
$\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]\subseteq\mathcal{T}$ as
desired.

######  Remark 8.8.

Note that we are able to use Theorem 6.5 since $\beta$ is
$\mathcal{C}$-compatible and $\gamma$ is a multiplicative rating map. However,
let us point out that $\gamma$ need not be nice in general. Therefore, it is
important here that this is not a requirement for applying Theorem 6.5.

Recall that by hypothesis, the pair $(S,\mathcal{T})$ is
$PBPol(\mathcal{C})$-saturated for $\rho$. Hence, we already know that
$\mathcal{T}$ is closed under downset and multiplication. It remains to show
that $\mathcal{P}_{\mathit{triv}}[\beta,\gamma]\subseteq\mathcal{T}$ and that
$\mathcal{T}$ satisfies ${Pol\/}(\mathcal{C})$-closure.

We start with $\mathcal{P}_{\mathit{triv}}[\beta,\gamma]\subseteq\mathcal{T}$.
Let $(r,T)\in\mathcal{P}_{\mathit{triv}}[\beta,\gamma]$, we show that
$(r,T)\in\mathcal{T}$. By definition of
$\mathcal{P}_{\mathit{triv}}[\beta,\gamma]$, there exists $w\in A^{*}$ such
that $\rho(w)=\beta(w)=r$ and $T\subseteq\gamma(w)$. Let $s=\alpha(w)$ and
consider the set $T^{\prime}=\\{(s,r^{\prime})\mid r^{\prime}\leq r\\}$. Since
$(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated for $\rho$, it is
immediate by definition that $(r,T^{\prime})\in\mathcal{T}$. We show that
$T\subseteq T^{\prime}$. Since we already established that $\mathcal{T}$ is
closed under downset, this will imply that $(r,T)\in\mathcal{T}$. Let
$(t,r^{\prime})\in T$. We have to show that $s=t$ and $r^{\prime}\leq r$.
Since $T\subseteq\gamma(w)$, we have $(t,r^{\prime})\in\gamma(w)$.
Furthermore, we have $(t,r^{\prime})\in\tau(w)$ since we observed in Remark
8.3 that $\gamma(w)\subseteq\tau(w)$. By definition of $\tau$, this means that
$r^{\prime}\in\mathcal{I}_{PBPol(\mathcal{C})}[\\{w\\}\cap\alpha^{-1}(t),\rho]$.
Therefore, $\\{w\\}\cap\alpha^{-1}(t)\neq\emptyset$ which means that
$\\{w\\}\cap\alpha^{-1}(t)=\\{w\\}$ and $t=\alpha(w)=s$. Moreover, since
$PBPol(\mathcal{C})$ contains all finite languages by Lemma 3.4,
$\mathbf{K}=\\{\\{w\\}\\}$ is a $PBPol(\mathcal{C})$-cover of
$\\{w\\}=\\{w\\}\cap\alpha^{-1}(t)$. Hence, we have
$r^{\prime}\in\mathcal{I}_{PBPol(\mathcal{C})}[\\{w\\}\cap\alpha^{-1}(t),\rho]\subseteq$
which means any $r^{\prime}\leq\rho(w)=r$ by definition.

We turn to ${Pol\/}(\mathcal{C})$-closure. Let $(f,E)\in\mathcal{T}$ be an
idempotent. We have to show that,

$(f,E\cdot\gamma([f]_{\mathcal{C}})\cdot E)\in\mathcal{T}$

Let $T=\\{(s,r)\in S\mid[f]_{\mathcal{C}}=[s]_{\mathcal{C}}\\}$. Since
$(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated for $\rho$, we get from
nested closure (i.e. Operation (6)) that,

$(f,E\cdot T\cdot E)\in\mathcal{T}$

Hence, by closure under downset, it suffices to show that
$\gamma([f]_{\mathcal{C}})\subseteq T$. Let
$(s,r)\in\gamma([f]_{\mathcal{C}})$. By definition, we know that
$(s,r)\in\tau([f]_{\mathcal{C}}\cap G)$ for some good language $G$. Therefore,
$(s,r)\in\tau(G)$ which is a subset of $S$ by the second item in the
definition of good languages. We get that $(s,r)\in S$. Moreover,
$(s,r)\in\tau([f]_{\mathcal{C}})$ which means that we have
$r\in\mathcal{I}_{PBPol(\mathcal{C})}[[f]_{\mathcal{C}}\cap\alpha^{-1}(s),\rho]$
. Therefore, $[f]_{\mathcal{C}}\cap\alpha^{-1}(s)\neq\emptyset$. Since
$\alpha$ is $\mathcal{C}$-compatible, this implies that
$[f]_{\mathcal{C}}=[s]_{\mathcal{C}}$. Altogether, we get that $(s,r)\in T$
which concludes the proof.

###  8.2. Step 2: An auxiliary class
$\mathcal{D}\subseteq{BPol\/}(\mathcal{C})$

We use the multiplicative rating map $\gamma$ introduced in the previous step
to define a finite quotienting Boolean algebra $\mathcal{D}$ included in
${BPol\/}(\mathcal{C})$. This object will serve as a key ingredient when
proving the third step. Moreover, we reformulate Proposition 8.6 as a property
on the equivalence classes of $\sim_{\mathcal{D}}$ (the canonical equivalence
associated to $\mathcal{D}$). This is the formulation that we shall actually
use later.

Given any $r\in R_{A^{*}}$, we may define $\mathbf{H}_{r}$ as an arbitrary
_optimal_ ${Pol\/}(\mathcal{C})$-cover of $\beta^{-1}(r)$ for $\gamma$.
Furthermore, we let $\mathbf{H}=\cup_{r\in R_{A^{*}}}\mathbf{H}_{r}$. Observe
that by definition, $\mathbf{H}$ is a finite set of languages in
${Pol\/}(\mathcal{C})$. Therefore, there exists a stratum
$Pol_{k}(\mathcal{C})$ in our stratification of ${Pol\/}(\mathcal{C})$ (we may
use it since $\mathcal{C}$ is a finite quotienting Boolean algebra, see
Section 4) such that all $H\in\mathbf{H}$ belong to $Pol_{k}(\mathcal{C})$. We
define,

$\mathcal{D}={Bool\/}(Pol_{k}(\mathcal{C}))$

By definition, $\mathcal{D}$ is a finite quotienting Boolean algebra and any
$H\in\mathbf{H}$ belongs to $\mathcal{D}$. We shall work with the canonical
equivalence $\sim_{\mathcal{D}}$ (over $A^{*}$) associated to $\mathcal{D}$.
Note that by definition, we have the following fact.

######  Fact 3.

We have $\mathcal{D}\subseteq{BPol\/}(\mathcal{C})\subseteq
PBPol(\mathcal{C})$. In particular, any $\sim_{\mathcal{D}}$-class $V$ is a
language of $PBPol(\mathcal{C})$.

We now reformulate Proposition 8.6 as a property on the
$\sim_{\mathcal{D}}$-classes. We state it in the following lemma.

######  Lemma 8.9.

Consider a $\sim_{\mathcal{D}}$-class $V\subseteq A^{*}$. Let $v\in V$ and
$r=\rho(v)$. Then,

$(r,\gamma(V))\in\mathcal{T}$

######  Proof 8.10.

By definition, $r=\rho(v)=\beta(v)$. Therefore, $v\in\beta^{-1}(r)$ and since
$\mathbf{H}_{r}$ is a cover of $\beta^{-1}(r)$ by definition, we have
$H\in\mathbf{H}_{r}$ such that $v\in H$. Moreover, $\mathbf{H}_{r}$ is an
optimal ${Pol\/}(\mathcal{C})$-cover of $\beta^{-1}(r)$ for $\gamma$ by
definition. Hence,

$(r,\gamma(H))\in\mathcal{P}_{{Pol\/}(\mathcal{C})}[\beta,\gamma]$

By Proposition 8.6, this yields $(r,\gamma(H))\in\mathcal{T}$. Finally, we
have $H\in\mathcal{D}$ by definition. Therefore, since $V$ is
$\sim_{\mathcal{D}}$-class such that $H\cap V\neq\emptyset$ ($v$ is in the
intersection), we get $V\subseteq H$. It follows that
$\gamma(V)\subseteq\gamma(H)$ since $\gamma$ is a multiplicative rating map.
Finally, we know that $\mathcal{T}$ is closed under downset since
$(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated which yields
$(r,\gamma(V))\in\mathcal{T}$, finishing the proof of Lemma 8.9.

###  8.3. Step 3: $PBPol(\mathcal{C})$-argument

We now come back to our main objective: proving the inclusion
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$. As expected, we
shall rely heavily on the objects introduced in the previous steps: the
multiplicative rating map $\gamma$ and the finite quotienting Boolean algebra
$\mathcal{D}\subseteq{BPol\/}(\mathcal{C})$. Our approach is based on the
following proposition.

######  Proposition 8.11.

For any $s\in M$, there exists a $PBPol(\mathcal{C})$-cover $\mathbf{K}_{s}$
of $\alpha^{-1}(s)$ such that for any $K\in\mathbf{K}_{s}$, we have
$(s,\rho(K))\in S$

The proof of Proposition 8.11 is constructive: we explain how to build the
$PBPol(\mathcal{C})$-covers $\mathbf{K}_{s}$. Once we have them in hand, by
definition of $PBPol(\mathcal{C})$-optimal $\rho$-imprints, it will follow
that for any $s\in M$, we have,

$\mathcal{I}_{PBPol(\mathcal{C})}[\alpha^{-1}(s),\rho]\subseteq$

Thus, since $\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]=\\{(s,r)\in M\times
R\mid r\in\mathcal{I}_{PBPol(\mathcal{C})}[\alpha^{-1}(s),\rho]\\}$ by
definition, it will follow that
$\mathcal{P}_{PBPol(\mathcal{C})}[\alpha,\rho]\subseteq S$ as desired,
finishing the proof.

We now focus on proving Proposition 8.11. The argument is based on the
factorization forest theorem of Simon. We refer the reader to Section 4 for
details on this result. In particular, this is where we need the non-standard
notion of _idempotent height_ which we introduced together with factorization
forests.

Consider the finite quotienting Boolean algebra
$\mathcal{D}\subseteq{BPol\/}(\mathcal{C})$ that we defined in Step 2. Since
$\mathcal{D}$ is closed under quotients, it follows from Lemma 2.9 that
$\sim_{\mathcal{D}}$ (the associated canonical equivalence on $A^{*}$) is a
congruence of finite index for word concatenation. Therefore the quotient set
${A^{*}}/{\sim_{\mathcal{D}}}$ is a finite monoid and the map
$w\mapsto[w]_{\mathcal{D}}$ (which associates its $\sim_{\mathcal{D}}$-class
to any word $w\in A^{*}$) is a morphism. Consequently, the Cartesian product
$P=M\times({A^{*}}/{\sim_{\mathcal{D}}})$ is a finite monoid for the
componentwise multiplication and the following map $\eta:A^{*}\to P$ is a
morphism:

$\begin{array}[]{llll}\eta:&A^{*}&\to&P\\\
&w&\mapsto&(\alpha(w),[w]_{\mathcal{D}})\end{array}$

We shall work with $\eta$-factorization forests. We are now ready to start the
proof of Proposition 8.11 and construct the $PBPol(\mathcal{C})$-covers
$\mathbf{K}_{s}$. We use an induction which we state in the next proposition.
Recall that for any $p\in P$ and any $h,m\in{\rm Nature}$, we write,

$F^{\eta}(p,h,m)\subseteq\eta^{-1}(p)\subseteq A^{*}$

for the language of all words in $\eta^{-1}(p)$ which admit an
$\eta$-factorization forest of height at most $h$ and idempotent height at
most $m$.

######  Proposition 8.12.

Let $h,m\in{\rm Nature}$ and $p=(s,V)\in P$ (i.e. $s\in M$ and $V$ a
$\sim_{\mathcal{D}}$-class). There exists a $PBPol(\mathcal{C})$-cover
$\mathbf{K}$ of $F^{\eta}(p,h,m)$ such that for any $K\in\mathbf{K}$, we have
$(s,\rho(K))\in S$.

Let us first use this result to prove Proposition 8.11 and finish the
completeness argument. Consider $s\in M$. Our objective is to build a
$PBPol(\mathcal{C})$-cover $\mathbf{K}_{s}$ of $\alpha^{-1}(s)$ such that,

$(s,\rho(K))\in S\quad\text{for all $K\in\mathbf{K}_{s}$}$

Let $h=m=3|P|-1$. We obtain the factorization forest theorem (i.e. Theorem
4.5) that for any $\sim_{\mathcal{D}}$-class $V$, we have
$\eta^{-1}((s,V))=F^{\eta}((s,V),h,m)$. Thus, for any
$\sim_{\mathcal{D}}$-class $V$, Proposition 8.12 yields a
$PBPol(\mathcal{C})$-cover $\mathbf{K}_{s,V}$ of $\eta^{-1}((s,V))$ such that
for any $K\in\mathbf{K}_{s,V}$, we have $(s,\rho(K))\in S$. Observe that by
definition of $\eta$, it is immediate that,

$\alpha^{-1}(s)=\bigcup_{V\in{A^{*}}/{\sim_{\mathcal{D}}}}\eta^{-1}((s,V))$

Therefore, it suffices to define $\mathbf{K}_{s}$ as the union of all sets
$\mathbf{K}_{s,V}$ where $V$ is some $\sim_{\mathcal{D}}$-class. It is
immediate by definition that $\mathbf{K}_{s}$ is a $PBPol(\mathcal{C})$-cover
of $\alpha^{-1}(s)$ and that $(s,\rho(K))\in S$ for all $K\in\mathbf{K}_{s}$.
This concludes the proof of Proposition 8.11.

It now remains to prove Proposition 8.12. Let $h,m\in{\rm Nature}$ and
$p=(s,V)\in P$. Our objective is to build a $PBPol(\mathcal{C})$-cover
$\mathbf{K}$ of $F^{\eta}(p,h,m)$ which satisfies the following property:

$\text{For all $K\in\mathbf{K}$,}\quad(s,\rho(K))\in S$ (2)

We proceed by induction on _two_ parameters which are listed below by order of
importance:

  1. (1)

The idempotent height $m$.

  2. (2)

The height $h$.

We start with the induction base: $h=0$. Let us point out that for this case,
the argument is actually slightly simpler than what we did for the
corresponding case in the ${Pol\/}(\mathcal{C})$ proof. This is because
$PBPol(\mathcal{C})$ always contains all finite languages (this may or may not
be the case for ${Pol\/}(\mathcal{C})$ depending on the finite quotienting
Boolean algebra $\mathcal{C}$).

Base case: Leaves. Assume that $h=0$. All words in $F^{\eta}(p,0,m)$ are
either empty or made of a single letter $a\in A$. In particular
$F^{\eta}(p,0,m)$ is a _finite language_. Thus, the following set $\mathbf{K}$
is finite:

$\mathbf{K}=\\{\\{w\\}\mid w\in F^{\eta}(p,0,m)\\}$

Clearly, $\mathbf{K}$ is a finite cover of $F^{\eta}(p,0,m)$. Moreover, it is
also a $PBPol(\mathcal{C})$-cover since $PBPol(\mathcal{C})$ contains all
finite languages (see Lemma 3.4). It remains to show that (2) is satisfied.

Let $K\in\mathbf{K}$. We show that $(s,\rho(K))\in S$. Since $K\in\mathbf{K}$,
we know that $K=\\{w\\}$ for some $w\in F^{\eta}(p,0,m)$. In particular, we
have $\eta(w)=p$ which means that $\alpha(w)=s$ by definition of $\eta$ since
$p=(s,V)$. Thus, we have,

$(s,\rho(K))=(\alpha(w),\rho(w))\in\mathcal{P}_{\mathit{triv}}[\alpha,\rho]$

This concludes the proof. Indeed, we know that $S$ is
$PBPol(\mathcal{C})$-saturated which means that
$\mathcal{P}_{\mathit{triv}}[\alpha,\rho]\subseteq S$ by definition.

Inductive case. We now assume that $h\geq 1$. Recall that our objective is to
build a $PBPol(\mathcal{C})$-cover $\mathbf{K}$ of $F^{\eta}(p,h,m)$ which
satisfies (2). We decompose $F^{\eta}(p,h,m)$ as the union of three languages
that we cover independently.

Recall that $F^{\eta}_{B}(p,h,m)$ (resp. $F^{\eta}_{I}(p,h,m)$) denotes the
language of all nonempty words in $\eta^{-1}(p)$ which admit an
$\eta$-factorization forest of height at most $h$, of idempotent height at
most $m$ and whose root is a _binary node_ (resp. _idempotent node_). The
construction is based on the two following lemmas.

######  Lemma 8.13.

There exists a $PBPol(\mathcal{C})$-cover $\mathbf{K}_{B}$ of
$F^{\eta}_{B}(p,h,m)$ such that for all $K\in\mathbf{K}_{B}$, we have
$(s,\rho(K))\in S$.

######  Lemma 8.14.

There exists a $PBPol(\mathcal{C})$-cover $\mathbf{K}_{I}$ of
$F^{\eta}_{I}(p,h,m)$ such that for all $K\in\mathbf{K}_{I}$, we have
$(s,\rho(K))\in S$.

Before we show these two results, let us use them to finish the proof. Let
$\mathbf{K}_{B}$ and $\mathbf{K}_{I}$ be as defined in the lemmas. By Fact
4.4, $F^{\eta}(p,h,m)$ is equal to the following union:

$F^{\eta}(p,h,m)=F^{\eta}_{B}(p,h,m)\cup F^{\eta}_{I}(p,h,m)\cup
F^{\eta}(p,0,0)$

Moreover, since $h\geq 1$, induction on $h$ in Proposition 8.12 yields a
$PBPol(\mathcal{C})$-cover $\mathbf{K}^{\prime}$ of $F^{\eta}(p,0,0)$ such
that for all $K\in\mathbf{K}^{\prime}$, we have $(s,\rho(K))\in S$. Thus, it
suffices to define
$\mathbf{K}=\mathbf{K}_{B}\cup\mathbf{K}_{I}\cup\mathbf{K}^{\prime}$. By
definition, we know that $\mathbf{K}$ is a $PBPol(\mathcal{C})$-cover of
$F^{\eta}(p,h,m)$ which satisfies (2).

It remains to prove the two lemmas. We start with Lemma 8.13 which is simpler.
The argument is essentially identical to the one we used when proving the
corresponding result for ${Pol\/}(\mathcal{C})$ in Section 6.

###  8.4. Proof of Lemma 8.13

For all $q\in P$, consider the language $F^{\eta}(q,h-1,m)$. Using induction
on our second parameter (the height $h$), we get that for all $q=(t,W)\in P$
(i.e. $t\in M$ and $W$ is a $\sim_{\mathcal{D}}$-class), there exists a
$PBPol(\mathcal{C})$-cover $\mathbf{U}_{q}$ of $F^{\eta}(q,h-1,m)$ such that
for any $U\in\mathbf{U}_{q}$, we have $(t,\rho(U))\in S$. Consider the
following set:

$\mathbf{K}_{B}=\\{K_{1}K_{2}\mid\text{there exists $q_{1},q_{2}\in P$ such
that $p=q_{1}q_{2}$, $K_{1}\in\mathbf{U}_{q_{1}}$ and
$K_{2}\in\mathbf{U}_{q_{2}}$}\\}$

One may now verify that $\mathbf{K}_{B}$ is a $PBPol(\mathcal{C})$-cover of
$F_{B}^{\eta}(p,h,m)$ and that $(s,\rho(K))\in S$ for $K\in\mathbf{K}_{B}$.
The proof is left to the reader as it is identical to that of Lemma 6.11 in
Section 6. In particular, when proving that $(s,\rho(K))\in S$ for
$K\in\mathbf{K}_{B}$, one uses the fact that $S$ is
$PBPol(\mathcal{C})$-saturated (specifically closure under multiplication).

###  8.5. Proof of Lemma 8.14

We turn to Lemma 8.14. The proof is more involved. In particular, let us point
out that this is where we finally use the preliminary results that we obtained
in Steps 1 and 2 (i.e. the multiplicative rating map $\gamma$ and Lemma 8.9).

Our objective is to construct a $PBPol(\mathcal{C})$-cover $\mathbf{K}_{I}$ of
$F_{I}^{\eta}(p,h,m)$ such that for all $K\in\mathbf{K}_{I}$, we have
$(s,\rho(K))\in S$. Note that we may assume without loss of generality that
$m\geq 1$ and $p$ is an idempotent of $P$. Indeed, otherwise we have
$F_{I}^{\eta}(p,h,m)=\emptyset$ and we may simply choose
$\mathbf{K}_{I}=\emptyset$. Note that since we have $p=(s,V)$, this means that
$s$ is an idempotent of $M$ and $V$ is an idempotent of
${A^{*}}/{\sim_{\mathcal{D}}}$.

In the sequel, we shall mostly use the hypothesis that $s\in M$ is idempotent.
Hence, we rename it $e$ to underline this hypothesis: we want to build a
$PBPol(\mathcal{C})$-cover $\mathbf{K}_{I}$ of $F_{I}^{\eta}(p,h,m)$ (with
$p=(e,V)$) such that for all $K\in\mathbf{K}_{I}$, we have $(e,\rho(K))\in S$.

This proof is where the argument departs from what we did for
${Pol\/}(\mathcal{C})$ in Section 6. On one hand, the construction itself
remains similar: it is still based on Lemma 6.2. However, there is a subtle
difference and more importantly, showing that $(e,\rho(K))\in S$ for all
$K\in\mathbf{K}_{I}$ is much more involved (this is where we shall need to use
induction on the idempotent height $m$ and the work we did in Steps 1 and 2).

Recall that applying Lemma 6.2 requires a cover $\mathbf{U}$ of
$F^{\eta}(p,h-1,m-1)$ and a language containing $\eta^{-1}(p)$. We first
define these two objects. We define $\mathbf{U}$ as an optimal
$PBPol(\mathcal{C})$-cover of $F^{\eta}(p,h-1,m-1)$. Moreover, recall
$p=(e,V)$ where $V$ is a $\sim_{\mathcal{D}}$-class. Clearly, we have
$\eta^{-1}(p)\subseteq V$ by definition of $\eta$.

######  Remark 8.15.

There is a subtle but crucial difference with what we did for
${Pol\/}(\mathcal{C})$. The $PBPol(\mathcal{C})$-cover $\mathbf{U}$ is not
obtained from induction. Instead, it is an arbitrary optimal
$PBPol(\mathcal{C})$-cover of $F^{\eta}(p,h-1,m-1)$. We shall use induction
later for a different purpose.

Before, we use $\mathbf{U}$ and $V$ together with Lemma 6.2 to build our
$PBPol(\mathcal{C})$-cover $\mathbf{K}_{I}$ of $F^{\eta}_{I}(p,h,m)$, let us
present two important properties of these objects that we shall need later.
Both are obtained by induction in Proposition 8.12. The first one involves
$\mathbf{U}$ only.

######  Lemma 8.16.

For any $n\geq 1$, $U_{1},\dots,U_{n}\in\mathbf{U}$, we have
$(e,\rho(U_{1}\cdots U_{n}))\in S$.

######  Proof 8.17.

We start by handling the special case when $n=1$ and then use it to treat the
general case. Consider $U\in\mathbf{U}$. We show that $(e,\rho(U))\in S$.
Using induction in Proposition 8.12 (the induction parameter that we use here
is unimportant since both $h$ and $m$ have decreased), we get a
$PBPol(\mathcal{C})$-cover $\mathbf{U}^{\prime}$ of $F^{\eta}(p,h-1,m-1)$ such
that $(e,\rho(U^{\prime}))\in S$ for any $U^{\prime}\in\mathbf{U}^{\prime}$.
Since $\mathbf{U}$ is an optimal $PBPol(\mathcal{C})$-cover of
$F^{\eta}(p,h-1,m-1)$ by definition, we have,

Moreover, since $U\in\mathbf{U}$, we have $\rho(U)\in$ and therefore,
$\rho(U)\in$ by the above inclusion. This yields
$U^{\prime}\in\mathbf{U}^{\prime}$ such that $\rho(U)\leq\rho(U^{\prime})$.
Finally, by definition of $\mathbf{U}^{\prime}$, we have
$(e,\rho(U^{\prime}))\in S$. Thus, since $S$ is $PBPol(\mathcal{C})$-saturated
and therefore closed under downset, this yields $(e,\rho(U))\in S$ as desired.

It remains to treat the general case. We consider
$U_{1},\dots,U_{n}\in\mathbf{U}$. By the special case treated above, we
already know that for all $i\leq n$, we have $(e,\rho(U_{i}))\in S$.
Therefore, since $S$ is $PBPol(\mathcal{C})$-saturated and $e$ is idempotent,
we obtain from closure under multiplication that,

$(e,\rho(U_{1}\cdots U_{n}))=(e^{n},\rho(U_{1})\cdots\rho(U_{n}))\in S$

This concludes the proof of Lemma 8.16.

Moreover, we have the following additional property of $\mathbf{U}$ and $V$
which is where we need induction on the idempotent height $m$ in Proposition
8.12 and the machinery introduced in Step 1 and 2 (i.e. the multiplicative
rating map $\gamma$ and Lemma 8.9). Moreover, this is also where $\rho$ being
nice is important.

######  Lemma 8.18.

Let $U_{1},\dots,U_{n}\in\mathbf{U}$ such that $\rho(U_{1}\cdots U_{n})$ is an
idempotent $f$ of $R$. We have,

$(e,f\cdot\rho(V)\cdot f)\in S$

The proof of Lemma 8.18 is quite involved. Thus, we postpone it to the end of
our argument. Let us first use $\mathbf{U}$ and $V$ to build our
$PBPol(\mathcal{C})$-cover of $F_{I}^{\eta}(p,h,m)$ and finish the proof of
Lemma 8.14.

We apply Lemma 6.2 together with our $PBPol(\mathcal{C})$-cover $\mathbf{U}$
of $F^{\eta}(p,h-1,m-1)$ and $V$ which contains $\eta^{-1}(p)$. This yields a
cover $\mathbf{K}_{I}$ of $F_{I}^{\eta}(p,h,m)$ such that any
$K\in\mathbf{K}_{I}$ is a concatenation $K=K_{1}\cdots K_{n}$ where each
$K_{i}$ is of one of the two following kinds:

  1. (1)

$K_{i}$ is a language in $\mathbf{U}$, or,

  2. (2)

$K_{i}=U_{1}\cdots U_{\ell}VU^{\prime}_{1}\cdots U^{\prime}_{\ell^{\prime}}$
where
$U_{1},\cdots,U_{\ell},U^{\prime}_{1},\dots,U^{\prime}_{\ell^{\prime}}\in\mathbf{U}$
and there exists an _idempotent_ $f\in R$ such that $\rho(U_{1}\cdots
U_{\ell})=\rho(U^{\prime}_{1}\cdots U^{\prime}_{\ell^{\prime}})=f$.

Clearly, any $K\in\mathbf{K}_{I}$ belongs to $PBPol(\mathcal{C})$. Indeed, $K$
is a concatenation of languages in $PBPol(\mathcal{C})$ by definition ($V\in
PBPol(\mathcal{C})$ by Fact 3 since it is $\sim_{\mathcal{D}}$-class) and
$PBPol(\mathcal{C})$ is closed under concatenation by Theorem 3.2. Thus,
$\mathbf{K}_{I}$ is a $PBPol(\mathcal{C})$-cover of $F^{\eta}_{I}(p,h,m)$.

It remains to prove that for any $K\in\mathbf{K}_{I}$, we have $(e,\rho(K))\in
S$. This is where we use Lemmas 8.16 and 8.18. Let $K\in\mathbf{K}_{I}$, by
definition we have $K=K_{1}\cdots K_{n}$ where all languages $K_{i}$ are as
described in the two items above. Observe that for all $i\leq n$, we have
$(e,\rho(K_{i}))\in S$. If $K_{i}$ is as described in the first item
($K_{i}\in\mathbf{U}$), this is by Lemma 8.16. Otherwise, when $K_{i}$ is as
described in the second item, this is by Lemma 8.18. Therefore, since $S$ is
$PBPol(\mathcal{C})$-saturated and $e$ is idempotent, we get from closure
under multiplication that,

$(e,\rho(K))=(e^{n},\rho(K_{1})\cdots\rho(K_{n}))\in S$

This concludes the proof of Lemma 8.14. It remains to show Lemma 8.18.

###  8.6. Proof of Lemma 8.18

Let $U_{1},\dots,U_{n}\in\mathbf{U}$ such that $\rho(U_{1}\cdots U_{n})$ is an
idempotent $f$ of $R$. We have to show that,

$(e,f\cdot\rho(V)\cdot f)\in S$

This is where we use induction on the idempotent height $m$ and the
preliminary results that we obtained in Steps 1 and 2 (specifically, we rely
on the multiplicative rating map $\gamma$ and Lemma 8.9). More precisely,
proving that $(e,f\cdot\rho(V)\cdot f)\in S$ is achieved using
$PBPol(\mathcal{C})$-closure. Applying this operation requires elements within
the set $\mathcal{T}$ such that $(S,\mathcal{T})$ is
$PBPol(\mathcal{C})$-saturated. In Lemma 8.19 below, we use induction on $m$
to prove the existence of specific elements in $S$. This gives us more
information on $\gamma$ (since its definition depends on $S$). Together with
Lemma 8.9, this information on $\gamma$ allows us to exhibit the right
elements in $\mathcal{T}$ to apply $PBPol(\mathcal{C})$-closure for proving
that $(e,f\cdot\rho(V)\cdot f)\in S$.

######  Lemma 8.19.

We have $(e,f)\in\gamma(V)$.

Before we prove Lemma 8.19, let us show that $(e,f\cdot\rho(V)\cdot f)\in S$
using $PBPol(\mathcal{C})$-closure. This is where we use the hypothesis that
$\rho$ is nice. It implies that we have words $v_{1},\dots,v_{\ell}\in V$ such
that, $\rho(v_{1})+\cdots+\rho(v_{\ell})=\rho(V)$.

For all $i\leq\ell$, we let $r_{i}=\rho(v_{i})$. Consequently, we have
$\rho(V)=r_{1}+\cdots+r_{\ell}$. Since all words $v_{i}$ belong to the
$\sim_{\mathcal{D}}$-class $V$ by definition, it follows from Lemma 8.9 that
for all $i\leq\ell$, we have,

$(r_{i},\gamma(V))\in\mathcal{T}$

Moreover, we have $(e,f)\in\gamma(V)$ by Lemma 8.19. Therefore, we may use the
hypothesis that $(S,\mathcal{T})$ is $PBPol(\mathcal{C})$-saturated to apply
$PBPol(\mathcal{C})$-closure (i.e. Operation (3)) for each $i\leq\ell$ which
yields that,

$(e,f\cdot(r_{i}+\rho(\varepsilon))\cdot f)\in S$

Since $e$ is idempotent, we may now use closure under multiplication to
obtain,

$\left(e,\prod_{1\leq i\leq\ell}f\cdot(r_{i}+\rho(\varepsilon))\cdot
f\right)\in S$

Recall that by hypothesis, we have $f=\rho(U_{1}\dots U_{n})$. Thus, we have
$\rho(\varepsilon)\cdot f=f\cdot\rho(\varepsilon)=f$. We may now distribute
the multiplication in the right component to obtain that,

$f\cdot\left(r_{1}+\cdots+r_{\ell}\right)\cdot f\leq\prod_{1\leq
i\leq\ell}\left(f\cdot(r_{i}+\rho(\varepsilon))\cdot f\right)$

Since $r_{1}+\cdots+r_{\ell}=\rho(V)$, the above can be rewritten as follows,

$f\cdot\rho(V)\cdot f\leq\prod_{1\leq
i\leq\ell}\left(f\cdot(r_{i}+\rho(\varepsilon))\cdot f\right)$

Combined with closure under downset, this yields as desired that,

$(e,f\cdot\rho(V)\cdot f)\in S$

This concludes the proof of Lemma 8.18. It remains to prove Lemma 8.19.

######  Proof 8.20 (Proof of Lemma 8.19).

Our objective is to show that $(e,f)\in\gamma(V)$. Recall that by definition
of $\gamma$, we have,

$\gamma(V)=\\{(s,r)\mid\text{$(s,r)\in\tau(V\cap G)$ for some good language
$G$}\\}$

Therefore, we must exhibit some good language $G\subseteq A^{*}$ such that
$(e,f)\in\tau(V\cap G)$.

Recall that $f=\rho(U_{1}\cdots U_{n})$ for $U_{1},\dots,U_{n}\in\mathbf{U}$.
We define $G$ as the language of all words which are an infix of some other
word in $F^{\eta}(p,h+n-2,m-1)$. It now remains to show that $G$ is indeed
good and that $(e,f)\in\tau(V\cap G)$. The two proofs are independent.

First property: $G$ is good. We have to show that $G$ is closed under infixes
and $\tau(G)\subseteq S$. The former is immediate by definition of $G$.
Therefore, we may concentrate on the latter: $\tau(G)\subseteq S$. This is
where we need induction on the idempotent height $m$ in Proposition 8.12.

By definition, all words in $G$ are an infix of some other word admitting an
$\eta$-factorization forest of height at most $h+n-2$ and of idempotent height
at most $m-1$. Therefore, it follows from Proposition 4.6 that all words in
$G$ admit an $\eta$-factorization forest of height at most $h+n$ and
idempotent height at most $m-1$. Thus, we have,

$G\subseteq\bigcup_{q\in P}F^{\eta}(q,h+n,m-1)$

Since $\tau$ is a multiplicative rating map (whose evaluation hemiring
$2^{M\times R}$ uses union as addition), it follows that,

$\tau(G)\subseteq\bigcup_{q\in P}\tau(F^{\eta}(q,h+n,m-1))$

Therefore, it suffices to show that for all $q\in P$, we have
$\tau(F^{\eta}(q,h+n,m-1))\subseteq S$. Let $q\in P$, we have $q=(t,W)$ with
$t\in M$ and $W$ a $\sim_{\mathcal{D}}$-class. Consider
$(s,r)\in\tau(F^{\eta}(q,h+n,m-1))$. We show that $(s,r)\in S$. By definition
of $\tau$, we have,

$r\in\mathcal{I}_{PBPol(\mathcal{C})}[F^{\eta}(q,h+n,m-1)\cap\alpha^{-1}(s),\rho]$

This implies that $F^{\eta}(q,h+n,m-1)\cap\alpha^{-1}(s)\neq\emptyset$. Since
$F^{\eta}(q,h+n,m-1)\subseteq\eta^{-1}(q)$ which is itself a subset of
$\alpha^{-1}(t)$ by definition of $\eta$, this implies that $s=t$.
Consequently, we have $F^{\eta}(q,h+n,m-1)\subseteq\alpha^{-1}(s)$.
Altogether, we obtain,

$r\in\mathcal{I}_{PBPol(\mathcal{C})}[F^{\eta}(q,h+n,m-1),\rho]$

Using induction on the idempotent height $m$ in Proposition 8.12 (our most
important parameter), we get a $PBPol(\mathcal{C})$-cover
$\mathbf{K}^{\prime}$ of $F^{\eta}(q,h+n,m-1)$ such that
$(s,\rho(K^{\prime}))\in S$ for any $K^{\prime}\in\mathbf{K}^{\prime}$ (recall
that $q=(t,W)$ and $t=s$). Since $\mathbf{K}^{\prime}$ is a
$PBPol(\mathcal{C})$-cover of $F^{\eta}(q,h+n,m-1)$,

$\mathcal{I}_{PBPol(\mathcal{C})}[F^{\eta}(q,h+n,m-1),\rho]\subseteq$

Therefore, we have $r\in$ and we obtain $K^{\prime}\in\mathbf{K}^{\prime}$
such that $r\leq\rho(K^{\prime})$. Finally, since $(s,\rho(K^{\prime}))\in S$
by definition of $\mathbf{K}^{\prime}$ and $S$ is
$PBPol(\mathcal{C})$-saturated, closure under downset yields $(s,r)\in S$.

Second property: $(e,f)\in\tau(V\cap G)$. Recall that $f=\rho(U_{1}\cdots
U_{n})$ where $U_{1},\dots,U_{n}\in\mathbf{U}$. Moreover, by definition,
$\mathbf{U}$ is an optimal $PBPol(\mathcal{C})$-cover of $F^{\eta}(p,h-1,m-1)$
(for $\rho$). Therefore, we know that for all $i\leq n$, we have,

$\rho(U_{i})\in\mathcal{I}_{PBPol(\mathcal{C})}[F^{\eta}(p,h-1,m-1),\rho]$

Moreover, since $p=(e,V)$, we have
$F^{\eta}(p,h-1,m-1)\subseteq\eta^{-1}(p)\subseteq\alpha^{-1}(e)$ which means
that $F^{\eta}(p,h-1,m-1)\cap\alpha^{-1}(e)=F^{\eta}(p,h-1,m-1)$. Thus, for
all $i\leq n$, we have,

$\rho(U_{i})\in\mathcal{I}_{PBPol(\mathcal{C})}[F^{\eta}(p,h-1,m-1)\cap\alpha^{-1}(e),\rho]$

By definition of $\tau$, this exactly says that for all $i\leq n$,

$(e,\rho(U_{i}))\in\tau(F^{\eta}(p,h-1,m-1))$

Therefore, since $e$ is an idempotent of $M$ and $f=\rho(U_{1}\cdots U_{n})$,
we may use the fact that $\tau$ is a morphism to get,

$(e,f)=(e^{n},\rho(U_{1}\cdots U_{n}))\in\tau((F^{\eta}(p,h-1,m-1))^{n})$

We now prove that $(F^{\eta}(p,h-1,m-1))^{n}\subseteq V\cap G$. By definition
of rating maps, it will then follow that
$\tau((F^{\eta}(p,h-1,m-1))^{n})\subseteq\tau(V\cap G)$. This implies as
desired that $(e,f)\in\tau(V\cap G)$.

Let $w\in(F^{\eta}(p,h-1,m-1))^{n}$. By definition, $w=w_{1}\cdots w_{n}$ with
$w_{i}\in F^{\eta}(p,h-1,m-1)$ for all $i$. In particular $\eta(w_{i})=p$ for
all $i$ and since $p$ is idempotent, this yields $\eta(w)=p=(e,V)$.
Consequently, $[w]_{\mathcal{D}}=V$ by definition of $\eta$ and we get that
$w\in V$. It remains to show that $w\in G$. Since all words $w_{i}$ belong to
$F^{\eta}(p,h-1,m-1)$, they admit $\eta$-factorization forests of height at
most $h-1$ and idempotent height at most $m-1$. Therefore $w=w_{1}\cdots
w_{n}$ admits an $\eta$-factorization forest of height at most $h-1+n-1$ and
idempotent height at most $m-1$. Indeed, it suffices to combine the forests of
the factors $w_{i}$ with binary nodes. This means that $w\in
F^{\eta}(p,h+n-2,m-1)$. Hence, by definition of $G$, we have $w\in G$. This
concludes the proof that $(e,f)\in\tau(V\cap G)$ and that of Lemma 8.19.

##  9\. Conclusion

We showed that the separation and covering problems are decidable for all
classes of the form ${Pol\/}(\mathcal{C})$ and $PBPol(\mathcal{C})$ where
$\mathcal{C}$ is an arbitrary finite quotienting Boolean algebra. As we
explained, these results have important consequences for the quantifier
alternation hierarchies within first-order logic overs words: we get that
separation and covering are decidable for the level $\Sigma_{3}(<)$. This
result may be lifted to the stronger logic
$\Sigma_{3}(<,+1,min,max,\varepsilon)$ with a transfer result of [PZ15a].
Finally, one also gets that the membership problem is decidable for
$\Sigma_{4}(<)$ and $\Sigma_{4}(<,+1,min,max,\varepsilon)$ using a reduction
theorem of [PZ14].

Let us point out that while this is not apparent in the above summary, we
still know more about ${Pol\/}(\mathcal{C})$ than we do about
$PBPol(\mathcal{C})$. Indeed, our ${Pol\/}(\mathcal{C})$-covering algorithm is
based on a characterization of _${Pol\/}(\mathcal{C})$ -optimal pointed
imprints_ which holds for any multiplicative rating map. This result is
stronger than the decidability of ${Pol\/}(\mathcal{C})$-covering (one only
needs to consider nice multiplicative rating maps for this). Moreover, the
fact that we have this stronger result is precisely why we are able to handle
the larger class $PBPol(\mathcal{C})$. On the other hand, while we also have a
characterization of $PBPol(\mathcal{C})$-optimal pointed imprints, it only
holds for nice multiplicative rating maps. Therefore, a natural next move is
trying to generalize this characterization to all _all_ multiplicative rating
maps. Indeed, such a result could be the key to solving covering for one more
level in concatenation hierarchies.

Another interesting (and much simpler) objective is analyzing the complexity
of the decision problems that we have just solved. Naturally, this depends on
the finite quotienting Boolean algebra $\mathcal{C}$ for both
${Pol\/}(\mathcal{C})$ and $PBPol(\mathcal{C})$. We leave this for further
work.

## References

  * [Arf87] Mustapha Arfi.  Polynomial operations on rational languages.  In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS’87, pages 198–206, 1987.
  * [BC71] Janusz A. Brzozowski and Rina S. Cohen.  Dot-depth of star-free events.  Journal of Computer and System Sciences, 5(1):1–16, 1971.
  * [BK78] Janusz A. Brzozowski and Robert Knast.  The dot-depth hierarchy of star-free languages is infinite.  Journal of Computer and System Sciences, 16(1):37–55, 1978.
  * [Boj09] Mikołaj Bojańczyk.  Factorization forests.  In Proceedings of the 13th International Conference on Developments in Language Theory, DLT’09, pages 1–17, 2009.
  * [CMM13] Wojciech Czerwiński, Wim Martens, and Tomáš Masopust.  Efficient separability of regular languages by subsequences and suffixes.  In Proceedings of the 40th International Colloquium on Automata, Languages, and Programming, ICALP’13, pages 150–161, 2013.
  * [Col10] Thomas Colcombet.  Factorization forests for infinite words and applications to countable scattered linear orderings.  Theoritical Computer Science, 411(4-5):751–764, 2010.
  * [DGK08] Volker Diekert, Paul Gastin, and Manfred Kufleitner.  A survey on small fragments of first-order logic over finite words.  International Journal on Foundations of Computer Science, 19(3), 2008.
  * [GS00] Christian Glaßer and Heinz Schmitz.  Languages of dot-depth 3/2.  In Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, (STACS’00), pages 555–566, 2000.
  * [Kna83] Robert Knast.  A semigroup characterization of dot-depth one languages.  RAIRO - Theoretical Informatics and Applications, 17(4):321–330, 1983.
  * [Kuf08] Manfred Kufleitner.  The height of factorization forests.  In Proceedings of the 33rd International Symposium on Mathematical Foundations of Computer Science, MFCS’08, pages 443–454, 2008.
  * [MP71] Robert McNaughton and Seymour A. Papert.  Counter-Free Automata.  MIT Press, 1971.
  * [Pin98] Jean-Éric Pin.  Bridges for concatenation hierarchies.  In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, ICALP’98, pages 431–442, 1998.
  * [Pin17] Jean-Éric Pin.  The dot-depth hierarchy, 45 years later.  In The Role of Theory in Computer Science. Essays Dedicated to Janusz Brzozowski. World Scientific, 2017.
  * [Pla15] Thomas Place.  Separating regular languages with two quantifiers alternations.  In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’15, pages 202–213. IEEE Computer Society, 2015.
  * [PP86] Dominique Perrin and Jean-Éric Pin.  First-order logic and star-free sets.  Journal of Computer and System Sciences, 32(3):393–406, 1986.
  * [PS85] Jean-Éric Pin and Howard Straubing.  Monoids of upper triangular boolean matrices.  In Semigroups. Structure and Universal Algebraic Problems, volume 39, pages 259–272. North-Holland, 1985.
  * [PvRZ13] Thomas Place, Lorijn van Rooijen, and Marc Zeitoun.  Separating regular languages by piecewise testable and unambiguous languages.  In Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS’13, pages 729–740, 2013.
  * [PW97] Jean-Éric Pin and Pascal Weil.  Polynomial closure and unambiguous product.  Theory of Computing Systems, 30(4):383–422, 1997.
  * [PZ14] Thomas Place and Marc Zeitoun.  Going higher in the first-order quantifier alternation hierarchy on words.  In Proceedings of the 41st International Colloquium on Automata, Languages, and Programming, ICALP’14, pages 342–353, 2014.
  * [PZ15a] Thomas Place and Marc Zeitoun.  Separation and the successor relation.  In 32nd International Symposium on Theoretical Aspects of Computer Science, STACS’15, pages 662–675, 2015.
  * [PZ15b] Thomas Place and Marc Zeitoun.  The tale of the quantifier alternation hierarchy of first-order logic over words.  SIGLOG news, 2(3):4–17, 2015.
  * [PZ16] Thomas Place and Marc Zeitoun.  The covering problem: A unified approach for investigating the expressive power of logics.  In Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science, MFCS’16, 2016.
  * [PZ17a] Thomas Place and Marc Zeitoun.  Adding successor: A transfer theorem for separation and covering.  Unpublished, a preliminary version can be found at https://arxiv.org/abs/1709.10052, 2017\.
  * [PZ17b] Thomas Place and Marc Zeitoun.  Concatenation hierarchies: New bottle, old wine.  In 12th International Computer Science Symposium in Russia, CSR’17, pages 25–37, 2017.
  * [PZ17c] Thomas Place and Marc Zeitoun.  Separation for dot-depth two.  In 32th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’17, 2017.
  * [PZ18a] Thomas Place and Marc Zeitoun.  The covering problem.  Logical Methods in Computer Science, 14(3), 2018.
  * [PZ18b] Thomas Place and Marc Zeitoun.  Generic results for concatenation hierarchies.  Theory of Computing Systems (ToCS), 2018.  Selected papers from CSR’17.
  * [Sch65] Marcel Paul Schützenberger.  On finite monoids having only trivial subgroups.  Information and Control, 8(2):190–194, 1965.
  * [Sim75] Imre Simon.  Piecewise testable events.  In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pages 214–222, 1975.
  * [Sim90] Imre Simon.  Factorization forests of finite height.  Theoritical Computer Science, 72(1):65–94, 1990.
  * [Str81] Howard Straubing.  A generalization of the Schützenberger product of finite monoids.  Theoretical Computer Science, 13(2):137–150, 1981.
  * [Str85] Howard Straubing.  Finite semigroup varieties of the form V * D.  Journal of Pure and Applied Algebra, 1985.
  * [Str88] Howard Straubing.  Semigroups and languages of dot-depth two.  Theoretical Computer Science, 58(1–3):361–378, 1988.
  * [Thé81] Denis Thérien.  Classification of finite monoids: The language approach.  Theoretical Computer Science, 14(2):195–208, 1981.
  * [Tho82] Wolfgang Thomas.  Classifying regular events in symbolic logic.  Journal of Computer and System Sciences, 25(3):360–376, 1982.
  * [TW98] Denis Thérien and Thomas Wilke.  Over words, two variables are as powerful as one quantifier alternation.  In Proceedings of the 30th Annual ACM Symposium on Theory of Computing, STOC’98, pages 234–240, 1998.