$\begin{array}[]{rcll}\mathsf{labs}(R_{1}/(t^{\prime}/S))&=&\mathsf{labs}((R_{0}/S)/(t^{\prime}/S))&\text{
by definition of $R_{1}$}\\\
&=&\mathsf{labs}((R_{0}/t^{\prime})/(S/t^{\prime}))&\text{ by
Lem.~{}\ref{lemma:generalized_cube_lemma}}\\\
&=&\mathsf{labs}(R_{0}/t^{\prime})\setminus\mathsf{labs}(S/t^{\prime})&\text{
by Lem.~{}\ref{lemma:names_after_projection_along_a_step}}\\\
&=&\mathsf{labs}(R_{0}/t^{\prime})\end{array}$

For the last step, note that $\mathsf{labs}(R_{0}/t^{\prime})$ and
$\mathsf{labs}(S/t^{\prime})$ are disjoint, since $R_{0}\neq S$.

Applying the i.h., we obtain that $\\#(R_{0}/S\tau)=\\#(R_{1}/\tau)\leq 1$.

###### Lemma 39

Let $R$ be a step, let $\rho$ a coinitial derivation, and let
$t^{\prime}\mathrel{\ltimes}\mathsf{src}(R)$. Suppose that $R$ is not
$t^{\prime}$-garbage, and that $R/\rho_{1}$ is a singleton for every prefix
$\rho_{1}\sqsubseteq\rho$. Then $R/\rho$ is not $(t^{\prime}/\rho)$-garbage.

###### Proof

By induction on $\rho$. The base case, when $\rho=\epsilon$, is immediate
since we know that $R$ is not garbage. For the inductive step, suppose that
$\rho=S\sigma$. We know that $R/S$ is a singleton, so let $R_{1}=R/S$. Note
that $R_{1}/(t^{\prime}/S)=(R/S)/(t^{\prime}/S)=(R/t^{\prime})/(S/t^{\prime})$
by Lem. 4. We know that $R/t^{\prime}$ is non-empty, because $R$ is not
garbage. Moreover, $\mathsf{labs}(R/t^{\prime})$ and
$\mathsf{labs}(S/t^{\prime})$ are disjoint since $R\neq S$. So
$\\#\mathsf{labs}((R/t^{\prime})/(S/t^{\prime}))=\mathsf{labs}(R/t^{\prime})$
by Lem. 18. This means that the set $R_{1}/(t^{\prime}/S)$ is non-empty, so
$R_{1}$ is not $(t^{\prime}/S)$-garbage . By i.h. we obtain that
$R_{1}/\sigma$ is not $((t^{\prime}/S)/\sigma)$-garbage, which means that
$(R/S\sigma)/(t^{\prime}/S\sigma)\neq\varnothing$, i.e. that $R/S\sigma$ is
not garbage, as required. To be able to apply the i.h., observe that if
$\sigma_{1}$ is a prefix of $\sigma$, then $S\sigma_{1}$ is a prefix of
$\rho$, so the fact that $R$ has a single residual after $S\sigma_{1}$ implies
that the step $R_{1}=R/S$ has a single residual after $\sigma_{1}$.

######  Proposition 14 (Characterization of garbage-free derivations)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and
$t^{\prime}\mathrel{\ltimes}t$. The following are equivalent:

  1. 1.

$\rho$ is $t^{\prime}$-garbage-free.

  2. 2.

$\rho\equiv\rho\Downarrow t^{\prime}$.

  3. 3.

$\rho\equiv\sigma\Downarrow t^{\prime}$ for some derivation $\sigma$.

###### Proof

Let us prove $1\implies 2\implies 3\implies 1$:

  * •

$(1\implies 2)$ Suppose that $\rho$ is $t^{\prime}$-garbage-free, and let us
show that $\rho\equiv\rho\Downarrow t^{\prime}$ by induction on the length of
$\rho\Downarrow t^{\prime}$.

If there are no coarse steps for $(\rho,t^{\prime})$, By Prop. 13, any
derivation with no coarse steps is garbage. So $\rho$ is $t^{\prime}$-garbage.
Since $\rho$ is garbage-free, this means that $\rho=\epsilon$. Hence
$\rho=\epsilon=\rho\Downarrow t^{\prime}$, as required.

If there exists a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the
leftmost such step. Note that $\rho\equiv R_{0}(\rho/R_{0})$ since
$R_{0}\sqsubseteq\rho$. Moreover, we claim that $\rho/R_{0}$ is
$(t^{\prime}/R_{0})$-garbage-free. Let $\sigma\sqsubseteq\rho/R_{0}$ such that
$(\rho/R_{0})/\sigma$ is garbage with respect to the term
$(t^{\prime}/R_{0})/\sigma=t^{\prime}/R_{0}\sigma$, and let us show that
$(\rho/R_{0})/\sigma$ is empty. Note that:

$\begin{array}[]{rcll}R_{0}\sigma&\sqsubseteq&R_{0}(\rho/R_{0})&\text{since
$\sigma\sqsubseteq\rho/R_{0}$}\\\ &\equiv&\rho&\text{as already noted}\\\
\end{array}$

Moreover, we know that the derivation $\rho/R_{0}\sigma=(\rho/R_{0})/\sigma$
is $(t^{\prime}/R_{0}\sigma)$-garbage. So, given that $\rho$ is
$t^{\prime}$-garbage-free, we conclude that $\rho/R_{0}\sigma=\epsilon$, that
is $(\rho/R_{0})/\sigma=\epsilon$, which completes the proof of the claim that
$\rho/R_{0}$ is $(t^{\prime}/R_{0})$-garbage-free. We conclude as follows:

$\begin{array}[]{rcll}\rho&\equiv&R_{0}(\rho/R_{0})&\text{as already noted}\\\
&\equiv&R_{0}((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))&\text{by {\em i.h.}
since $\rho/R_{0}$ is $(t^{\prime}/R_{0})$-garbage-free}\\\
&\equiv&\rho\Downarrow t^{\prime}&\text{by definition of sieving}\\\
\end{array}$

  * •

$(2\implies 3)$ Obvious, taking $\sigma:=\rho$.

  * •

$(3\implies 1)$ Let $\rho\equiv\sigma\Downarrow t^{\prime}$. Let us show that
$\rho$ is garbage-free by induction on the length of $\sigma\Downarrow
t^{\prime}$.

If there are no coarse steps for $(\sigma,t^{\prime})$, then
$\rho\equiv\sigma\Downarrow t^{\prime}=\epsilon$, which means that
$\rho=\epsilon$. Observe that the empty derivation is trivially garbage-free.

If there exists a coarse step for $(\sigma,t^{\prime})$, let $R_{0}$ be the
leftmost such step. Then $\rho\equiv\sigma\Downarrow
t^{\prime}=R_{0}((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))$. To see that
$\rho$ is $t^{\prime}$-garbage-free, let $\tau\sqsubseteq\rho$ such that
$\rho/\tau$ is garbage, and let us show that $\rho/\tau$ is empty. We know
that $\rho/\tau$ is of the following form (modulo permutation equivalence):

$\rho/\tau\equiv\frac{R_{0}((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))}{\tau}=\left(\frac{R_{0}}{\tau}\right)\left(\frac{(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})}{\tau/R_{0}}\right)$

That is, we know that the following derivation is $(t^{\prime}/\tau)$-garbage,
and it suffices to show that it is empty:

$\left(\frac{R_{0}}{\tau}\right)\left(\frac{(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})}{\tau/R_{0}}\right)$

Recall that, in general, $AB$ is garbage if and only if $A$ and $B$ are
garbage (Prop. 9). Similarly, $AB$ is empty if and only if $A$ and $B$ are
empty. So it suffices to prove the two following implications:

$\begin{array}[]{clll}{\bf(A)}&\text{ If }&R_{0}/\tau\text{ is
garbage,}&\text{ then it is empty.}\\\ {\bf(B)}&\text{ If
}&((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))/(\tau/R_{0})\text{ is
garbage,}&\text{ then it is empty.}\end{array}$

Let us check that each implication holds:

    * –

(A) Suppose that $R_{0}/\tau$ is $(t^{\prime}/\tau)$-garbage, and let us show
that $R_{0}/\tau$ is empty. Knowing that the derivation $R_{0}/\tau$ is
garbage means that $(R_{0}/\tau)/(t^{\prime}/\tau)=\varnothing$. Since $R_{0}$
is the leftmost step coarse for $(\sigma,t^{\prime})$, by Lem. 38 we have that
$\\#(R_{0}/\tau)\leq 1$. If $R_{0}/\tau$ is empty we are done, since this is
what we wanted to prove.

The remaining possibility is that $R_{0}/\tau$ be a singleton. We argue that
this case is impossible. Note that for every prefix $\tau_{1}\sqsubseteq\tau$,
the set $R_{0}/\tau_{1}$ is also a singleton, since otherwise it would be
empty, as a consequence of Lem. 38. So we may apply Lem. 39 and conclude that,
since $R_{0}$ is not $t^{\prime}$-garbage then $R_{0}/\tau$ is not
$(t^{\prime}/\tau)$-garbage. This contradicts the hypothesis.

    * –

(B) Suppose that $((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))/(\tau/R_{0})$
is garbage with respect to the term $(t^{\prime}/R_{0})/(\tau/R_{0})$, and let
us show that it is empty. Since $(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$
is a shorter derivation than $\sigma\Downarrow t^{\prime}$, we may apply the
i.h. we obtain that $(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$ is
$(t^{\prime}/R_{0})$-garbage-free. Moreover, the following holds:

$\tau/R_{0}\sqsubseteq\rho/R_{0}\equiv(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$

So, by definition of $(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$ being
garbage-free, the fact that the derivation
$((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))/(\tau/R_{0})$ is garbage implies
that it is empty, as required.

######  Lemma 40 (The projection after a sieve is garbage)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and
$t^{\prime}\mathrel{\ltimes}t$. Then $\rho/(\rho\Downarrow t^{\prime})$ is
$(t^{\prime}/(\rho\Downarrow t^{\prime}))$-garbage.

###### Proof

By induction on the length of $\rho\Downarrow t^{\prime}$.

If there are no coarse steps for $(\rho,t^{\prime})$, then $\rho\Downarrow
t^{\prime}=\epsilon$. Moreover, by Prop. 13, a derivation with no coarse steps
is garbage. So $\rho/(\rho\Downarrow t^{\prime})=\rho$ is garbage, as
required.

If there exists a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the
leftmost such step, and let $\sigma=\rho/R_{0}$ and
$s^{\prime}=t^{\prime}/R_{0}$. Then:

$\begin{array}[]{rcll}\rho/(\rho\Downarrow
t^{\prime})&=&\rho/(R_{0}((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))&\text{ by
definition}\\\ &=&(\rho/R_{0})/((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))\\\
&=&\sigma/(\sigma\Downarrow s^{\prime})\\\ \end{array}$

By i.h., $\sigma/(\sigma\Downarrow s^{\prime})$ is
$(s^{\prime}/(\sigma\Downarrow s^{\prime}))$-garbage. That is:

$\frac{\sigma/(\sigma\Downarrow s^{\prime})}{s^{\prime}/(\sigma\Downarrow
s^{\prime})}=\epsilon$

Unfolding the definitions of $\sigma$ and $s^{\prime}$ we have that:

$\frac{(\rho/R_{0})/((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))}{(t^{\prime}/R_{0})/((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))}=\epsilon$

Equivalently:

$\frac{\rho/R_{0}((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))}{t^{\prime}/R_{0}((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))}=\epsilon$

Finally, by definition of sieve,

$\frac{\rho/(\rho\Downarrow t^{\prime})}{t^{\prime}/(\rho\Downarrow
t^{\prime})}=\epsilon$

which means that $\rho/(\rho\Downarrow t^{\prime})$ is
$(t^{\prime}/(\rho\Downarrow t^{\prime}))$-garbage, as required.

The proof of Prop. 10 is a consequence of the preceding results, namely:

  1. 1.

Proof that $\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free and
$\rho\Downarrow t^{\prime}\sqsubseteq\rho$.
Note that $\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free by Prop.
14. Moreover, $\rho\Downarrow t^{\prime}\sqsubseteq\rho$ by Lem. 35.

  2. 2.

Proof that $\rho/(\rho\Downarrow t^{\prime})$ is $(t^{\prime}/(\rho\Downarrow
t^{\prime}))$-garbage.
This is precisely Lem. 40.

  3. 3.

Proof that $\rho$ is $t^{\prime}$-garbage if and only if $\rho\Downarrow
t^{\prime}=\epsilon$.
An immediate consequence of Prop. 13.

  4. 4.

Proof that $\rho$ is $t^{\prime}$-garbage-free if and only if $\rho\Downarrow
t^{\prime}\equiv\rho$.
An immediate consequence of Prop. 14.

###  0.A.14 Proof of Prop. 11 – Semilattices of garbage-free and garbage
derivations

To prove Prop. 11 we need a few auxiliary lemmas:

###### Lemma 41

Let $\rho\equiv\sigma$. Then $\rho\Downarrow t^{\prime}=\sigma\Downarrow
t^{\prime}$.

###### Proof

Observe that, given two permutation equivalent derivations $\rho$ and
$\sigma$, a step $R$ is coarse for $(\rho,t^{\prime})$ if and only if $R$ is
coarse for $(\sigma,t^{\prime})$, since
$(R\sqsubseteq\rho)\iff(R/\rho=\varnothing)\iff(R/\sigma=\varnothing)\iff(R\sqsubseteq\sigma)$.
Using this observation, the proof is straightforward by induction on the
length of $\rho\Downarrow t^{\prime}$.

######  Lemma 42 (Sieving trailing garbage)

Let $\rho$ and $\sigma$ be composable derivations, and let
$t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)$. If $\sigma$ is
$(t^{\prime}/\rho)$-garbage, then $\rho\sigma\Downarrow
t^{\prime}=\rho\Downarrow t^{\prime}$.

###### Proof

By induction on the length of $\rho\Downarrow t^{\prime}$. If there are no
coarse steps for $(\rho,t^{\prime})$, then by Prop. 13, the derivation $\rho$
is $t^{\prime}$-garbage, so $\rho\sigma$ is $t^{\prime}$-garbage by Prop. 9.
Resorting to Prop. 13 we obtain that $\rho\sigma\Downarrow
t^{\prime}=\epsilon=\rho\Downarrow t^{\prime}$, as required.

If there exists a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the
leftmost such step. Then since $R_{0}\sqsubseteq\rho$ also
$R_{0}\sqsubseteq\rho\sigma$, so $R_{0}$ is a coarse step for
$(\rho\sigma,t^{\prime})$. In particular, since there exists at least one
coarse step for $(\rho\sigma,t^{\prime})$, let $S_{0}$ be the leftmost such
step. We argue that $R_{0}=S_{0}$. We consider two cases, depending on whether
$S_{0}$ is coarse for $(\rho,t^{\prime})$:

  1. 1.

If $S_{0}$ is coarse for $(\rho,t^{\prime})$. Then $R_{0}$ and $S_{0}$ are
both simultaneously coarse for $(\rho,t^{\prime})$ and for
$(\rho\sigma,t^{\prime})$. Note that $R_{0}$ cannot be to the left of $S_{0}$,
since then $S_{0}$ would not be the leftmost coarse step for
$(\rho\sigma,t^{\prime})$. Symmetrically, $S_{0}$ cannot be to the left of
$R_{0}$, since then $R_{0}$ would not be the leftmost coarse step for
$(\rho,t^{\prime})$. Hence $R_{0}=S_{0}$ as claimed.

  2. 2.

If $S_{0}$ is not coarse for $(\rho,t^{\prime})$. We argue that this case is
impossible. Note that $S_{0}\sqsubseteq\rho\sigma$ but it is not the case that
$S_{0}\sqsubseteq\rho$, so $S_{0}/\rho$ is not empty. Note also that
$S_{0}/\rho\sqsubseteq\sigma$, so by Coro. 2 we have that
$(S_{0}/\rho)/(t^{\prime}/\rho)\sqsubseteq\sigma/(t^{\prime}/\rho)$. Moreover,
$\sigma/(t^{\prime}/\rho)=\epsilon$ is empty because $\sigma$ is
$(t^{\prime}/\rho)$-garbage. This means that
$(S_{0}/\rho)/(t^{\prime}/\rho)=\epsilon$. Then we have the following chain of
equalities:

$\begin{array}[]{rcll}\varnothing&=&\mathsf{labs}((S_{0}/\rho)/(t^{\prime}/\rho))\\\
&=&\mathsf{labs}((S_{0}/t^{\prime})/(\rho/t^{\prime}))&\text{by
Coro.~{}\ref{coro:permutation_equivalence_in_terms_of_names} and
Lem.~{}\ref{lemma:generalized_cube_lemma}}\\\
&=&\mathsf{labs}(S_{0}/t^{\prime})\setminus\mathsf{labs}(\rho/t^{\prime})&\text{by
Lem.~{}\ref{lemma:names_after_projection_along_a_step}}\\\
&=&\mathsf{labs}(S_{0}/t^{\prime})\end{array}$

To justify the last step, start by noting that no residual of $S_{0}$ is
contracted along the derivation $\rho$. Indeed, if $S_{0}$ had a residual,
then $\rho=\rho_{1}S_{1}\rho_{2}$ where $S_{1}\in S_{0}/\rho$. But recall that
$S_{0}$ is the leftmost coarse step for $(\rho\sigma,t^{\prime})$ and
$\rho_{1}\sqsubseteq\rho\sigma$, so it has at most one residual (Lem. 38).
This means that $S_{0}/\rho_{1}=S_{1}$, so $S_{0}/\rho=\varnothing$, which is
a contradiction. Given that no residuals of $S_{0}$ are contracted along the
derivation $\rho$, we have that the sets $\mathsf{labs}(S_{0}/t^{\prime})$ and
$\mathsf{labs}(\rho/t^{\prime})$ are disjoint which justifies the last step.

According to the chain of equalities above, we have that
$\mathsf{labs}(S_{0}/t^{\prime})=\varnothing$. This means that $S_{0}$ is
$t^{\prime}$-garbage. This in turn contradicts the fact that $S_{0}$ is coarse
for $(\rho\sigma,t^{\prime})$, confirming that this case is impossible.

We have just claimed that $R_{0}=S_{0}$. Then we conclude as follows:

$\begin{array}[]{rcll}\rho\sigma\Downarrow
t^{\prime}&=&R_{0}((\rho\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))\\\
&=&R_{0}(((\rho/R_{0})(\sigma/(R_{0}/\rho)))\Downarrow(t^{\prime}/R_{0}))\\\
&=&R_{0}((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))\hskip 14.22636pt\text{by
{\em i.h.}, as $\sigma/(R_{0}/\rho)$ is garbage by
Prop.~{}\ref{prop:properties_of_garbage}}\\\ &=&\rho\Downarrow t^{\prime}\\\
\end{array}$

Let us check the two items of Prop. 11:

  1. 1.

The set $\mathbb{F}(t^{\prime},t)$ forms a finite lattice. Let us check all
the conditions:

    1. 1.1

Partial order. First let us show that $\unlhd$ is a partial order.

      1. 1.1.1

Reflexivity. It is immediate that ${[\rho]}\unlhd{[\rho]}$ holds since
$\rho/\rho=\epsilon$ is garbage.

      2. 1.1.2

Antisymmetry. Let ${[\rho]}\unlhd{[\sigma]}\unlhd{[\rho]}$. This means that
$\rho/\sigma$ and $\sigma/\rho$ are garbage. Then:

$\begin{array}[]{rcll}\rho&\equiv&\rho\Downarrow t^{\prime}&\text{ since
$\rho$ is garbage-free, by
Prop.~{}\ref{prop:characterization_of_garbage_free_derivations}}\\\
&\equiv&\rho(\sigma/\rho)\Downarrow t^{\prime}&\text{ since $\sigma/\rho$ is
garbage, by Lem.~{}\ref{lemma:sieving_trailing_garbage}}\\\
&\equiv&\sigma(\rho/\sigma)\Downarrow t^{\prime}&\text{ since $A(B/A)\equiv
B(A/B)$ in general, using
Lem.~{}\ref{lemma:sieving_is_compatible_with_permutation_equivalence}}\\\
&\equiv&\sigma\Downarrow t^{\prime}&\text{ since $\rho/\sigma$ is garbage, by
Lem.~{}\ref{lemma:sieving_trailing_garbage}}\\\ &\equiv&\sigma&\text{ since
$\sigma$ is garbage-free, by
Prop.~{}\ref{prop:characterization_of_garbage_free_derivations}}\\\
\end{array}$

Since $\rho\equiv\sigma$ we conclude that ${[\rho]}={[\sigma]}$, as required.

      3. 1.1.3

Transitivity. Let ${[\rho]}\unlhd{[\sigma]}\unlhd{[\tau]}$ and let us show
that ${[\rho]}\unlhd{[\tau]}$. Note that $\rho/\sigma$ and $\sigma/\tau$ are
garbage. By the fact that the projection of garbage is garbage (Prop. 9) the
derivation $(\rho/\sigma)/(\sigma/\tau)$ is garbage. The composition of
garbage is also garbage (Prop. 9), so
$(\sigma/\tau)((\rho/\sigma)/(\sigma/\tau))$ is garbage. In general the
following holds:

$\begin{array}[]{rcll}\rho/\tau&\sqsubseteq&(\rho/\tau)((\sigma/\tau)/(\rho/\tau))&\text{
since $A\sqsubseteq AB$ in general}\\\
&\equiv&(\sigma/\tau)((\rho/\tau)/(\sigma/\tau))&\text{ since $A(B/A)\equiv
B(A/B)$ in general}\\\
&\equiv&(\sigma/\tau)((\rho/\sigma)/(\tau/\sigma))&\text{ since $A(B/A)\equiv
B(A/B)$ in general}\\\ \end{array}$

So since any prefix of a garbage derivation is garbage (Prop. 9) we conclude
that $\rho/\tau$ is garbage. This means that $[\rho]\unlhd[\tau]$, as
required.

    2. 1.2

Finite. Let us check that $\mathbb{F}(t^{\prime},t)$ is a finite lattice, i.e.
that it has a finite number of elements. Recall that
$\mathbb{F}(t^{\prime},t)$ is the set of equivalence classes ${[\rho]}$ where
$\rho$ is $t^{\prime}$-garbage-free.

On one hand, recall that the $\lambda^{\texttt{{\\#}}}$-calculus is finitely
branching and strongly normalizing (Prop. 1). So by König’s lemma the set of
$\mathrel{\to_{\texttt{{\\#}}}}$-derivations starting from $t^{\prime}$ is
bounded in length. More precisely, there is a constant $M$ such that for any
$s^{\prime}\in\mathcal{T}^{\texttt{{\\#}}}$ and any derivation
$\rho:t^{\prime}\mathrel{\to_{\texttt{{\\#}}}}^{*}s^{\prime}$ we have that the
length $|\rho|$ is bounded by $M$.

On the other hand, let $F=\\{\rho\ |\ \rho\text{ is $t^{\prime}$-garbage-free
and }\rho\Downarrow t^{\prime}=\rho\\}$. Consider the mapping
$\varphi:\mathbb{F}(t^{\prime},t)\to F$ given by
${[\rho]}\mapsto\rho\Downarrow t^{\prime}$, and note that:

       * •

$\varphi$ does not depend on the choice of representative, that is, if
${[\rho]}={[\sigma]}$ then $\varphi({[\rho]})=\rho\Downarrow
t^{\prime}=\sigma\Downarrow t^{\prime}=\varphi({[\sigma]})$. This is a
consequence of Lem. 41.

       * •

$\varphi$ is a well-defined function, that is $\varphi({[\rho]})\in F$. This
is because $\varphi({[\rho]})=\rho\Downarrow t^{\prime}$ is
$t^{\prime}$-garbage-free by Prop. 10. Moreover, we have that
$\varphi({[\rho]})\Downarrow t^{\prime}=({[\rho]}\Downarrow
t^{\prime})\Downarrow t^{\prime}={[\rho]}\Downarrow
t^{\prime}=\varphi({[\rho]})$, which is also a consequence of Lem. 41, and the
fact that ${[\rho]}\Downarrow t^{\prime}\equiv\rho$ (Prop. 10).

       * •

$\varphi$ is injective. Indeed, suppose that
$\varphi({[\rho]})=\varphi({[\sigma]})$, that is, $\rho\Downarrow
t^{\prime}=\sigma\Downarrow t^{\prime}$. Then $\rho\equiv\rho\Downarrow
t^{\prime}=\sigma\Downarrow t^{\prime}\equiv\sigma$ by Prop. 10 since $\rho$
and $\sigma$ are $t^{\prime}$-garbage-free. Hence ${[\rho]}={[\sigma]}$.

Since $\varphi:\mathbb{F}(t^{\prime},t)\to F$ is injective, it suffices to
show that $F$ is finite to conclude that $\mathbb{F}(t^{\prime},t)$ is finite.
Recall that the $\lambda$-calculus is finitely branching, so the number of
derivations of a certain length is finite. To show that $F$ is finite, it
suffices to show that the length of derivations in $F$ is bounded by some
constant. Let $\rho$ be a derivation in $F$. We have that $\rho=\rho\Downarrow
t^{\prime}$. By construction of the sieve, none of the steps of
$\rho\Downarrow t^{\prime}$ are garbage. That is $\rho=\rho\Downarrow
t^{\prime}=R_{1}\ldots R_{n}$ where for all $i$ we have that
$R_{i}/(t^{\prime}/R_{1}\ldots R_{i-1})\neq\varnothing$. So we have that the
length of $\rho/t^{\prime}$ is greater than the length of $\rho$ for all
$\rho\in F$:

$|\rho/t^{\prime}|=\sum_{i=1}^{n}|\underbrace{R/(t^{\prime}/R_{1}\ldots
R_{i-1})}_{\neq\varnothing}|\geq n=|\rho|$

As a consequence given any $\mathrel{\to_{\beta}}$-derivation $\rho\in F$ we
have that $|\rho|\leq|\rho/t^{\prime}|\leq M$. This concludes the proof that
$\mathbb{F}(t^{\prime},t)$ is finite.

    3. 1.3

Bottom element. As the bottom element take
$\bot_{(\mathbb{F}(t^{\prime},t))}:={[\epsilon]}$. Observe that this is well-
defined since $\epsilon$ is $t^{\prime}$-garbage-free. Moreover, let us show
that $\bot_{(\mathbb{F}(t^{\prime},t))}$ is the least element. Let $[\rho]$ be
an arbitrary element of $\mathbb{F}(t^{\prime},t)$ and let us check that
$\bot_{(\mathbb{F}(t^{\prime},t))}\unlhd[\rho]$. This is immediate since, by
definition, $\bot_{(\mathbb{F}(t^{\prime},t))}\unlhd[\rho]$ if and only if
$\epsilon/\rho$ is garbage. But $\epsilon/\rho=\epsilon$ is trivially garbage.

    4. 1.4

Join. Let $[\rho],[\sigma]$ be arbitrary elements of
$\mathbb{F}(t^{\prime},t)$, and let us check that
$[\rho]\triangledown[\sigma]$ is the join. First observe that
$[\rho]\triangledown[\sigma]$ is well-defined i.e. that
$(\rho\sqcup\sigma)\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free, which
is an immediate consequence of Prop. 14. Moreover, it is indeed the least
upper bound of $\\{[\rho],[\sigma]\\}$:

      1. 1.4.1

Upper bound. Let us show that $[\rho]\unlhd[\rho]\triangledown[\sigma]$; the
proof for $[\sigma]$ is symmetrical. We must show that
$\rho/((\rho\sqcup\sigma)\Downarrow t^{\prime})$ is garbage. Note that
$\rho\sqsubseteq\rho\sqcup\sigma$, so in particular
$\rho/((\rho\sqcup\sigma)\Downarrow
t^{\prime})\sqsubseteq(\rho\sqcup\sigma)/((\rho\sqcup\sigma)\Downarrow
t^{\prime})$. Given that any prefix of a garbage derivation is garbage (Prop.
9), it suffices to show that $(\rho\sqcup\sigma)/((\rho\sqcup\sigma)\Downarrow
t^{\prime})$ is garbage. This is a straightforward consequence of the fact
that projecting after a sieve is garbage (Lem. 40).

      2. 1.4.2

Least upper bound. Let $[\rho],[\sigma]\unlhd[\tau]$, and let us show that
$[\rho]\triangledown[\sigma]\unlhd[\tau]$. We know that $\rho/\tau$ and
$\sigma/\tau$ are garbage, and we are to show that
$((\rho\sqcup\sigma)\Downarrow t^{\prime})/\tau$ is garbage. Note that
$(\rho\sqcup\sigma)\Downarrow t^{\prime}\sqsubseteq\rho\sqcup\sigma$ as a
consequence of the fact that the sieve is a prefix (Lem. 35). So in particular
$((\rho\sqcup\sigma)\Downarrow
t^{\prime})/\tau\sqsubseteq(\rho\sqcup\sigma)/\tau$. Given that any prefix of
a garbage derivation is garbage (Prop. 9), it suffices to show that
$(\rho\sqcup\sigma)/\tau$ is garbage. But
$(\rho\sqcup\sigma)/\tau\equiv\rho/\tau\sqcup\sigma/\tau$ so we conclude by
the fact that the join of garbage is garbage (Prop. 9).

    5. 1.5

Top element. Since $\mathbb{F}(t^{\prime},t)$ is finite, its elements are
$\\{{[\tau_{1}]},\ldots,{[\tau_{n}]}\\}$. It suffices to take
$\top:={[\tau_{1}]}\triangledown\ldots\triangledown{[\tau_{n}]}$ as the top
element.

    6. 1.6

Meet. Let ${[\rho]},{[\sigma]}\in\mathbb{F}(t^{\prime},t)$. Note that the set
$L=\\{{[\tau]}\in\mathbb{F}(t^{\prime},t)\ |\ {[\tau]}\unlhd{[\rho]}\text{ and
}{[\tau]}\unlhd{[\sigma]}\\}$ is finite because, as we have already proved,
the set $\mathbb{F}(t^{\prime},t)$ is itself finite. Then
$L=\\{{[\tau_{1}]},\ldots,{[\tau_{n}]}\\}$. Take
${[\rho]}\\!\vartriangle\\!{[\sigma]}:={[\tau_{1}]}\triangledown\ldots\triangledown{[\tau_{n}]}$.
It is straightforward to show that ${[\rho]}\\!\vartriangle\\!{[\sigma]}$ thus
defined is the greatest lower bound for $\\{{[\rho]},{[\sigma]}\\}$.

  2. 2.

The set $\mathbb{G}(t^{\prime},t)$ forms an upper semilattice. The semilattice
structure of $\mathbb{G}(t^{\prime},t)$ is inherited from
$\mathbb{D}^{\lambda}(t)$. More precisely, ${[\rho]}\sqsubseteq{[\sigma]}$ is
declared to hold if $\rho\sqsubseteq\sigma$, the bottom element is
${[\epsilon]}$, and the join is
${[\rho]}\sqcup{[\sigma]}={[\rho\sqcup\sigma]}$. Let us check that this is an
upper semilattice:

    1. 2.1

Partial order. The relation $(\sqsubseteq)$ is a partial order on
$\mathbb{G}(t^{\prime},t)$ because it is already a partial order in
$\mathbb{D}^{\lambda}(t)$.

    2. 2.2

Bottom element. It suffices to note that the empty derivation
$\epsilon:t\mathrel{\to_{\beta}}^{*}t$ is $t^{\prime}$-garbage, so
${[\epsilon]}\in\mathbb{G}(t^{\prime},t)$ is the least element.

    3. 2.3

Join. By Prop. 9 we know that if $\rho$ and $\sigma$ are $t^{\prime}$-garbage
then $\rho\sqcup\sigma$ is $t^{\prime}$-garbage, so ${[\rho]}\sqcup{[\sigma]}$
is indeed the least upper bound of $\\{{[\rho]},{[\sigma]}\\}$.

###  0.A.15 Proof of Thm. 5.1 – Factorization

We need a few auxiliary lemmas:

######  Lemma 43 (Garbage-free/garbage decomposition)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and
$t^{\prime}\mathrel{\ltimes}t$. Then there exist $\rho_{1},\rho_{2}$ such
that:

  1. 1.

$\rho\equiv\rho_{1}\rho_{2}$

  2. 2.

$\rho_{1}$ is $t^{\prime}$-garbage-free,

  3. 3.

$\rho_{2}$ is $t^{\prime}$-garbage.

Moreover, $\rho_{1}$ and $\rho_{2}$ are unique modulo permutation equivalence,
and we have that $\rho_{1}\equiv\rho\Downarrow t^{\prime}$ and
$\rho_{2}\equiv\rho/(\rho\Downarrow t^{\prime})$.

###### Proof

Let us prove that said decomposition exists and that it is unique:

  * •

Existence. Take $\rho_{1}:=\rho\Downarrow t^{\prime}$ and
$\rho_{2}:=\rho/(\rho\Downarrow t^{\prime})$. Then we may check the three
conditions in the statement:

    1. 1.

Recall that $\rho\Downarrow t^{\prime}\sqsubseteq\rho$ holds by Lem. 35, so:

$\begin{array}[]{rcll}\rho_{1}\rho_{2}&=&(\rho\Downarrow
t^{\prime})(\rho/(\rho\Downarrow t^{\prime}))\\\ &\equiv&\rho((\rho\Downarrow
t^{\prime})/\rho)&\text{ since $A(B/A)\equiv B(A/B)$ holds in general}\\\
&\equiv&\rho&\text{ since $\rho\Downarrow
t^{\prime}\sqsubseteq\rho$}\end{array}$

as required.

    2. 2.

The derivation $\rho_{1}=\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-
free. This is as an immediate consequence of Prop. 14, namely the result of
sieving is always garbage-free.

    3. 3.

The derivation $\rho_{2}=\rho/(\rho\Downarrow t^{\prime})$ is garbage. This is
an immediate consequence of Lem. 40, namely projection after a sieve is always
garbage.

  * •

Uniqueness, modulo permutation equivalence. Let
$\rho\equiv\sigma_{1},\sigma_{2}$ where $\sigma_{1}$ is $t^{\prime}$-garbage-
free, and $\sigma_{2}$ is $t^{\prime}$-garbage. Then we argue that
$\sigma_{1}\equiv\rho_{1}$ and $\sigma_{2}\equiv\rho_{2}$.

Since $\rho_{1}\rho_{2}\equiv\rho\equiv\sigma_{1}\sigma_{2}$ and sieving is
compatible with permutation equivalence (Lem. 41) we have that
$\rho_{1}\rho_{2}\Downarrow t^{\prime}\equiv\sigma_{1}\sigma_{2}\Downarrow
t^{\prime}$. By Lem. 42, we know that trailing garbage does not affect
sieving, hence $\rho_{1}\Downarrow t^{\prime}\equiv\sigma_{1}\Downarrow
t^{\prime}$. Moreover, $\rho_{1}$ and $\sigma_{1}$ are garbage-free, which by
Prop. 14 means that $\rho_{1}\equiv\sigma_{1}$. This means that $\rho_{1}$ is
unique, modulo permutation equivalence. Finally, since
$\rho_{1}\rho_{2}\equiv\sigma_{1}\sigma_{2}$ and $\rho_{1}\equiv\sigma_{1}$,
we have that $\rho_{1}\rho_{2}/\rho_{1}\equiv\sigma_{1}\sigma_{2}/\sigma_{1}$,
that is $\rho_{2}\equiv\sigma_{2}$. This means that $\rho_{2}$ is unique,
modulo permutation equivalence.

###### Lemma 44

Let $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)=\mathsf{src}(\sigma)$. Then
${[(\rho\sqcup\sigma)\Downarrow t^{\prime}]}={[\rho\Downarrow
t^{\prime}]}\triangledown{[\sigma\Downarrow t^{\prime}]}$.

###### Proof

Let:

$\begin{array}[]{rcl}\alpha&:=&\rho/(\rho\Downarrow t^{\prime})\\\
\beta&:=&\sigma/(\sigma\Downarrow t^{\prime})\\\
\gamma&:=&(\alpha/((\sigma\Downarrow t^{\prime})/(\rho\Downarrow
t^{\prime})))\sqcup(\beta/((\rho\Downarrow t^{\prime})/(\sigma\Downarrow
t^{\prime})))\\\ \end{array}$

Note that $\alpha$ and $\beta$ are garbage by Lem. 40 and hence $\gamma$ is
also garbage, as a consequence of the facts that the join of garbage is
garbage and that the projection of garbage is garbage (Prop. 9). Remark that,
in general, $AB\sqcup CD\equiv(A\sqcup C)(B/(C/A)\sqcup D/(A/C))$. Then the
statement of this lemma is a consequence of the following chain of equalities:

$\begin{array}[]{rcll}{[(\rho\sqcup\sigma)\Downarrow
t^{\prime}]}&=&{[((\rho\Downarrow t^{\prime})\alpha\sqcup(\sigma\Downarrow
t^{\prime})\beta)\Downarrow t^{\prime}]}&\text{by
Lem.~{}\ref{lemma:garbage_free_garbage_decomposition}}\\\
&=&{[((\rho\Downarrow t^{\prime})\sqcup(\sigma\Downarrow
t^{\prime}))\gamma\Downarrow t^{\prime}]}&\text{by the previous remark}\\\
&=&{[((\rho\Downarrow t^{\prime})\sqcup(\sigma\Downarrow
t^{\prime}))\Downarrow
t^{\prime}]}&\text{by~{}Lem.~{}\ref{lemma:sieving_trailing_garbage}}\\\
&=&{[\rho\Downarrow t^{\prime}]}\triangledown{[\sigma\Downarrow
t^{\prime}]}&\text{by definition of $\triangledown$}\end{array}$

To prove Thm. 5.1, let us check that $\int_{\mathcal{F}}{\mathcal{G}}$ is
well-defined, that it is an upper semilattice, and finally that
$\mathbb{D}^{\lambda}(t)\simeq\int_{\mathcal{F}}{\mathcal{G}}$ are isomorphic
as upper semilattices.

  1. 1.

The Grothendieck construction $\int_{\mathcal{F}}{\mathcal{G}}$ is well-
defined. This amounts to checking that $\mathcal{G}$ is indeed a lax
2-functor:

    1. 1.1

The mapping $\mathcal{G}$ is well-defined on objects. Note that
$\mathcal{G}({[\rho]})=\mathbb{G}(t^{\prime}/\rho,\mathsf{tgt}(\rho))$, which
is a poset. Moreover, the choice of the representative $\rho$ of the
equivalence class ${[\rho]}$ does not matter, since if $\rho$ and $\sigma$ are
permutation equivalent derivations, then $t^{\prime}/\rho=t^{\prime}/\sigma$
(by Prop. 8) and $\mathsf{tgt}(\rho)=\mathsf{tgt}(\sigma)$.

    2. 1.2

The mapping $\mathcal{G}$ is well-defined on morphisms. Let us check that
given ${[\rho]},{[\sigma]}\in\mathcal{F}$ such that ${[\rho]}\unlhd{[\sigma]}$
then
$\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]}):\mathcal{G}({[\rho]})\to\mathcal{G}({[\sigma]})$
is a morphism of posets, i.e. a monotonic function.

First, we can see that it is well-defined, since if
${[\alpha]}\in\mathcal{G}([\rho])$ then the image
$\mathcal{G}({[\rho]})({[\alpha]}\hookrightarrow{[\sigma]})={[\rho\alpha/\sigma]}$
is an element of $\mathcal{G}([\sigma])$, since
$\rho\alpha/\sigma=(\rho/\sigma)(\alpha/(\sigma/\rho))$ is garbage, as it is
the composition of garbage derivations (Prop. 9): the derivation $\rho/\sigma$
is garbage since ${[\rho]}\unlhd{[\sigma]}$ (by definition), and the
derivation $\alpha/(\sigma/\rho)$ is garbage since $\alpha$ is garbage (Prop.
9). Moreover, the choice of representative does not matter, since if
$\rho_{1}\equiv\rho_{2}$ and $\sigma_{1}\equiv\sigma_{2}$ and
$\alpha_{1}\equiv\alpha_{2}$ then
$\rho_{1}\alpha_{1}/\sigma_{1}\equiv\rho_{2}\alpha_{2}/\sigma_{2}$.

We are left to verify that $\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})$ is
monotonic. Let ${[\alpha]},{[\beta]}\in\mathcal{G}([\rho])$ such that
${[\alpha]}\sqsubseteq{[\beta]}$, and let us show that
$\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})({[\alpha]})\sqsubseteq\mathcal{G}([\rho]\hookrightarrow[\sigma])({[\beta]})$.
Indeed, $\alpha\sqsubseteq\beta$, so
$\rho\alpha/\sigma=(\rho/\sigma)(\alpha/(\sigma/\rho))\sqsubseteq(\rho/\sigma)(\beta/(\sigma/\rho))=\rho\beta/\sigma$.

    3. 1.3

Identity. Let ${[\rho]}\in\mathcal{F}$. Let us check that
$\mathcal{G}({[\rho]}\hookrightarrow{[\rho]})=\mathsf{id}_{\mathcal{G}({[\rho]})}$
is the identity morphism. Indeed, if ${[\alpha]}\in\mathcal{G}({[\rho]})$,
then
$\mathcal{G}({[\rho]}\hookrightarrow{[\rho]})({[\alpha]})={[\rho\alpha/\rho]}={[\alpha]}$.

    4. 1.4

Composition. Let ${[\rho]},{[\sigma]},{[\tau]}\in\mathcal{F}$ such that
${[\rho]}\unlhd{[\sigma]}\unlhd{[\tau]}$. Let us check that there is a 2-cell
$\mathcal{G}(({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}))\sqsubseteq\mathcal{G}({[\sigma]}\hookrightarrow{[\tau]})\circ\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})$.
Note that
$({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}):{[\rho]}\unlhd{[\tau]}$
is a morphism in the upper semilattice $\mathcal{F}$ seen as a category.
Moreover, since it is a semilattice, there a unique morphism
${[\rho]}\unlhd{[\tau]}$, namely ${[\rho]}\hookrightarrow{[\tau]}$, so we have
that
$({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]})={[\rho]}\hookrightarrow{[\tau]}$.
Now if ${[\alpha]}\in\mathcal{G}{{[\rho]}}$, then:

$\begin{array}[]{rcll}\mathcal{G}(({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}))({[\alpha]})&=&\mathcal{G}({[\rho]}\hookrightarrow{[\tau]})({[\alpha]})\\\
&=&\rho\alpha/\tau\\\
&\sqsubseteq&(\rho\alpha/\tau)((\sigma/\rho\alpha)/(\tau/\rho\alpha))\\\
&=&\rho\alpha(\sigma/\rho\alpha)/\tau\\\
&\equiv&\sigma(\rho\alpha/\sigma)/\tau\hskip 14.22636pt\text{ since
$A(B/A)\equiv B(A/B)$}\\\
&=&\mathcal{G}({[\sigma]}\hookrightarrow{[\tau]})(\rho\alpha/\sigma)\\\
&=&(\mathcal{G}({[\sigma]}\hookrightarrow{[\tau]})\circ\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]}))({[\alpha]})\end{array}$

so
$\mathcal{G}(({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}))\sqsubseteq\mathcal{G}({[\sigma]}\hookrightarrow{[\tau]})\circ\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})$
as required.

  2. 2.

The Grothendieck construction $\int_{\mathcal{F}}{\mathcal{G}}$ is an upper
semilattice.

    1. 2.1

Partial order. Recall that $\int_{\mathcal{F}}{\mathcal{G}}$ is always poset
with the order given by $(a,b)\leq(a^{\prime},b^{\prime})$ if and only if
$a\unlhd a^{\prime}$ and $\mathcal{G}(a\hookrightarrow
a^{\prime})(b)\sqsubseteq b^{\prime}$.

    2. 2.2

Bottom element. We argue that
$(\bot_{\mathcal{F}},\bot_{\mathcal{G}(\bot_{\mathcal{F}})})$ is the bottom
element. Let $({[\rho]},{[\sigma]})\in\int_{\mathcal{F}}{\mathcal{G}}$. Then
clearly $\bot_{\mathcal{F}}\unlhd{[\rho]}$. Moreover,
$\mathcal{G}([\bot_{\mathcal{F}}]\hookrightarrow[\rho])(\bot_{\mathcal{G}})=[\epsilon/\rho]=[\epsilon]\sqsubseteq{[\sigma]}$.

    3. 2.3

Join. Let us show that $(a,b)\lor(a^{\prime},b^{\prime})=(a\triangledown
a^{\prime},\mathcal{G}(a\hookrightarrow(a\triangledown
a^{\prime}))(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow(a\triangledown
a^{\prime}))(b^{\prime}))$. is the least upper bound of
$\\{(a,b),(a^{\prime},b^{\prime})\\}$.

      1. 2.3.1

Upper bound. Let us show that $(a,b)\leq(a,b)\lor(a^{\prime},b^{\prime})$.
Recall that $(a,b)\lor(a^{\prime},b^{\prime})=(a\triangledown
a,\mathcal{G}(a\hookrightarrow(a\lor
a^{\prime}))(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow(a\triangledown
a^{\prime}))(b^{\prime}))$. First, we have $a\unlhd a\triangledown
a^{\prime}$. Moreover, $\mathcal{G}(a\hookrightarrow(a\triangledown
a^{\prime}))(b)\sqsubseteq\mathcal{G}(a\hookrightarrow(a\lor
a^{\prime}))(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow(a\triangledown
a^{\prime}))(b^{\prime})$, as required.

      2. 2.3.2

Least upper bound. Let $(a,b)=({[\rho]},{[\sigma]})$ and
$(a^{\prime},b^{\prime})=({[\rho^{\prime}]},{[\sigma^{\prime}]})$. Moreover,
let $({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$ be an upper bound,
i.e. an element such that
$({[\rho]},{[\sigma]})\leq({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$
and
$({[\rho^{\prime}]},{[\sigma^{\prime}]})\leq({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$.
Let us show that
$({[\rho]},{[\sigma]})\lor({[\rho^{\prime}]},{[\sigma^{\prime}]})\leq({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$.
First note that ${[\rho]}\unlhd{[\rho^{\prime\prime}]}$ and
${[\rho^{\prime}]}\unlhd{[\rho^{\prime\prime}]}$ so
${[\rho]}\triangledown{[\rho^{\prime}]}\unlhd{[\rho^{\prime\prime}]}$.
Moreover, we know that:

${[\rho\sigma/\rho^{\prime\prime}]}=\mathcal{G}({[\rho]}\hookrightarrow{[\rho^{\prime\prime}]})({[\sigma]})\sqsubseteq{[\sigma^{\prime\prime}]}\
\text{ and }\
{[\rho^{\prime}\sigma^{\prime}/\rho^{\prime\prime}]}=\mathcal{G}({[\rho^{\prime}]}\hookrightarrow{[\rho^{\prime\prime}]})({[\sigma^{\prime}]})\sqsubseteq{[\sigma^{\prime\prime}]}$

Let $\alpha:=(\rho\sqcup\rho^{\prime})\Downarrow t^{\prime}$. First we claim
that $\alpha\sqsubseteq\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime}$. Indeed,
$\alpha=(\rho\sqcup\rho^{\prime})\Downarrow
t^{\prime}\sqsubseteq\rho\sqcup\rho^{\prime}$ by Lem. 35, and it is easy to
check that
$\rho\sqcup\rho^{\prime}\sqsubseteq\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime}$.
What we have to check is the following inequality:

$\mathcal{G}({[\alpha]}\hookrightarrow{[\rho^{\prime\prime}]})(\mathcal{G}({[\rho]}\hookrightarrow{[\alpha]})({[\sigma]})\sqcup\mathcal{G}({[\rho^{\prime}]}\hookrightarrow{[\alpha]})({[\sigma^{\prime}]}))\sqsubseteq{[\sigma^{\prime\prime}]}$

Indeed:

$\begin{array}[]{rcll}&&\mathcal{G}({[\alpha]}\hookrightarrow{[\rho^{\prime\prime}]})(\mathcal{G}({[\rho]}\hookrightarrow{[\alpha]})({[\sigma]})\sqcup\mathcal{G}({[\rho^{\prime}]}\hookrightarrow{[\alpha]})({[\sigma^{\prime}]}))\\\
&=&{[\alpha((\rho\sigma/\alpha)\sqcup(\rho^{\prime}\sigma^{\prime}/\alpha))/\rho^{\prime\prime}]}\\\
&=&{[\alpha((\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime})/\alpha)/\rho^{\prime\prime}]}&\text{since
$A/C\sqcup B/C\equiv(A\sqcup B)/C$}\\\
&=&{[(\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime})(\alpha/(\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime}))/\rho^{\prime\prime}]}&\text{since
$A(B/A)\equiv B(A/B)$}\\\
&=&{[(\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime})/\rho^{\prime\prime}]}&\text{since
$\alpha\sqsubseteq\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime}$}\\\
&=&{[\rho\sigma/\rho^{\prime\prime}\sqcup\rho^{\prime}\sigma^{\prime}/\rho^{\prime\prime}]}&\text{since
$A/C\sqcup B/C\equiv(A\sqcup B)/C$}\\\
&\sqsubseteq&{[\sigma^{\prime\prime}]}&\text{since
${[\rho\sigma/\rho^{\prime\prime}]}\sqsubseteq{[\sigma^{\prime\prime}]}$ and
${[\rho^{\prime}\sigma^{\prime}/\rho^{\prime\prime}]}\sqsubseteq{[\sigma^{\prime\prime}]}$}\end{array}$

  3. 3.

There is an isomorphism
$\mathbb{D}^{\lambda}(t)\simeq\int_{\mathcal{F}}{\mathcal{G}}$ of upper
semilattices. As stated, the isomorphism is given by:

$\begin{array}[]{rclcl}\varphi&:&\mathbb{D}^{\lambda}(t)&\to&\int_{\mathcal{F}}{\mathcal{G}}\\\
&&{[\rho]}&\mapsto&({[\rho\Downarrow t^{\prime}]},{[\rho/(\rho\Downarrow
t^{\prime})]})\\\ \\\
\psi&:&\int_{\mathcal{F}}{\mathcal{G}}&\to&\mathbb{D}^{\lambda}(t)\\\
&&({[\rho]},{[\sigma]})&\mapsto&[\rho\sigma]\\\ \end{array}$

Note that $\varphi$ and $\psi$ are well-defined mappings, since their value
does not depend on the choice of representative, due, in particular, to the
fact that sieving is compatible with permutation equivalence (Lem. 41). Let us
check that $\varphi$ and $\psi$ are morphisms of upper semilatices, and that
they are mutual inverses:

    1. 3.1

$\varphi$ is a morphism of upper semilattices. Let us check the three
conditions:

      1. 3.1.1

Monotonic. Let ${[\rho]}\sqsubseteq{[\sigma]}$ in $\mathbb{D}^{\lambda}(t)$,
and let us show that the following inequality holds:

$\varphi({[\rho]})=({[\rho\Downarrow t^{\prime}]},{[\rho/(\rho\Downarrow
t^{\prime})]})\leq({[\sigma\Downarrow t^{\prime}]},{[\sigma/(\sigma\Downarrow
t^{\prime})]})=\varphi({[\sigma]})$

We check the two conditions (by definition of
$\int_{\mathcal{F}}{\mathcal{G}}$):

        1. 3.1.1.1

On the first hand, ${[\rho\Downarrow t^{\prime}]}\unlhd{[\sigma\Downarrow
t^{\prime}]}$ since

$\begin{array}[]{rcll}(\rho\Downarrow t^{\prime})/(\sigma\Downarrow
t^{\prime})&\sqsubseteq&\rho/(\sigma\Downarrow t^{\prime})&\text{since
$\rho\Downarrow t^{\prime}\sqsubseteq\rho$ by
Lem.~{}\ref{lemma:sieve_is_prefix}}\\\ &\sqsubseteq&\sigma/(\sigma\Downarrow
t^{\prime})&\text{since $\rho\sqsubseteq\sigma$ by hypothesis}\\\ \end{array}$

Note that this is garbage by Lem. 40. So by Prop. 9, $(\rho\Downarrow
t^{\prime})/(\sigma\Downarrow t^{\prime})$ is also garbage, as required.

        2. 3.1.1.2

On the other hand, let us show that $\mathcal{G}({[\rho\Downarrow
t^{\prime}]}\hookrightarrow{[\sigma\Downarrow
t^{\prime}]})({[\rho/(\rho\Downarrow
t^{\prime})]})\sqsubseteq\sigma/(\sigma\Downarrow t^{\prime})$. In fact:

$\begin{array}[]{rcll}\mathcal{G}({[\rho\Downarrow
t^{\prime}]}\hookrightarrow{[\sigma\Downarrow
t^{\prime}]})({[\rho/(\rho\Downarrow t^{\prime})]})&=&{[(\rho\Downarrow
t^{\prime})(\rho/(\rho\Downarrow t^{\prime}))/(\sigma\Downarrow
t^{\prime})]}&\text{ by definition}\\\ &=&{[\rho/(\sigma\Downarrow
t^{\prime})]}&\text{ by
Lem.~{}\ref{lemma:garbage_free_garbage_decomposition}}\\\
&\sqsubseteq&{[\sigma/(\sigma\Downarrow t^{\prime})]}&\text{ since
$\rho\sqsubseteq\sigma$}\\\ \end{array}$

      2. 3.1.2

Preserves bottom. By definition:
$\varphi(\bot_{\mathbb{D}^{\lambda}(t)})=({[\epsilon\Downarrow
t^{\prime}]},{[\epsilon/(\epsilon\Downarrow
t^{\prime})]})=({[\epsilon]},{[\epsilon]})=(\bot_{\mathcal{F}},\bot_{\mathcal{G}(\bot_{\mathcal{F}})})$.

      3. 3.1.3

Preserves joins. Let ${[\rho]},{[\sigma]}\in\mathbb{D}^{\lambda}(t)$, and let
us show that
$\varphi({[\rho]}\sqcup{[\sigma]})=\varphi({[\sigma]})\lor\varphi({[\sigma]})$.
Indeed, note that:

$\varphi({[\rho]}\sqcup{[\sigma]})=(\alpha,\beta)$

where

$\begin{array}[]{rcl}\alpha&=&{[(\rho\sqcup\sigma)\Downarrow t^{\prime}]}\\\
\beta&=&{[(\rho\sqcup\sigma)/((\rho\sqcup\sigma)\Downarrow t^{\prime})]}\\\
\end{array}$

and

$\varphi({[\rho]})\lor\varphi({[\sigma]})=({[\rho\Downarrow
t^{\prime}]},{[\rho/(\rho\Downarrow t^{\prime})]})\lor({[\sigma\Downarrow
t^{\prime}]},{[\sigma/(\sigma\Downarrow t^{\prime})]})\\\
=(\alpha^{\prime},\beta^{\prime})\\\ $

where

$\begin{array}[]{rcl}\alpha^{\prime}&=&{[\rho\Downarrow
t^{\prime}]}\triangledown{[\sigma\Downarrow t^{\prime}]}\\\
\beta^{\prime}&=&\mathcal{G}({[\rho\Downarrow
t^{\prime}]}\hookrightarrow\alpha)({[\rho/(\rho\Downarrow
t^{\prime})]})\sqcup\mathcal{G}({[\sigma\Downarrow
t^{\prime}]}\hookrightarrow\alpha)({[\sigma/(\sigma\Downarrow
t^{\prime})]})\end{array}$

It suffices to show that $\alpha=\alpha^{\prime}$ and $\beta=\beta^{\prime}$.
Let us show each separately:

        1. 3.1.3.1

Proof of $\alpha=\alpha^{\prime}$. The equality
$\alpha={[(\rho\sqcup\sigma)\Downarrow t^{\prime}]}={[\rho\Downarrow
t^{\prime}]}\triangledown{[\sigma\Downarrow t^{\prime}]}=\alpha^{\prime}$ is
an immediate consequence of Lem. 44.

        2. 3.1.3.2

Proof of $\beta=\beta^{\prime}$. Note that:

$\begin{array}[]{rcll}\beta^{\prime}&=&\mathcal{G}({[\rho\Downarrow
t^{\prime}]}\hookrightarrow\alpha^{\prime})({[\rho/(\rho\Downarrow
t^{\prime})]})\sqcup\mathcal{G}({[\sigma\Downarrow
t^{\prime}]}\hookrightarrow\alpha^{\prime})({[\sigma/(\sigma\Downarrow
t^{\prime})]})\\\ &=&{[(\rho\Downarrow t^{\prime})(\rho/(\rho\Downarrow
t^{\prime}))/\alpha^{\prime}\sqcup(\sigma\Downarrow
t^{\prime})(\sigma/(\sigma\Downarrow t^{\prime}))/\alpha^{\prime}]}\\\
&=&{[\rho/\alpha^{\prime}\sqcup\sigma/\alpha^{\prime}]}&\text{by
Lem.~{}\ref{lemma:garbage_free_garbage_decomposition}}\\\
&=&{[(\rho\sqcup\sigma)/\alpha^{\prime}]}&\text{since $A/C\sqcup
B/C\equiv(A\sqcup B)/C$}\\\
&=&{[(\rho\sqcup\sigma)/((\rho\sqcup\sigma)\Downarrow
t^{\prime})]}&\text{since $\alpha^{\prime}=\alpha=(\rho\sqcup\sigma)\Downarrow
t^{\prime}$}\\\ &=&\beta\\\ \end{array}$

as required.

    2. 3.2

$\psi$ is a morphism of upper semilattices. Let us check the three conditions:

      1. 3.2.1

Monotonic. Let
$({[\rho_{1}]},{[\sigma_{1}]})\leq({[\rho_{2}]},{[\sigma_{2}]})$ in
$\int_{\mathcal{F}}{\mathcal{G}}$ and let us show that
$\psi({[\rho_{1}]},{[\sigma_{1}]})\sqsubseteq\psi({[\rho_{2}]},{[\sigma_{2}]})$
in $\mathbb{D}^{\lambda}(t)$. Indeed, we know that
$\mathcal{G}({[\rho_{1}]}\hookrightarrow{[\rho_{2}]})({[\sigma_{1}]})\sqsubseteq{[\sigma_{2}]}$,
that is to say $\rho_{1}\sigma_{1}/\rho_{2}\sqsubseteq\sigma_{2}$. Then:

$\rho_{1}\sigma_{1}/\rho_{2}\sigma_{2}=(\rho_{1}\sigma_{1}/\rho_{2})/\sigma_{2}=\epsilon$

which means that $\rho_{1}\sigma_{1}\sqsubseteq\rho_{2}\sigma_{2}$. This
immediately implies that
$\psi({[\rho_{1}]},{[\sigma_{1}]})\sqsubseteq\psi({[\rho_{2}]},{[\sigma_{2}]})$.

      2. 3.2.2

Preserves bottom. Recall that the bottom element
$\bot_{(\int_{\mathcal{F}}{\mathcal{G}})}$ is defined as
$(\bot_{\mathcal{F}},\bot_{\mathcal{G}(\bot_{\mathcal{F}})})$, that is
$({[\epsilon]},{[\epsilon]})$. Therefore
$\psi(\bot_{(\int_{\mathcal{F}}{\mathcal{G}})})={[\epsilon]}=\bot_{\mathbb{D}^{\lambda}(t)}$.

      3. 3.2.3

Preserves joins. Let $({[\rho_{1}]},{[\sigma_{1}]})$ and
$({[\rho_{2}]},{[\sigma_{2}]})$ be elements of
$\int_{\mathcal{F}}{\mathcal{G}}$, and let us show that
$\psi(({[\rho_{1}]},{[\sigma_{1}]})\lor({[\rho_{2}]},{[\sigma_{2}]}))=\psi({[\rho_{1}]},{[\sigma_{1}]})\sqcup\psi({[\rho_{2}]},{[\sigma_{2}]}))$.

Let:

$\begin{array}[]{rcl}\alpha&:=&(\rho_{1}\sqcup\rho_{2})\Downarrow
t^{\prime}\end{array}$

First we claim that
$\alpha\sqsubseteq\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}$. This is because
by Lem. 35 we know that $\alpha=(\rho_{1}\sqcup\rho_{2})\Downarrow
t^{\prime}\sqsubseteq\rho_{1}\sqcup\rho_{2}$. Moreover, it is easy to check
that
$\rho_{1}\sqcup\rho_{2}\sqsubseteq\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}$.
Using this fact we have:

$\begin{array}[]{rcll}\psi(({[\rho_{1}]},{[\sigma_{1}]})\lor({[\rho_{2}]},{[\sigma_{2}]}))&=&\psi({[\alpha]},\mathcal{G}({[\rho_{1}]}\hookrightarrow{[\alpha]})({[\sigma_{1}]})\sqcup\mathcal{G}({[\rho_{2}]}\hookrightarrow{[\alpha]})({[\sigma_{2}]}))\\\
&=&\psi({[\alpha]},{[(\rho_{1}\sigma_{1}/\alpha)\sqcup(\rho_{2}\sigma_{2}/\alpha)]})\\\
&=&\psi({[\alpha]},{[(\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2})/\alpha]})\\\
&&\text{ since $A/C\sqcup B/C\sqsubseteq(A\sqcup B)/C$}\\\
&=&{[\alpha((\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2})/\alpha)]}\\\
&=&{[(\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2})(\alpha/(\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}))]}\\\
&=&{[\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}]}\\\ &&\text{ since
$\alpha\sqsubseteq\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}$, so
$\alpha/(\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2})=\epsilon$}\\\
&=&\psi({[\rho_{1}]},{[\sigma_{1}]})\sqcup\psi({[\rho_{2}]},{[\sigma_{2}]}))\end{array}$

as required.

    3. 3.3

Left inverse: $\psi\circ\varphi=\mathsf{id}$. Let
${[\rho]}\in\mathbb{D}^{\lambda}(t)$. Then by Lem. 43:

$\psi(\varphi({[\rho]}))=\psi({[\rho\Downarrow
t^{\prime}]},{[\rho/(\rho\Downarrow t^{\prime})]})={[(\rho\Downarrow
t^{\prime})(\rho/(\rho\Downarrow t^{\prime}))]}={[\rho]}$

    4. 3.4

Right inverse: $\varphi\circ\psi=\mathsf{id}$. Let
$({[\rho]},{[\sigma]})\in\int_{\mathcal{F}}{\mathcal{G}}$. Note that $\rho$ is
$t^{\prime}$-garbage-free and $\sigma$ is $t^{\prime}$-garbage, so by Lem. 42
and Prop. 14 we know that $\rho\sigma\Downarrow t^{\prime}=\rho\Downarrow
t^{\prime}\equiv\rho$. Hence:

$\varphi(\psi({[\rho]},{[\sigma]}))=\varphi({[\rho\sigma]})=({[\rho\sigma\Downarrow
t^{\prime}]},{[\rho\sigma/(\rho\sigma\Downarrow
t^{\prime})]})=({[\rho]},{[\rho\sigma/\rho]})=({[\rho]},{[\sigma]})$