~ohad-kammar/ohads-thesis/trunk

\Section{Ad-hoc combination}\sectionlabel{ad-hoc}
Unfortunately, not all the global algebraic optimisations are
operation-wise valid. The Copy, Weak Copy, and Unique optimisations
are not operation-wise valid. Thus, in order to validate them in a
combined theory, we need to employ ad-hoc methods. We begin with a
general tool: if a theory validates a global algebraic optimisation,
then every super-theory of it with the same signature also validates
the same optimisation.
\begin{proposition}\propositionlabel{supertheory optimisation inheritance}
  If\/ $\mL=\Theory{\pair\uaSignature\uaEq}$ validates one of the
  Discard, Copy, Weak Copy, Unique, Pure Hoise, or Hoist
  optimisations, and if $\mL' = \Theory{\pair\uaSignature{\uaEq'}}$ is
  any theory with $\uaEq \subset\uaEq'$, then $\mL'$ validates
  the same optimisation.

  Analogously, if\/
  $\Theory{\pair{\uaSignature_1}{\uaEq_1}}
  \xto{\Theory{\Translation_1}} \Theory{\pair{\uaSignature}{\uaEq}}
  \xfrom {\Theory{\Translation_2}}
  \Theory{\pair{\uaSignature_2}{b\uaEq_2}}$
  satisfy any the various {Swap} optimisations, and if, further,
  $\Theory{\pair{\uaSignature_1}{\uaEq'_1}}
  \xto{\Theory{\Translation'_1}} \Theory{\pair{\uaSignature'}{\uaEq'}}
  \xfrom{\Theory{\Translation'_2}}
  \Theory{\pair{\uaSignature'_2}{\uaEq'_2}}$ are such that
  $\uaSignature \subset \uaSignature'$, $\uaEq \subset \uaEq'$,
  for each $i=1,2$, $\uaEq_1 \subset \uaEq$, and for each $\mop$ in
  $\uaSignature_i$, ${\Translation_i(\mop) = \Translation'_i(\mop)}$, then
    $\Theory{\pair{\uaSignature_1}{\uaEq'_1}}
  \xto{\Theory{\Translation'_1}} \Theory{\pair{\uaSignature'}{\uaEq'}}
  \xfrom{\Theory{\Translation'_2}}
  \Theory{\pair{\uaSignature'_2}{\uaEq'_2}}$ validate the same swap optimisation.
\end{proposition}

\begin{proof}%
  Each of the algebraic characterisations of the
  optimisations only involves the provability of
  certain equations over the sets of terms. Adding more axioms
  without changing the signature maintains
  the provability of these characterisations, and the theorem follows.
\end{proof}

The first two optimisation we consider are Copy and Weak Copy.

\begin{theorem}\theoremlabel{constant copy combination}
  Let $\mL = \Theory{\pair{\uaSignature}\uaEq}$ and $\mL'$ be two Lawvere
  theories satisfying the (Weak) Copy optimisation.
  If, for every $\mop \in \uaSignature$, $\mop \of 0$, then $\mL +
  \mL'$ and $\mL\tensor\mL'$ satisfy the same optimisation.
\end{theorem}
Note that, as $\mL$ only has constant operations, it necessarily
satisfies the (Weak) Copy optimisation.

{
\allowdisplaybreaks
\newindex\ii{n}{i}
\newindex\iv{n}{i'}
\newindex\iw{n}{i''}
\newindex\jj{k}{j}
\newindex\jv{k}{j'}
\newindex\jw{k}{j''}
\newindex\el{n+k}{\ell}
\begin{proof}%
  First, we assume $\mL'$ validates the Copy optimisation, and prove
  the statement for the sum $\mL+\mL'$.  Denote $\mL' =
  \Theory{\pair{\uaSignature'}{\uaEq'}}$, and consider any
  $\uaSignature+\uaSignature'$-term $\mtermu(\tx_1, \ldots, \tx_n)$. As
  $\uaSignature$ consists solely of constants, $\mtermu$ must be of the
  form $\mterm(\tx_1, \ldots, \tx_n, \uaconst_1, \ldots, \uaconst_k)$,
  where $\mterm(\tx_1, \ldots, \tx_{n+k})$ is a $\uaSignature'$-term,
  and $\uaconst_i \of 0$ in $\uaSignature$, for every $1 \leq i \leq
  k$. Note that $\mterm$, as a $\uaSignature'$-term, satisfies the
  idempotency law.

  First, we demonstrate the
  algebraic manipulation in the proof for the case $n = k = 2$.
  \begin{align*}
    \mtermu(\mtermu(\tx^1_1, &\tx^1_2), \mtermu(\tx^2_1, \tx^2_2))
    \\&=
    \mterm(
      \mterm(\tx^1_1, \tx^1_2, \uaconst_1, \uaconst_2),
      \mterm(\tx^2_1, \tx^2_2, \uaconst_1, \uaconst_2),
      \uaconst_1,
      \uaconst_2)
      \\&\mathbin{ \smash{\explain*={($*$)}}}
      \begin{aligned}[t]
        \mterm(&\boxed{
          \mterm(\mterm(\tx^1_1, \tx^1_2, \uaconst_1, \uaconst_2),
                 \mterm(\tx^2_1, \tx^2_2, \uaconst_1, \uaconst_2),
                 \mterm(\tx^3_1, \tx^3_2, \uaconst_1, \uaconst_2),
                 \mterm(\tx^4_1, \tx^4_2, \uaconst_1, \uaconst_2)),}\\&\boxed{
          \mterm(\mterm(\tx^1_1, \tx^1_2, \uaconst_1, \uaconst_2),
                 \mterm(\tx^2_1, \tx^2_2, \uaconst_1, \uaconst_2),
                 \mterm(\tx^3_1, \tx^3_2, \uaconst_1, \uaconst_2),
                 \mterm(\tx^4_1, \tx^4_2, \uaconst_1, \uaconst_2)),}\\&
          \mterm(\tx^3_1, \tx^3_2, \uaconst_1, \uaconst_2),\\&
          \mterm(\tx^4_1, \tx^4_2, \uaconst_1, \uaconst_2)
        )
      \end{aligned}
      \\&  \smash{\explain={($**$)}}
      \begin{aligned}[t]
        \mterm(&
          \mterm(\tx^1_1,
                 \tx^2_2,
                 \uaconst_1,
                 \uaconst_2),\\&
          \mterm(\tx^1_1,
                 \tx^2_2,
                 \uaconst_1,
                  \uaconst_2),\\&
          \mterm(\tx^3_1, \tx^3_2, \uaconst_1, \uaconst_2),\\&
          \mterm(\tx^4_1, \tx^4_2, \uaconst_1, \uaconst_2)
    )
    \explain*={($***$)}
    \mterm(\tx^1_1, \tx^2_2, \uaconst_1, \uaconst_2)
    =
    \mtermu(\tx^1_1, \tx^2_2)
\end{aligned}
  \end{align*}
  First, note how in transition $(*)$ we use the idempotency law to
  introduce new subterms. In particular, we introduce four fresh
  variables, $\tx^3_1$, $\tx^3_1$, $\tx^4_1$, and $\tx^4_2$.  The
  freshness of these variables is not important, but merely
  illustrates that we may choose arbitrary terms in their stead.  In
  transition $(**)$, we simplify the first two arguments in the
  outermost term using the idempotency law. We then
  simplify the entire term using the idempotency law in transition
  $(***)$ to obtain the right-hand side of the idempotency law.

  This example generalises to arbitray $n$ and $k$, but requires more
  complex index manipulations. To clarify those manipulations, we write
  $\tseq in{x_i}$ for the sequence $\seq[i=1][n]{x_i} = \seq{x_1,
    \ldots, x_n}$.  This notation has the benefit of binding the index
  \emph{before} usage, while maintaining the lightweight syntax of the
  sequencing brackets. We  suppress string concatenation, by writing
  $\mterm(\tseq in{\tx_i}, \tseq jk{\uaconst_k})$ for
  $\mterm(\tx_1, \ldots, \tx_n, \uaconst_1, \ldots, \uaconst_k)$.

  With these conventions, calculate:
  \begin{align*}
    \mathrlap{\mtermu{\myseq\ii{\mtermu{\myseq\iv{\tx^{\ii}_{\iv}}}}}}\\
    &\qquad=
      \mterm\parent{\myseq\ii{\mterm\parent{\myseq\iv{\tx^{\ii}_{\iv}},
          \myseq\jv{\uaconst_{\jv}}}}, \myseq\jj{\uaconst_{\jj}}}
    \\&\explain={($*$)}
    \mterm
    \begin{aligned}[t]
    &\left(\myseq\iw{\boxed{\mterm{
          \myseq\el{\mterm\parent{\myseq{\iv}{\tx^{\el}_{\iv}}, \myseq{\jv}{\uaconst_{\jv}}}}
      }}},\right.\\
    &\ \ \ \left.\myseq\jw{\mterm\parent{\myseq\ii{\tx^{\iwdomain + \jw}_{\ii}}, \myseq\jj{\uaconst_{\jj}}}}\right)
    \end{aligned}
    \\&\explain={($**$)}
    \mterm
    \begin{aligned}[t]
    &\left(\myseq\iw{{
          {\mterm\parent{\myseq\iv{\tx^{\iv \hphantom{+\iwdomain}}_{\iv}}, \myseq\jv{\uaconst_{\jv}}}}
      }},\right.\\
    &\ \ \!\left.\myseq\jw{\mterm\parent{\myseq\ii{\tx^{\iwdomain + \jw}_{\ii}}, \myseq\jj{\uaconst_{\jj}}}}\right)
    \end{aligned}
    \\&\explain={($***$)}
    \begin{aligned}[t]
      &\mterm\left(\myseq\ii{{
          {{\tx^{\ii}_{\ii}}}
      }},\right.\\
      &\ \ \ \left.\myseq\jj{\uaconst_{\jj}}\right)
      = \mtermu\myseq\ii{\tx^{\ii}_{\ii}}
    \end{aligned}
  \end{align*}
  Thus in $\mL+\mL'$ the idempotency law holds, hence it validates
  Copy.  To show that the tensor also validates Copy, we appeal to
  \propositionref{supertheory optimisation inheritance}.

  To prove the statement for Weak Copy, erase the superscript from all
  the variables $\tx^{i}_{i'}$ in the proof. Note how
  every appeal to Copy can be soundly replaced with an appeal to Weak
  Copy. Also note we no longer add any fresh variables in
  the first transition of the calculation.
\end{proof}
}

Our proof consists of two steps. First, we use our assumption on $\mL$
to identify a special form to which all $\uaSignature+\uaSignature'$
can be brought. In the last proof, it was $\mterm(\tx_1, \ldots,
\tx_n, \uaconst_1, \ldots, \uaconst_k)$.  Then we establish the
idempotency law by direct calculation using the idempotency laws in
each component theory. We use this tactic in all our ad-hoc
combination theorems for Copy and Weak Copy.

\begin{theorem}\theoremlabel{unary copy combination}
  Let $\Ax = {\pair\uaSignature\uaEq}$, $\Ax' =
  {\pair{\uaSignature'}{\uaEq}}$ be two presentations such that
    $\Theory\Ax$ and $\Theory{\Ax'}$ validate the  Copy (resp.~Weak Copy)
    optimisation. If $\uaSignature$ assigns arity $1$ to all operation
    symbols, then $\Theory{\parent{\Ax\tensor\Ax'}}$ satisfies the Copy (resp.~Weak
    Copy) optimisation.
\end{theorem}

The proof is straightforward, but technically involved. Therefore we
first illustrate it with an example.  First, a \defterm{unary
  signature} is a signature that assigns to every operation symbol the
arity $1$, i.e., in which all operations are unary. A \defterm{unary
  presentation} is a presentation with a unary signature.  The first
crucial observation is that if $\Ax$ is unary, then every
$\Ax+\Ax'$-term can be separated into an $\Ax'$-term with $\Ax$-terms
substituted for its variables.

For example, let $\uaSignature'$, and
$\uaSignature$ be given by $\set{f' \of 3}$ and $\set{g,h \of 1}$,
respectively. The tensor equation for $g$ and $f'$ in this case is
\[
  g(f'(\tx, \ty, \tz)) = f'(g(\tx), g(\ty), g(\tz))
\]
Using the tensor equations, we can separate any
$\uaSignature+\uaSignature'$-term by cascading the unary
$\uaSignature$ operations towards the variables. For example,
\[
g(f'(\tx, h(\ty), \tz)) = f'(g(\tx), g(h(\ty)), g(\tz))
\]
In this separated form, we have a $\uaSignature'$-term, $f'(\tx, \ty,
\tz)$, in which we substitute the $\uaSignature$-terms $g(\tx)$,
$g(h(\ty))$, $g(\tz)$.

\allowdisplaybreaks
With this observation in place, we prove the theorem by directly
establishing the idempotency law. For example, consider the term
$\mtermu(\tx_1, \tx_2) \definedby f'(\tx_1, g(\tx_2), h(\tx_1))$. We
have:
\begin{align*}
\mtermu(\mtermu(\tx^1_1, \tx^1_2), \mtermu(\tx^2_1, \tx^2_2))
&=
\begin{aligned}[t]
f'(&f'(\tx^1_1, g(\tx^1_2), h(\tx^1_2))),   \\
   &\boxed{g(f'(\tx^2_1, g(\tx^2_2), h(\tx^2_1))),} \\
   &\boxed{h(f'(\tx^1_1, g(\tx^1_2), h(\tx^1_1)))})
\end{aligned}
\\&\explain+={tensor\\equations}
\begin{aligned}[t]
f'(&f'(\tx^1_1, g(\tx^1_2), h(\tx^1_2))),   \\
   &f'(g(\tx^2_1), g(g(\tx^2_2)), g(h(\tx^2_1))), \\
   &f'(h(\tx^1_1), h(g(\tx^1_2)), h(h(\tx^1_1))))
\end{aligned}
\\&\explain+{=}{idempotency\\in $\mL'$}
\begin{aligned}[t]
f'(&\tx^1_1,\\
   &\boxed{g(g(\tx^2_2)),}\\
   &\boxed{h(h(\tx^1_1))})
\explain*={idempotency in $\mL$}
f'(\tx^1_1, g(\tx^2_2), h(\tx^1_2)) = u(\tx^1_1, \tx^2_2)
\end{aligned}
\end{align*}
The full proof generalises these two steps.

{
\newindex\cc{k}{c}
\let\aa\undefined
\newindex\bb{m}{a}
\newindex\bd{m^{\dd}}{a'}
\newindex\dd{\ell}{d}
\newcommand\varseq[1]{i_{#1}}

\begin{lemma}\lemmalabel{unary decomposition}
  Let $\uaSignature$ be a unary signature, and $\uaSignature'$ be any
  other signature. For every $\uaSignature+\uaSignature'$-term
  $\mtermu(\tx_1, \ldots, \tx_{\ccdomain})$ there exist:
  \begin{itemize}
  \item a natural number $\bbdomain$ and a sequence $\varseq{1},
    \ldots, \varseq{\bbdomain}$ from $\set{1, \ldots, \ccdomain}$;
  \item a $\uaSignature'$-term $\mterm(\tx_1, \ldots,
    \tx_{\bbdomain})$; and
  \item $\uaSignature$-terms $\mtermv_1(\tx)$, $\ldots$,
    $\mtermv_{\bbdomain}(\tx)$
  \end{itemize}
  such that $\mL_{\uaSignature}\tensor\mL_{\uaSignature'}$ proves
  \[
  \mtermu(\tx_1, \ldots, \tx_{\ccdomain}) = \mterm(\mtermv_1(\tx_{\varseq 1}),
  \ldots, \mtermv_{\bbdomain}(\tx_{\varseq \bbdomain}))
  \]
\end{lemma}

\begin{proof}
  Given any $\ccdomain$, we show by
  induction that $\mtermu(\tx_1, \ldots, \tx_{\ccdomain})$ satisfies the lemma.

  For $\mtermu(\tx_1, \ldots, \tx_{\ccdomain}) = \tx_{\cc}$, for some $\indexrange\cc$, choose
  $\bbdomain \definedby 1$, $\varseq1 \definedby \cc$, $\mterm(\tx)
  \definedby \tx$, and $\mtermv_1(\tx) \definedby \tx$, and then
  \[
  \mterm(\mtermv_1(\tx_{\varseq1})) = \tx_{\cc} = \mtermu(\tx_1,
  \ldots, \tx_{\ccdomain})
  \]

  Consider any $\mtermu(\tx_1, \ldots, \tx_{\ccdomain}) =
  \mop(\mtermu^{1}, \ldots, \mtermu^{\dddomain})$, such that, for
  every $1 \leq \dd \leq \dddomain$, the
  $\uaSignature+\uaSignature'$-term $\mtermu^{\dd}(\tx_1, \ldots,
  \tx_{\ccdomain})$ satisfies the induction hypothesis.  As $\mop$ is
  in $\uaSignature+\uaSignature'$, we may split into two cases.

  Assume $\mop$ is a $\uaSignature$-operation. Therefore, $\mop$
  is unary, hence $\dddomain = 1$, and $\mtermu = \mop(\mtermu')$,
  where $\mtermu'(\tx_1, \ldots, \tx_{\ccdomain})$ satisfies the
  induction hypothesis, i.e., there exist:
  \begin{itemize}
  \item a natural number $\bbdomain$ and a sequence $\varseq{1},
    \ldots, \varseq{\bbdomain}$ from $\set{1, \ldots, \ccdomain}$;
  \item a $\uaSignature'$-term $\mterm(\tx_1, \ldots,
    \tx_{\bbdomain})$; and
  \item $\uaSignature$-terms $\mtermv_1'(\tx)$, $\ldots$,
    $\mtermv_{\bbdomain}'(\tx)$
  \end{itemize}
  such that $\mL_{\uaSignature}\tensor\mL_{\uaSignature'}$ proves
  \[
  \mtermu'\myseq\cc{\tx_{\cc}} = \mterm'\myseq\bb{\mtermv'(\tx_{\varseq {\bb}})}
  \]
  To establish the induction hypothesis, take $\bbdomain$, $\myseq\bb{\varseq \bb}$, and
  $\mterm\myseq\bb{\tx_{\bb}}$ as themselves, and for every $1 \leq
  \bb \leq \bbdomain$, take $\mtermv_{\bb}(\tx) \definedby
  \mop(\mtermv'_{\bb}(\tx))$. We then have:
  \[
  \mterm\myseq\bb{\mtermv(\tx_{\varseq\bb})}
  =
  \mterm\myseq\bb{\mop(\mtermv'(\tx_{\varseq\bb}))}
  \explain={tensor equations}
  \mop(\mterm\myseq\bb{\mtermv'(\tx_{\varseq\bb})})
  =
  \mtermu\myseq\cc{\tx_{\cc}}
  \]
  Thus, in this case, the induction hypothesis holds.

  Assume $\mop$ is a $\uaSignature'$ operation. Therefore, for every $1
  \leq \dd \leq \dddomain$, there
  exist
  \begin{itemize}
  \item a natural number $\bbdomain^{\dd}$ and a sequence $\varseq{1}^{\dd},
    \ldots, \varseq{\bbdomain^{\dd}}^{\dd}$ from $\set{1, \ldots, \ccdomain}$;
  \item a $\uaSignature'$-term $\mterm^{\dd}(\tx_1, \ldots,
    \tx_{\bbdomain})$; and
  \item a $\uaSignature$-terms $\mtermv_1^{\dd}(\tx)$, $\ldots$,
    $\mtermv_{\bbdomain}^{\dd}(\tx)$
  \end{itemize}
  such that $\mL_{\uaSignature}\tensor\mL_{\uaSignature'}$ proves
  \[
  \mtermu^{\dd}\myseq\cc{\tx_{\cc}} = \mterm^{\dd}\myseq\bd{\mtermv_{\bd}^{\dd}(\tx_{\varseq {\bd}^{\dd}})}
  \]
  We establish the induction hypothesis.
  \begin{itemize}
  \item Take $\bbdomain \definedby
    \sum_{\dd=1}^{\dddomain}\bbdomain^{\dd}$. Denote by $\inj\dd \of
    \set{1, \ldots, \bbdomain^{\dd}} \to \set{1, \ldots, \bbdomain}$
    the canonical injection. For every $\indexrange\dd$, and
    $\indexrange\bd$ take $\varseq{\inj\dd\bd} \definedby
    \varseq\bd^{\dd}$.
  \item Take
    \[
    \mterm\myseq\bb{\tx_{\bb}} \definedby \mop\myseq\dd{\mterm^{\dd}\myseq\bd{\tx_{\inj\dd\bd}}}
    \]
  \item Take, for every $\indexrange\dd$ and $\indexrange\bd$:
    \[
    \mtermv_{\inj\dd\bd}(\tx) \definedby \mtermv^{\dd}_{\bd}(\tx)
    \]
  \end{itemize}
  We then have:
  \begin{align*}
  \mterm\myseq\bb{\mtermv_{\bb}(\tx_{\varseq{\bb}})}
  &=
  \mop\myseq\dd{\mterm^{\dd}\myseq\bd{\boxed{\mtermv_{\inj\dd\bd}(\tx_{\varseq{\inj\dd\bd}})}}}
  \\&=
  \mop\myseq\dd{\boxed{\mterm^{\dd}\myseq\bd{\mtermv^{\dd}_{\bd}(\tx_{\varseq{\bd}^{\dd}})}}}
  \\&\explain={\InductionHypothesisExp}
  \mop\myseq\dd{\mtermu^{\dd}\myseq\cc{\tx_{\cc}}}
  \\&= \mtermu\myseq\cc{\tx_{\cc}}
  \end{align*}
  And the induction hypothesis holds.
\end{proof}

We return to the proof at hand:
\newindex\cv{\ccdomain}{\cc'}
\newindex\bv{\bbdomain}{\bb'}
\begin{proof}[of \theoremref{unary copy combination}]%
  Let $\Ax = {\pair\uaSignature\uaEq}$, $\Ax' =
  {\pair{\uaSignature'}{\uaEq}}$ be two presentations such that
  $\Theory\Ax$ and $\Theory{\Ax'}$ validate the Copy (resp.~Weak Copy)
  optimisation. Assume further that $\uaSignature$ is unary.

  Consider any $\uaSignature+\uaSignature'$-term
  $\mtermu\myseq\cc{\tx_{\cc}}$. By \lemmaref{unary decomposition},
  there exist:
  \begin{itemize}
  \item a natural number $\bbdomain$ and a sequence $\varseq{1},
    \ldots, \varseq{\bbdomain}$ from $\set{1, \ldots, \ccdomain}$;
  \item a $\uaSignature'$-term $\mterm(\tx_1, \ldots,
    \tx_{\bbdomain})$; and
  \item $\uaSignature$-terms $\mtermv_1(\tx)$, $\ldots$,
    $\mtermv_{\bbdomain}(\tx)$
  \end{itemize}
  such that $\mL_{\uaSignature}\tensor\mL_{\uaSignature'}$ proves, and hence
  $\Theory{\parent{\Ax\tensor\Ax'}}$ also proves,
  \[
  \mtermu\myseq\cc{\tx_{\cc}} = \mterm\myseq\bb{\mtermv_{\bb}(\tx_{\varseq \bb})}
  \]

  Calculate:
  \begin{align*}
    \mtermu\myseq\cc{\mtermu\myseq\cv{\tx^{\cc}_{\cv}}}
    &=
    \mtermu\myseq\cc{\hphantom{\mtermv_{\bb}(}\mterm\myseq\bv{\mtermv_{\bv}(\tx^{\cc}_{\varseq\bv})}}
    \\&=
    \mterm\myseq\bb{\boxed{\mtermv_{\bb}\parent{\mterm\myseq\bv{\mtermv_{\bv}(\tx^{\varseq\bb}_{\varseq\bv})}}}}
    \\&\explain={tensor equations}
    \mterm\myseq\bb{{\mterm\myseq\bv{\mtermv_{\bb}(\mtermv_{\bv}(\tx^{\varseq\bb}_{\varseq\bv}))}}}
    \\&\explain={idempotency in $\mL'$}
    \mterm\myseq\bb{\boxed{\mtermv_{\bb}(\mtermv_{\bb}(\tx^{\varseq\bb}_{\varseq\bb}))}}
    \\&\explain={idempotency in $\mL$}
    \mterm\myseq\bb{\mtermv_{\bb}(\tx^{\varseq\bb}_{\varseq\bb})}
    \\&=
    \mtermu\myseq\cc{\tx^{\cc}_{\cc}}
  \end{align*}
  Therefore $\Theory{\parent{\Ax\tensor\Ax'}}$ proves the idempotency
  law. Note that by erasing the superscripts from variables in the
  proof we obtain a proof for the corresponding statement for Weak
  Copy.
\end{proof}
}

The previous proof depended on the ability to push the operations from
$\uaSignature$ deeper into the term, towards the variables. In the
next theorem we depend on the ability to pull them towards the
root of the term.

\begin{theorem}\theoremlabel{absorption copy combination}
  Let $\mL$, $\mL'$ be two theories that validate the Copy (resp.~Weak
  Copy) optimisation. If $\mL$ also validates the Discard
  optimisation, then $\mL\tensor\mL'$ validates the Copy (resp.~Weak
  Copy) optimisation.
\end{theorem}

We first demonstrate how we separate each $\uaSignature+\uaSignature'$-term
when $\Theory{\pair\uaSignature\uaEq}$ validates the Discard
optimisation, i.e., satisfies the absorption law
\[
\mtermu(\tx, \ldots, \tx) = \tx
\]
Consider a theory $\mL$ consisting of two operations $\uaSignature
\definedby {\set{g \of 1, h \of 3}}$ in which the idempotency and
absorption laws hold. Take $\mL'$ to be any theory with a single
binary operation $\mL_{\set{f'\of2}}$ in which the idempotency law
hold. In every $\uaSignature+\uaSignature'$-term we can bubble the
$\uaSignature$-operations towards the root of the term. For example:
\begin{align*}
f'(g(\tx), \boxed{h(\ty, \tz, \ty)})
&\explain={absorption in $\mL$}
f'(g(\tx), g(h(\ty, \tz, \ty)))
\\&\explain={tensor equation}
g(f'(\boxed\tx, h(\ty, \tz, \ty)))
\\&\explain={absorption in $\mL$}
g(\boxed{f'(h(\tx, \tx, \tx), h(\ty, \tz, \ty))})
\\&\explain={tensor equation}
g(h(f'(\tx, \ty), h(\tx, \tz), h(\tx, \ty)))
\end{align*}
Thus we may separate every $\uaSignature+\uaSignature'$-term into a
$\uaSignature$-term substituted with $\uaSignature'$-terms.

With this observation we directly establish the idempotency law. For
example, continuing the previous example, we verify that the term
$\mtermu(\tx_1, \tx_2) = g(h(f'(\tx_1, \tx_2), \tx_1, \tx_2))$ is
idempotent.
\begin{align*}
\mtermu(\mtermu(\tx^1_1, \tx^1_2), \mtermu(\tx^2_1, \tx^2_2))
&=
\begin{aligned}[t]
g(h(&\fbox{$\begin{aligned}[t]
    f'(&g(h(f'(\tx^1_1, \tx^1_2), \tx^1_1, \tx^1_2)),\\
       &g(h(f'(\tx^2_1, \tx^2_2), \tx^2_1, \tx^2_2))),\\
    \end{aligned}$}\\
    &g(h(f'(\tx^1_1, \tx^1_2), \tx^1_1, \tx^1_2)),\\
    &g(h(f'(\tx^2_1, \tx^2_2), \tx^2_1, \tx^2_2))
    ))
\end{aligned}
\\&\explain+={tensor\\equations}
\begin{aligned}[t]
g(h(&\begin{aligned}[t]
     g(h(
         &f'(f'(\tx^1_1, \tx^1_2), f'(\tx^2_1, \tx^2_2)),\\
         &f'(\tx^1_1, \tx^2_1),\\
         &f'(\tx^1_2, \tx^2_2)),
    \end{aligned}\\
    &g(h(f'(\tx^1_1, \tx^1_2), \tx^1_1, \tx^1_2)),\\
    &g(h(f'(\tx^2_1, \tx^2_2), \tx^2_1, \tx^2_2))))
\end{aligned}
\\&\explain+={idempotency\\in $\mL$}
\begin{aligned}[t]
g(h(&\fbox{$f'(f'(\tx^1_1, \tx^1_2), f'(\tx^2_1, \tx^2_2)),$}\\
    &\tx^1_1,\\
    &\tx^2_2))
\end{aligned}
\\&\explain+={idempotency\\in $\mL'$}
\begin{aligned}[t]
g(h(&f'(\tx^1_1, \tx^2_2),\\
    &\tx^1_1,\\
    &\tx^2_2))
\end{aligned}
\\&=
\mtermu(\tx^1_1, \tx^2_2)
\end{align*}
Therefore $\mtermu$ satisfies the idempotency law.

{
\let\aa\undefined
\newindex\dd{\ell}{d}
\newindex\ad{\aadomain^{\dd}}{\aa'}
\newindex\ka{\aadomain_{\kk}}{\aa''}
\newindex\aa{m}{a}
\newindex\kk{\dddomain}{k}
\newindex\dk{\kk}{\dd}
\newcommand\warseq[2]{j^{#1}_{#2}}
\newcommand\zarseq[3]{{\vphantom{j}}^{#1}\!\!j^{#2}_{#3}}
\newcommand\Prop[1]{\Phi_{#1}}
\begin{lemma}\lemmalabel{absorption decomposition for operations}
  Let $\mL = \Theory{\pair{\uaSignature}{\uaEq}}$ be a theory
  validating the Discard optimisation and $\mL'$ be any other theory. Let
  $\mop \of \dddomain$ be any operation in $\mL'$. For every sequence
  of $\uaSignature$-terms $\mtermv^1(\tx_1, \ldots,
  \tx_{\aadomain^1})$, $\ldots$, $\mtermv^{\dddomain}(\tx_1, \ldots,
  \tx_{\aadomain^{\dddomain}})$ there exist:
  \begin{itemize}
  \item a natural number $\aadomain$ and a doubly-indexed sequence
    $\myseq\dd{\myseq\aa{\warseq\dd\aa}}$; and
  \item a $\uaSignature$-term $\mtermv(\tx_1, \ldots, \tx_{\aadomain})$,
  \end{itemize}
  such that
  \begin{itemize}
  \item for all $\indexrange\dd$ and $\indexrange\aa$, $\warseq\dd\aa$
    is in $\set{1, \ldots, \addomain}$; and
  \item $\mL\tensor\mL'$ proves
    \[
      \mop\myseq\dd{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}
      =
      \mtermv\myseq\aa{\mop\myseq\dd{\tx^{\dd}_{\warseq\dd\aa}}}
    \]
  \end{itemize}
\end{lemma}

\begin{proof}
  Consider any $\mL$, $\mL'$, $\mop \of \dddomain$, and
  $\myseq\dd{\mtermv^{\dd}\myseq\ad{\tx_{\ad}}}$ as in the Lemma's
  statement. Denote
  \[
      \mtermu \definedby \mop\myseq\dd{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}
  \] For every $\indexrange\kk$, denote by $\Prop\kk$ the
  following invariant: there exist
  \begin{itemize}
  \item a natural number $\kadomain$ and a doubly-indexed sequence
    $\myseq\dk{\myseq\ka{\zarseq\kk\dd\ka}}$; and
  \item a $\uaSignature$-term $\mtermv_{\kk}(\tx_1, \ldots, \tx_{\kadomain})$,
  \end{itemize}
  such that
  \begin{itemize}
  \item for all $\indexrange\dk$ and $\indexrange\ka$, $\zarseq\kk\dd\ka$
    is in $\set{1, \ldots, \addomain}$; and
  \item $\mL\tensor\mL'$ proves
    \[
      \mtermu
      =
      \mtermv_{\kk}\myseq\ka{\mop\parent{\myseq\dk{\tx^{\dd}_{\zarseq\kk\dk\ka}},
          \tseq[\kk+1]{\dd}{\dddomain}{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}
    \]
  \end{itemize}

  Note that $\Prop0$ holds, as, by taking $\aadomain^0\definedby 1$ and
  $\mterm_0(\tx) \definedby \tx$, the conclusion of $\Prop0$ amounts to
  $\mtermu = \mtermu$.  Also note that $\Prop\dddomain$ is the Lemma's
  statement.  Therefore, it suffices to establish that, for every
  $1\leq\kk<\kkdomain$, $\Prop\kk$ implies $\Prop{\kk+1}$.

  Consider any  $1\leq\kk<\kkdomain$ and assume $\Prop\kk$. Therefore,
  we have some number $\kadomain$, sequence
  $\myseq\dk{\myseq\ka{\zarseq\kk\dd\ka}}$, and term $\mtermv_{\kk}(\tx_1,
  \ldots, \tx_{\kadomain})$ witnessing $\Prop\kk$.

  Take $\aadomain_{\kk+1} \definedby
  \kadomain\times\aadomain^{\kk+1}$. Denote by
  $\prodmorphism{\placeholder}{\placeholder}$ the canonical
  bijection \[
  \prodmorphism\placeholder\placeholder\of\set{1, \ldots, \kadomain}\times\set{1, \ldots,
    \aadomain^{\kk+1}} \isomorphic \set{1, \ldots,
    \aadomain_{\kk+1}}
  \] Take, for every $\indexrange\ka$,
  $1\leq\aa\leq\aadomain^{\kk+1}$, and $\indexrange\dk$,
  \begin{align*}
  \zarseq{\kk+1}{\dk}{\prodmorphism\ka\aa} &\definedby
    \zarseq\kk\dk\ka \\
    \intertext{and, for $\dk = \kk+1$, take:}
  \zarseq{\kk+1}{\kk+1}{\prodmorphism\ka\aa} &\definedby
    \aa
  \end{align*}
  Note that in both cases indeed $\zarseq{\kk+1}\dk\ka \leq
  \aadomain^{\kk}$.
  Finally, take \[
  \mtermv_{\kk+1}\tseq{\aa'}{\aadomain^{\kk+1}}{\tx_{\aa'}}
  \definedby
  \mtermv_{\kk}\myseq\ka{\mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{\tx_{\prodmorphism\ka\aa}}}
  \]

  Calculate, with care:
  \begin{align*}
      &\mtermv_{\kk+1}\tseq{\aa}{\aadomain_{\kk+1}}{\mop\parent{\boxed{\tseq\dk{\kk+1}{\tx^{\dd}_{\zarseq{\kk+1}\dk\aa}}},
          \tseq[\kk+2]{\dd}{\dddomain}{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}
    \\
      &\explain={reindex}
      \mtermv_{\kk+1}\tseq{\aa}{\aadomain_{\kk+1}}{\mop\parent{\myseq\dk{\tx^{\dd}_{{\zarseq{\kk+1}\dk\aa}}},
          \tx^{\dd}_{{\zarseq{\kk+1}\dk\aa}},
          \tseq[\kk+2]{\dd}{\dddomain}{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}
      \\&=
      \mtermv_{\kk}\myseq\ka{\mspace{-30mu}
        \mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{\mspace{-30mu}
            \mop\parent{\myseq\dk{\tx^{\dd}_{\boxed{\zarseq{\kk+1}\dk{\prodmorphism\ka\aa}}}},
              \tx^{\dd}_{\boxed{\zarseq{\kk+1}\dk{\prodmorphism\ka\aa}}},
              \tseq[\kk+2]{\dd}{\dddomain}{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}}
      \\&=
      \mtermv_{\kk}\myseq\ka{
        \boxed{
        \mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{\mspace{-30mu}
            \mop\parent{\myseq\dk{\tx^{\dd}_{{\zarseq{\kk}\dk{\ka}}}},
              \tx^{\dd}_{\aa},
              \tseq[\kk+2]{\dd}{\dddomain}{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}}}
      \\&\explain={tensor\\equations}
      \mtermv_{\kk}\myseq\ka{\mspace{-30mu}
        \mop\parent{\mspace{-7mu}
          \myseq\dk{\boxed{
            \mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{\mspace{-20mu}
                \tx^{\dd}_{{\zarseq{\kk}\dk{\ka}}}}}},
            \mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{\mspace{-22mu}
              \tx^{\dd}_{\aa}
            },
              \tseq[\kk+2]{\dd}{\dddomain}{\boxed{
                \mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{\mspace{-30mu}
                  \mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}\mspace{-7mu}}\mspace{-7mu}}
      \\&\explain={absorption\\law}
      \mtermv_{\kk}\myseq\ka{
        \mop\parent{\myseq\dk{
                \tx^{\dd}_{{\zarseq{\kk}\dk{\ka}}}},
            \boxed{\mtermv^{\kk+1}\tseq{\aa}{\aadomain^{\kk+1}}{
              \tx^{\dd}_{\aa}
            },
              \tseq[\kk+2]{\dd}{\dddomain}{
                  \mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}}
      \\&\explain={reindex}
      \mtermv_{\kk}\myseq\ka{
        \mop\parent{\myseq\dk{
                \tx^{\dd}_{{\zarseq{\kk}\dk{\ka}}}},
              \tseq[\kk+1]{\dd}{\dddomain}{
                  \mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}}}
      \\&\explain={$\Prop\kk$}
      \mtermu
      \end{align*}
  Therefore $\Prop{\kk+1}$ holds.
\end{proof}

Based on this result, we separate arbitrary
$\uaSignature+\uaSignature'$ terms:
\newindex\cc{k}{c}
\newindex\ba{n_{\aa}}{b'}
\newindex\bad{n^{\dd}_{\ad}}{b''}
\newindex\bb{n}{b}
\newcommand\varseq[2]{i_{#2}^{#1}}
\newcommand\uarseq[3]{\vphantom{i}^{#1}\!\!i_{#3}^{#2}}
\begin{lemma}\lemmalabel{absorption decomposition for terms}
  Let $\mL = \Theory{\pair\uaSignature\uaEq}$, $\mL' =
  \Theory{\pair{\uaSignature'}{\uaEq'}}$ be two theories. If $\mL$
  validates the Discard optimisation, then for every
  $\uaSignature+\uaSignature'$-term $\mtermu(\tx_1, \ldots,
  \tx_{\cc})$ there exist:
  \begin{itemize}
  \item a natural number $\aadomain$, a sequence of natural numbers
    $\myseq\aa{\badomain}$, and a doubly-indexed sequence
    $\myseq\aa{\myseq\ba{\varseq\aa\ba}}$ over $\set{1, \ldots,
    \ccdomain}$;
  \item a $\uaSignature$-term $\mtermv(\tx_1, \ldots,
    \tx_{\aadomain})$; and
  \item a sequence of $\uaSignature'$-terms $\myseq\aa{\mterm_{\aa}\myseq\ba{\tx_{\ba}}}$
  \end{itemize}
  such that $\mL\tensor\mL'$ proves:
  \[
  \mtermu(\tx_1, \ldots, \tx_{\ccdomain})
  =
  \mtermv\myseq\aa{\mterm_{\aa}\myseq\ba{\tx_{\varseq\aa\ba}}}
  \]
\end{lemma}
\begin{proof}
  Consider $\mL$ and $\mL'$ as in the Lemma's statement, and any
  natural number $\ccdomain$. We prove the Lemma by induction over terms
  $\mtermu(\tx_1, \ldots, \tx_{\ccdomain})$.

  For $\mtermu(\tx_1, \ldots, \tx_{\ccdomain}) = \tx_i$, take
  $\aadomain \definedby 1$, $\bbdomain^{1}\definedby 1$, $\varseq11
  \definedby i$, $\mtermv(\tx) \definedby \tx$, and $\mterm_1(\tx)
  \definedby \tx$. We indeed have:
  \[
  \mtermv(\mterm_1(\tx_{\varseq11}))
  = \tx_i
  = \mtermu(\tx_1, \ldots, \tx_{\ccdomain})
  \]

  Consider any $\mtermu = \mop\myseq\dd{\mtermu^{\dd}}$ such that, for
  every $\indexrange\dd$, $\mtermu$ satisfies the induction
  hypothesis, i.e., there exist:
  \begin{itemize}
  \item a natural number $\aadomain^{\dd}$, a sequence of natural numbers
    $\myseq\ad{\baddomain}$, and a doubly-indexed sequence
    $\myseq\ad{\myseq\bad{\varseq\ad\bad}}$ over $\set{1, \ldots,
    \ccdomain}$;
  \item a $\uaSignature$-term $\mtermv^{\dd}(\tx_1, \ldots,
    \tx_{\addomain})$; and
  \item a sequence of $\uaSignature'$-terms $\myseq\ad{\mterm^{\dd}_{\ad}\myseq\bad{\tx_{\bad}}}$
  \end{itemize}
  such that $\mL\tensor\mL'$ proves:
  \[
  \mtermu^{\dd}(\tx_1, \ldots, \tx_{\ccdomain})
  =
  \mtermv^{\dd}\myseq\ad{\mterm^{\dd}_{\ad}\myseq\bad{\tx_{\uarseq\dd\ad\bad}}}
  \]
  As $\mop$ is in $\uaSignature+\uaSignature'$, we may split into two
  cases.

  Assume $\mop$ is in $\uaSignature$.
  \begin{itemize}
  \item Take $\aadomain \definedby
    \sum_{\dd=1}^{\dddomain}\addomain$. For every $\indexrange\dd$ and
    $\indexrange\ad$, take $\bbdomain_{\inj\dd\aa} \definedby
    \bbdomain_{\aa}^{\dd}$, and for every $\indexrange\bad$, take
    $\varseq{\inj\dd\aa}{\bad} \definedby \uarseq\dd\aa\bad$.
  \item Take $\mtermv(\tx_1, \ldots, \aadomain) \definedby
    \mop\myseq\dd{\mtermv^{\dd}\myseq\ad{\tx_{\inj\dd\ad}}}$.
  \item For every $\indexrange\dd$ and $\indexrange\ad$, take
    $\mterm_{\inj\dd\ad}(\tx_1, \ldots, \tx_{\baddomain}) \definedby
    \mterm^{\dd}_{\ad}\myseq\bad{\tx_{\bad}}$.
  \end{itemize}
  Calculate:
  \[
    \mtermv\myseq\aa{\mterm_{\aa}\myseq\ba{\tx_{\varseq\aa\ba}}}
    \begin{aligned}[t]
      &=
      \mop\myseq\dd{
        \mtermv^{\dd}\myseq\ad{
          \boxed{\mterm_{\inj\dd\ad}}\tseq\bad{\bbdomain_{\inj\dd\ad}}{
            \tx_{\boxed{\varseq{\inj\dd\ad}\bad}}}}}
      \\
      \\&=
      \mop\myseq\dd{\boxed{
        \mtermv^{\dd}\myseq\ad{
          \mterm^{\dd}_{\ad}\tseq\bad{\bbdomain_{\inj\dd\ad}}{
            \tx_{\uarseq\dd\ad\bad}}}}}
      \\&\explain={\InductionHypothesisExp}
      \mop\myseq\dd{\mtermu^{\dd}}
      =
      \mtermu
    \end{aligned}
  \]
  Thus we established the induction hypothesis in this case.

  Assume $\mop$ is in $\uaSignature'$. We invoke \lemmaref{absorption
    decomposition for operations}, and deduce there exist:
  \begin{itemize}
  \item a natural number $\aadomain$ and a doubly-indexed sequence
    $\myseq\dd{\myseq\aa{\warseq\dd\aa}}$; and
  \item a $\uaSignature$-term $\mtermv(\tx_1, \ldots, \tx_{\aadomain})$,
  \end{itemize}
  such that
  \begin{itemize}
  \item for all $\indexrange\dd$ and $\indexrange\aa$, $\warseq\dd\aa$
    is in $\set{1, \ldots, \addomain}$; and
  \item $\mL\tensor\mL'$ proves
    \[
      \mop\myseq\dd{\mtermv^{\dd}\myseq\ad{\tx^{\dd}_{\ad}}}
      =
      \mtermv\myseq\aa{\mop\myseq\dd{\tx^{\dd}_{\warseq\dd\aa}}}
    \]
  \end{itemize}

  To establish the induction hypothesis,
  \begin{itemize}
    \item
    Take $\aadomain$ as $\aadomain$ from \lemmaref{absorption
    decomposition for operations}. For every $\indexrange\aa$, take $\badomain \definedby
    \sum_{\dd=1}^{\dddomain}\bbdomain^{\dd}_{\warseq\dd\aa}$. For
    every $1\leq\bb\leq\bbdomain^{\dd}_{\warseq\dd\aa}$, take $\varseq\aa{\inj\dd\bb} \definedby
    \uarseq\dd{\warseq\dd\aa}\bb$, and indeed
    $\varseq\aa{\inj\dd\bb}$ is in $\set{1, \ldots, \ccdomain}$.
  \item
    Take $\mtermv(\tx_1, \ldots, \tx_{\aadomain})$ as the same $\mtermv$
    from \lemmaref{absorption decomposition for operations}.
  \item
    For every $\indexrange\aa$, take:
    \[
    \mterm_{\aa}\myseq\ba{\tx_{\ba}} \definedby
    \mop\myseq\dd{\mterm^{\dd}_{\warseq\dd\aa}\tseq\bb{\bbdomain^{\dd}_{\warseq\dd\aa}}{\tx_{\inj\dd\bb}}}
    \]
  \end{itemize}
  Calculate:
  \[
  \mtermv\myseq\aa{
    \boxed{\mterm_{\aa}\myseq\ba{\tx_{\varseq\aa\ba}}}}
  \begin{aligned}[t]
    &=
    \mtermv\myseq\aa{
      \mop\myseq\dd{
        \mterm^{\dd}_{\warseq\dd\aa}\tseq\bb{\bbdomain^{\dd}_{\warseq\dd\aa}}{
          \tx_{\boxed{\varseq\aa{\inj\dd\bb}}}}}
    }
    \\
    \\&=
    \mtermv\myseq\aa{
      \mop\myseq\dd{
        \mterm^{\dd}_{\warseq\dd\aa}\tseq\bb{\bbdomain^{\dd}_{\warseq\dd\aa}}{
          \tx_{\uarseq\dd{\warseq\dd\aa}\bb}}}
    }
    \\
    \\&\explain={\lemmaref{absorption decomposition for operations}}
    \mop\myseq\dd{
      \boxed{
      \mtermv^{\dd}\myseq\ad{
        \mterm^{\dd}_{\ad}\myseq\bad{
          \tx_{\uarseq\dd{\ad}\bad}}}
    }}
    \\&\explain={\InductionHypothesisExp}
    \mop\myseq\dd{
      \mtermu^{\dd}
    } = \mtermu
  \end{aligned}
  \]
  Thus the induction hypothesis holds in this case too.
\end{proof}

We are ready to prove our theorem:
\newindex\cv{\ccdomain}{\cc'}
\newindex\av{\aadomain}{\aa'}
\newindex\bav{\bbdomain_{\av}}{\bb''}
\newindex\bva{\bbdomain_{\aa}}{\bb''}
\begin{proof}[of \theoremref{absorption copy combination}]%
  Consider theories $\mL = \Theory{\pair\uaSignature\uaEq}$,
  $\mL' = \Theory{\pair{\uaSignature'}{\uaEq'}}$ that validate the
  Copy optimisation, and assume $\mL$ also validates the Discard
  optimisation. Consider any
  $\uaSignature+\uaSignature'$-term $\mtermu(\tx_1, \ldots,
  \tx_{\ccdomain})$.

  By \lemmaref{absorption decomposition for terms} there exist:
  \begin{itemize}
  \item a natural number $\aadomain$, a sequence of natural numbers
    $\myseq\aa{\badomain}$, and a doubly-indexed sequence
    $\myseq\aa{\myseq\ba{\varseq\aa\ba}}$ over $\set{1, \ldots,
    \ccdomain}$;
  \item a $\uaSignature$-term $\mtermv(\tx_1, \ldots,
    \tx_{\aadomain})$; and
  \item a sequence of $\uaSignature'$-terms $\myseq\aa{\mterm_{\aa}\myseq\ba{\tx_{\ba}}}$
  \end{itemize}
  such that $\mL\tensor\mL'$ proves:
  \[
  \mtermu(\tx_1, \ldots, \tx_{\ccdomain})
  =
  \mtermv\myseq\aa{\mterm_{\aa}\myseq\ba{\tx_{\varseq\aa\ba}}}
  \]

  Calculate:
  \[
  \mtermu\myseq\cc{\mtermu\myseq\cv{\tx^{\cc}_{\cv}}}
  \begin{aligned}[t]
    &=
    \mtermu\myseq\cc{
      \mtermv\myseq\aa{\mterm_{\av}\myseq\bav{\tx^{\cc}_{\varseq\av\bav}}}
    }
    \\&=
    \mtermv\myseq\aa{
      \boxed{
        \mterm_{\aa}\myseq\ba{
          \mtermv\myseq\av{
            \mterm_{\av}\myseq\bav{
              \tx^{\varseq\aa\ba}_{\varseq\av\bav}}}}
    }}
    \\&\explain={tensor equations}
    \mtermv\myseq\aa{
      \mtermv\myseq\av{
        \mterm_{\aa}\myseq\ba{
          \mterm_{\aa}\myseq\bav{\tx^{\varseq\aa\ba}_{\varseq\av\bav}}}
    }}
    \\&\explain={idempotency\\in $\mL$}
    \mtermv\myseq\aa{\boxed{
        \mterm_{\aa}\myseq\ba{
          \mterm_{\aa}\myseq\bva{\tx^{\varseq\aa\ba}_{\varseq\aa\bva}}}}
    }
    \\&\explain={idempotency\\in $\mL'$}
    \mtermv\myseq\aa{
        \mterm_{\aa}\myseq\ba{
          \tx^{\varseq\aa\ba}_{\varseq\aa\ba}}
    }
    \\&=
    \mtermu\myseq\cc{\tx^{\cc}_{\cc}}
  \end{aligned}
  \]
  Thus $\mL\tensor\mL'$ validates the Copy optimisation.  Note that by
  erasing the superscripts from variables in the proof we obtain a
  proof for the corresponding statement for Weak Copy.
\end{proof}
}

Finally, we consider the Unique optimisation:
\begin{theorem}\theoremlabel{unique combination}
Let $\mL = \Theory{\pair\uaSignature\uaEq}$ be a theory.  Then $\mL$
validates the Unique optimisation if and only if every
nullary operation in $\uaSignature$ commutes with every operation in
$\uaSignature$.
\end{theorem}

The above condition, stated explicitly, requires that, for every
$\uaconst \of 0$ and $\mop \of n$ in $\uaSignature$, $\mL$ proves
\[
\mop(\uaconst, \ldots, \uaconst) = \uaconst
\]
In particular, for every two nullary operations $\uaconst$, $\uaconst'$, we
have $\uaconst = \uaconst'$.

\begin{proof}
  The `only if' implication is immediate. For the converse, first note
  that if $\uaSignature$ contains no nullary operations, then it has
  no constant terms and the algebraic condition for the Unique
  optimisation is vacuously true.

  Assume $\uaSignature$ contains at least one nullary operation
  $\uaconst_0 \of 0$. We prove by induction that, for every nullary
  term $\mtermu$ with no variables, $\mL$ proves $\mtermu =
  \uaconst_0$.

  Assume $\mtermu = \mop(\mtermu^1, \ldots, \mtermu^{\ell})$ where,
  for all $1 \leq d \leq \ell$,
  $\mL$ proves $\mtermu^{d} = \uaconst_0$. Therefore:
  \[
  \mterm = \mop(\uaconst_0, \ldots, \uaconst_0) = \uaconst_0
  \]
  Therefore, $\mL$ proves all nullary terms equal to each other, and
  $\mL$ validates the Unique optimisation.
\end{proof}