
\subsection{Commute}

We now define commutation of catches.

\begin{Idefinition}[catch-commute]
We extend $<->$ to operate on catches, as defined below.

We can break the rules down into 3 classes: Those where the patches are
unrelated, and simply commute freely; those where the patches are the
result of a conflicting merge, and the conflicts gets reshuffled when
they commute; and a fail case for anything else.

% XXX To do:
Currently we don't give the commute rules for anything involving inverse
conflictors. We don't believe that those rules will raise any new
problems, though.

\subsubsection*{Unrelated}

First the simple non-conflicted patch case:\\
$\pair{\patch{p}}{\patch{q}} <-> \pair{\patch{q'}}{\patch{p'}}
    \textrm{ if } \pair{p}{q} <-> \pair{q'}{p'}$

\begin{Iexplanation}
If our catches just wrap up patches,
then they commute like the underlying patches.
\end{Iexplanation}

Now commute a conflictor past a patch, where everything goes
smoothly:\\
$\pair{\conflictor{\seq{r}}{X}{y}}{\patch{q}} <->
 \pair{\patch{q'}}{\conflictor{\seq{r}'}{X'}{y'}}
    \textrm{ if } \begin{array}[t]{@{}l@{}}
                  \pair{\seq{r}}{q} <-> \pair{q'}{\seq{r}'}\\
                  \pair{q^}{y} -> \single{y'}\\
                  \pair{q^}{X} -> \single{X'}\\
                  \end{array}$

\begin{Iexplanation}
OK, now things start to look a little more daunting, but if you work
through it then it's really not that bad. We start off with this
situation:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midr}(-2,0)
    \pointdef{r}(0,0)
    \pointdef{midQ}(2,0)
    \pointdef{Q}(4,0)
    \pointdef{midy}(1,1.5)
    \pointdef{y}(2,3)
    \pointdef{midXa}(0.5,-1.5)
    \pointdef{Xa}(1,-3)
    \pointdef{Xb}(2,-3)
    \pointdef{Xc}(3,-3)
    %
    \point{\O,\r,\Q}
    \arrlab{\O}{\midr}{\r}{tc}{$\seq{r}$}
    \arrlab{\r}{\midQ}{\Q}{tc}{$q$}
    \arrlab{\r}{\midy}{\y}{br}{$y$}
    \arrlab{\r}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\r}{\Xb}
    \arrow\lin{\r}{\Xc}
\end{mfpic}\\
Now, we want to commute the two patches, so clearly we need to commute
$\seq{r}$ and $q$, which leaves us here:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midQ}(-2,0)
    \pointdef{Q}(0,0)
    \pointdef{midQR}(2,0)
    \pointdef{QR}(4,0)
    \pointdef{midR}(-2.5,3)
    \pointdef{R}(0,4)
    \pointdef{midRQ}(2.5,3)
    \pointdef{midY}(1,5.5)
    \pointdef{Y}(2,7)
    \pointdef{midXa}(0.5,2.5)
    \pointdef{Xa}(1,1)
    \pointdef{Xb}(2,1)
    \pointdef{Xc}(3,1)
    %
    \point{\O,\Q,\R,\QR}
    \arrlab{\O}{\midQ}{\Q}{tc}{$q'$}
    \arrlab{\Q}{\midQR}{\QR}{tc}{$\seq{r}'$}
    \arrlab{\O}{\midR}{\R}{br}{$\seq{r}$}
    \arrlab{\R}{\midRQ}{\QR}{bl}{$q$}
    \arrlab{\O}{\midR}{\R}{br}{$\seq{r}$}
    \arrlab{\R}{\midRQ}{\QR}{bl}{$q$}
    \arrlab{\R}{\midY}{\Y}{br}{$y$}
    \arrlab{\R}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\R}{\Xb}
    \arrow\lin{\R}{\Xc}
\end{mfpic}\\
The $q' \seq{r}'$ is what we want, but the $y$ and $X$ that should be
part of the conflictor have become detached from it. Let's rearrange the
diagram a bit to make it clearer what we need to do:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midQ}(-2,0)
    \pointdef{Q}(0,0)
    \pointdef{midQR}(2,0)
    \pointdef{QR}(4,0)
    \pointdef{midQi}(5.5,3)
    \pointdef{Qi}(8,4)
    \pointdef{midY}(9,5.5)
    \pointdef{Y}(10,7)
    \pointdef{midXa}(8.5,2.5)
    \pointdef{Xa}(9,1)
    \pointdef{Xb}(10,1)
    \pointdef{Xc}(11,1)
    %
    \point{\O,\Q,\QR,\Qi}
    \arrlab{\O}{\midQ}{\Q}{tc}{$q'$}
    \arrlab{\Q}{\midQR}{\QR}{tc}{$\seq{r}'$}
    \arrlab{\QR}{\midQi}{\Qi}{br}{$q^$}
    \arrlab{\Qi}{\midY}{\Y}{br}{$y$}
    \arrlab{\Qi}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\Qi}{\Xb}
    \arrow\lin{\Qi}{\Xc}
\end{mfpic}\\
So we need to add $q^$ into the context of $y$ and $X$. We have two ways
of doing this: We can simply add $q^$ to the context, which cannot fail,
or we can commute $q^$ past $y$ and $X$, which can. Being able to
commute patches is good, so if possible we would prefer to use the
option that doesn't fail; but is that possible?

First, let's consider $y$, and for the purpose of contradiction, let us
assume that the catch commute can suceed even if $q^$ cannot be commuted
past $y$.

Suppose we have two repos $\patch{s}$ and $\patch{t}$, where $s$ and $t$
conflict. We merge them, giving us
$\patch{s} \conflictor{s^}{\mkset{:s}}{:t}$, and then record another
patch $\patch{u}$, giving us
$\patch{s} \conflictor{s^}{\mkset{:s}}{:t} \patch{u}$. We choose $u$
such that $\pair{s^}{u} <-> \pair{u'}{s'^}$ and
$\pair{t^}{u} <-> \fail$.
Then we can commute $\patch{u}$ past both catches, giving us
$\patch{u} \patch{s'} \conflictor{s'^}{\mkset{:s'}}{u^:t}$. So far so
good.

But before we commute $u$ past, we can first commute $s$ and $t$, giving
us $\patch{t} \conflictor{t^}{\mkset{:t}}{:s} \patch{u}$. But now it is
not possible to commute $u$ past!

This isn't what we want, so we now know that we must require that the
commute past $y$ succeeds. This explains why we require
$\pair{q^}{y} -> \single{y'}$, and gets us to here:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midQ}(-2,0)
    \pointdef{Q}(0,0)
    \pointdef{midQR}(2,0)
    \pointdef{QR}(4,0)
    \pointdef{midQi}(6.5,1.5)
    \pointdef{Qi}(8,4)
    \pointdef{midY}(5,1.5)
    \pointdef{Y}(6,3)
    \pointdef{midXa}(8.5,2.5)
    \pointdef{Xa}(9,1)
    \pointdef{Xb}(10,1)
    \pointdef{Xc}(11,1)
    %
    \point{\O,\Q,\QR,\Qi}
    \arrlab{\O}{\midQ}{\Q}{tc}{$q'$}
    \arrlab{\Q}{\midQR}{\QR}{tc}{$\seq{r}'$}
    \arrlab{\QR}{\midQi}{\Qi}{tl}{$q^$}
    \arrlab{\QR}{\midY}{\Y}{br}{$y'$}
    \arrlab{\Qi}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\Qi}{\Xb}
    \arrow\lin{\Qi}{\Xc}
\end{mfpic}\\
Now we need to work out whether we need to require that $q^$ commutes
past $X$ or not. Again, for the purpose of contradiction, assume that we
don't require this.

Suppose we have three repos $\patch{s}$, $\patch{t}$ and $\patch{u}$,
where $s$ conflicts with $t$ and $u$. Then we merge these
three repos to give us something like
\[\patch{s}
  \conflictor{s^}{\mkset{:s}}{:t}
  \conflictor{\nopatches}{\mkset{:s}}{:u}\]
Next record another patch $v$, which commutes with everything except for
$s^$. So now we have
\[\patch{s}
  \conflictor{s^}{\mkset{:s}}{:t}
  \conflictor{\nopatches}{\mkset{:s}}{:u}
  \patch{v}\]
Now, we can commute $v$ past the $u$ conflictor, but not the $t$
conflictor (as it cannot commute past the effect, $s^$):
\[\patch{s}
  \conflictor{s^}{\mkset{:s}}{:t}
  \patch{v}
  \conflictor{\nopatches}{\mkset{v^:s}}{:u'}\]
Likewise, we can first commute the $t$ and $u$ conflictors and then
commute $v$ past the $t$ conflictor, but not the $u$ conflictor:
\[\patch{s}
  \conflictor{s^}{\mkset{:s}}{:u}
  \patch{v}
  \conflictor{\nopatches}{\mkset{v^:s}}{:t'}\]
By unpulling patches from these last two repos, we get repos with the
patches $\mkset{s,t,v}$ and $\mkset{s,u,v}$, but it is not possible to
make a repo containing the patches $\mkset{s,v}$. This causes problems
when we try to merge these two repos, as explained in
Appendix~\ref{sec:named_patch_motivation}, so this is also not something
that we want to allow.

This explains why we require $\pair{q^}{X} -> \single{X'}$,
and brings us to our destination:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midQ}(-2,0)
    \pointdef{Q}(0,0)
    \pointdef{midQR}(2,0)
    \pointdef{QR}(4,0)
    \pointdef{midY}(5,1.5)
    \pointdef{Y}(6,3)
    \pointdef{midXa}(4.5,-1.5)
    \pointdef{Xa}(5,-3)
    \pointdef{Xb}(6,-3)
    \pointdef{Xc}(7,-3)
    %
    \point{\O,\Q,\QR}
    \arrlab{\O}{\midQ}{\Q}{tc}{$q'$}
    \arrlab{\Q}{\midQR}{\QR}{tc}{$\seq{r}'$}
    \arrlab{\QR}{\midY}{\Y}{br}{$y'$}
    \arrlab{\QR}{\midXa}{\Xa}{tr}{$X'$}
    \arrow\lin{\QR}{\Xb}
    \arrow\lin{\QR}{\Xc}
\end{mfpic}
\end{Iexplanation}

Next we have the case where the patch and conflictor start off the other
way round:\\
$\pair{\patch{p}}{\conflictor{\seq{r}}{X}{y}} <->
 \pair{\conflictor{\seq{r}'}{X'}{y'}}{\patch{p'}}
    \textrm{ if } \begin{array}[t]{@{}l@{}}
                  \pair{p}{\seq{r}} <-> \pair{\seq{r}'}{p'}\\
                  \pair{p'}{X} -> \single{X'}\\
                  \pair{p'}{y} -> \single{y'}\\
                  \end{array}$

\begin{Iexplanation}
This is similar to the previous case. We start off here:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midP}(-2,0)
    \pointdef{P}(0,0)
    \pointdef{midr}(2,0)
    \pointdef{r}(4,0)
    \pointdef{midy}(5,1.5)
    \pointdef{y}(6,3)
    \pointdef{midXa}(4.5,-1.5)
    \pointdef{Xa}(5,-3)
    \pointdef{Xb}(6,-3)
    \pointdef{Xc}(7,-3)
    %
    \point{\O,\P,\r}
    \arrlab{\O}{\midP}{\P}{tc}{$p$}
    \arrlab{\P}{\midr}{\r}{tc}{$\seq{r}$}
    \arrlab{\r}{\midy}{\y}{br}{$y$}
    \arrlab{\r}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\r}{\Xb}
    \arrow\lin{\r}{\Xc}
\end{mfpic}\\
As before, we start off by commuting $p$ and $\seq{r}$:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midr}(-2,0)
    \pointdef{r}(0,0)
    \pointdef{midP}(2,0)
    \pointdef{P}(4,0)
    \pointdef{midy}(5,1.5)
    \pointdef{y}(6,3)
    \pointdef{midXa}(4.5,-1.5)
    \pointdef{Xa}(5,-3)
    \pointdef{Xb}(6,-3)
    \pointdef{Xc}(7,-3)
    %
    \point{\O,\r,\P}
    \arrlab{\O}{\midr}{\r}{tc}{$\seq{r}'$}
    \arrlab{\r}{\midP}{\P}{tc}{$p'$}
    \arrlab{\P}{\midy}{\y}{br}{$y$}
    \arrlab{\P}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\P}{\Xb}
    \arrow\lin{\P}{\Xc}
\end{mfpic}\\
We now need to get $X$ and $y$ into the right context, and as we want
commute to be self-inverting, we'd better require that the commute pasts
succeed, as we did in the previous case:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(-4,0)
    \pointdef{midr}(-2,0)
    \pointdef{r}(0,0)
    \pointdef{midP}(2,0)
    \pointdef{P}(4,0)
    \pointdef{midy}(1,1.5)
    \pointdef{y}(2,3)
    \pointdef{midXa}(0.5,-1.5)
    \pointdef{Xa}(1,-3)
    \pointdef{Xb}(2,-3)
    \pointdef{Xc}(3,-3)
    %
    \point{\O,\P,\r}
    \arrlab{\O}{\midr}{\r}{tc}{$\seq{r}'$}
    \arrlab{\r}{\midP}{\P}{tc}{$p'$}
    \arrlab{\r}{\midy}{\y}{br}{$y'$}
    \arrlab{\r}{\midXa}{\Xa}{tr}{$X'$}
    \arrow\lin{\r}{\Xb}
    \arrow\lin{\r}{\Xc}
\end{mfpic}
\end{Iexplanation}

And the last and most complex of the unrelated cases, commuting a
conflictor past another conflictor:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\conflictor{\seq{r} \seq{s}}{W}{x}}{\conflictor{\seq{t}}{Y}{z}} <->
 \pair{\conflictor{\seq{r} \seq{t}'}{\seq{s}' Y}{z'}}%
      {\conflictor{\seq{s}'}{\seq{t}^ W}{x'}}\\
    \textrm{ if } \begin{array}[t]{@{}l@{}}
                  \names{\seq{r}^} \subseteq \names{Y}\\
                  \names{\seq{s}^} \cap \names{Y} = \emptyset\\
                  \pair{\seq{s}}{\seq{t}} <-> \pair{\seq{t}'}{\seq{s}'}\\
                  x <X> \seq{t} z\\
                  \forall w \in W . (w <X> \seq{t} z)\\
                  \forall y \in Y . (x <X> \seq{t} y)\\
                  \pair{\seq{t}^}{x} -> \single{x'}\\
                  \pair{\seq{s}'}{z} -> \single{z'}\\
                  \end{array}
 \end{array}$

\begin{Iexplanation}
The number of rules and side conditions grows, but if we take it one
step at a time we can get through this! We start here:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{O}(0,0)
    \pointdef{midr}(2,0)
    \pointdef{r}(4,0)
    \pointdef{mids}(6,0)
    \pointdef{s}(8,0)
    \pointdef{midt}(10,0)
    \pointdef{t}(12,0)
    \pointdef{midx}(8.5,1.5)
    \pointdef{x}(9,3)
    \pointdef{midWa}(8.5,-1.5)
    \pointdef{Wa}(9,-3)
    \pointdef{Wb}(10,-3)
    \pointdef{Wc}(11,-3)
    \pointdef{midz}(12.5,1.5)
    \pointdef{z}(13,3)
    \pointdef{midYa}(12.5,-1.5)
    \pointdef{Ya}(13,-3)
    \pointdef{Yb}(14,-3)
    \pointdef{Yc}(15,-3)
    %
    \point{\O,\r,\s,\t}
    \arrlab{\O}{\midr}{\r}{tc}{$\seq{r}$}
    \arrlab{\r}{\mids}{\s}{tc}{$\seq{s}$}
    \arrlab{\s}{\midt}{\t}{tc}{$\seq{t}$}
    \arrlab{\s}{\midx}{\x}{br}{$x$}
    \arrlab{\t}{\midz}{\z}{br}{$z$}
    \arrlab{\s}{\midWa}{\Wa}{tr}{$W$}
    \arrow\lin{\s}{\Wb}
    \arrow\lin{\s}{\Wc}
    \arrlab{\t}{\midYa}{\Ya}{tr}{$Y$}
    \arrow\lin{\t}{\Yb}
    \arrow\lin{\t}{\Yc}
\end{mfpic}\\
The first thing to note is that we have $\seq{r} \seq{s}$ where you probably
expected $\seq{t}$. What we have done here is to break up the effect of the
first conflictor into those patches that \emph{both} conflictors
conflict with, $\seq{r}$, and those patches that only the first conflictor
conflicts with, $\seq{s}$. $\seq{r}$ won't move; it'll become part of the $z$
conflictor after the commute, thus maintaining the invariant that the
first conflictor that conflicts with a patch reverts it. The first two
side conditions just say that we have correctly split up the effect of
the first conflictor.

With that out of the way, let's start to look at how we perform the
commute. We start, as usual, by commuting the effects of the two
patches. Now comes the difficult part: Where do we need to check for
conflicts?

First let's consider the repo $\patch{p} \patch{q}$, where $q$ depends
on $p$, and the repo $\patch{u}$, where $p$ conflicts with $u$. If we
merge these as
$\patch{p} \patch{q} \conflictor{q^p^}{\mkset{:p, p:q}}{:u}$ then we
cannot commute the $p$ and $q$ catches. Therefore, in the alternate
merge
$\patch{u} \conflictor{u^}{\mkset{:u}}{:p} \conflictor{}{\mkset{:u}}{p:q}$
the catches shouldn't commute either. Therefore we need to check that
$p$ and $p:q$ don't conflict, or in general, $x <X> \seq{t} z$.

Now let us consider whether we need to worry about $z$ and $W$
conflicting. Suppose first we record $o$, $p$ and $q$, which conflict,
in separate repos, and then merge them, giving us
\[ \patch{o}
   \conflictor{o^}{\mkset{:o}}{:p}
   \conflictor{}{\mkset{:o, :p}}{:q} \]
Next record $u$ (which commutes with $o$, $p$ and $q$) and $v$ (which
commutes with $q$ but not $o$ or $p$) in
two copies of this repo, and merge, giving us
\[ \patch{o}
   \conflictor{o^}{\mkset{:o}}{:p}
   \conflictor{}{\mkset{:o, :p}}{:q}
   \patch{u}
   \conflictor{u^}{\mkset{:u}}{:v}\]
Now, we can commute $u$ and $v$, giving us
\[ \patch{o}
   \conflictor{o^}{\mkset{:o}}{:p}
   \conflictor{}{\mkset{:o, :p}}{:q}
   \patch{v}
   \conflictor{v^}{\mkset{:v}}{:u}\]
and by the earlier rules we know that the $q$ catch does not commute
with the $v$ catch. But we could also have commuted $q$ and $u$, giving
us
\[ \patch{o}
   \conflictor{o^}{\mkset{:o}}{:p}
   \patch{u}
   \conflictor{}{\mkset{:o', :p'}}{:q'}
   \conflictor{u^}{\mkset{:u}}{:v}\]
Now we musn't be allowed to commute the $q$ and $v$ conflictors, and we
must therefore, in the general case, check that $z$ and $W$ do not
conflict. This gives us the $\forall w \in W . (w <X> \seq{t} z)$ side
condition, and by considering commuting the patches back the other way
we must also have $\forall y \in Y . (x <X> \seq{t} y)$.

If this is satisfied then we know that the commute pasts will succeed.

This only leaves conflicts between $W$ and $Y$. However, I claim that it
is not possible to get into a situation where there are any conflicts
here; Any patch in $Y$ would have had to be commuted past the $x$
conflictor at some point in order to get into this situation, and
therefore cannot conflict with $W$.
% XXX Prove that properly!
\end{Iexplanation}

\subsubsection*{Conflicted merge}

Now we get to the interesting cases. First, if we have a patch, and a
conflictor that has only conflicted with that patch, then they swap
places:\\
$\pair{\patch{p}}{\conflictor{p^}{\mkset{:p}}{:q}} <->
 \pair{\patch{q}}{\conflictor{q^}{\mkset{:q}}{:p}}$

\begin{Iexplanation}
This should make sense if you consider that the result of merging two
conflicting patches $p$ and $q$ is
$\patch{p} \conflictor{p^}{\mkset{:p}}{:q}$
({\ie}, from right to left, the second catch represents $q$, conflicts
with $p$, and as it is the first patch to conflict with $p$ it has to
invert $p$'s effect), or equivalently
$\patch{q} \conflictor{q^}{\mkset{:p}}{:q}$.
\end{Iexplanation}

If we have two conflictors, but the one on the right only conflicts with
the one on the left, then it becomes a patch after it has commuted:\\
$\pair{\conflictor{\seq{r}}{X}{y}}%
      {\conflictor{\nopatches}{\mkset{y}}{\seq{r}^:q}} <->
 \pair{\patch{q}}{\conflictor{q^ \seq{r}}{\mkset{\seq{r}^:q} \union X}{y}}$

\begin{Iexplanation}
This case comes up when you merge a patch $q$ with a conflictor
representing $p$. If $q$ is the first in the resulting sequence then it
is still just $\patch{q}$, and the $q$ conflictor must record that it
conflicts with $p$. On the other hand, if $p$ comes after $p$ then it
must also turn into a conflictor, as it needs to record that is has
conflicted with $p$.
\end{Iexplanation}

And the inverse of the previous case:\\
$\pair{\patch{p}}{\conflictor{p^ \seq{r}}{\mkset{\seq{r}^:p} \union X}{y}} <->
 \pair{\conflictor{\seq{r}}{X}{y}}%
      {\conflictor{\nopatches}{\mkset{y}}{\seq{r}^:p}}$

\begin{Iexplanation}
This is just the inverse of the previous case.
\end{Iexplanation}

And now the case where both are conflictors, and conflict with each
other:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\conflictor{\seq{r} \seq{s}}{W}{x}}
      {\conflictor{\seq{t}}{\mkset{\seq{t}^x} \union Y}{z}} <->
 \pair{\conflictor{\seq{r} \seq{t}'}{\seq{s}'Y}{\seq{s}'z}}%
      {\conflictor{\seq{s}'}{\mkset{z} \union \seq{t}^W}{\seq{t}^x}}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{\seq{s}}{\seq{t}} <-> \pair{\seq{t}'}{\seq{s}'}\\
                        \names{\seq{r}^} \subseteq \names{Y}\\
                        \names{\seq{s}^} \cap \names{Y} = \emptyset\\
                        \end{array}
 \end{array}$

\begin{Iexplanation}
In this case we just move the conflict from one to the other.
The splitting of the effect of the $z$ conflictor into two parts is the
same as we saw earlier, in the ``unrelated'' conflict-conflictor
commute.
\end{Iexplanation}

\subsubsection*{Fail}

Finally, if none of the above hold, then\\
$\pair{c}{d} <-> \fail$
\end{Idefinition}

\start{conjecture}{catch-commute-conflicting-patches-succeeds}
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d e) \in \repos .\\
         d \in \catchConflicts{e} => (\pair{d}{e} <-> \pair{\_}{\_})
 \end{array}$

\begin{Iexplanation}
If two patches conflict (and thus, were merged at some point in the
past), then they can be commuted.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{catch-commute-unique}
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d e) \in \repos,
         r \in (\catches \times \catches) \cup \mkset{\fail},
         s \in (\catches \times \catches) \cup \mkset{\fail} .\\
 (\pair{d}{e} <-> r) \wedge (\pair{d}{e} <-> s) => r = s
 \end{array}$
\begin{Iexplanation}
This states that Axiom~\ref{axiom:patch-commute-unique}, {\ie} that
the result of a commute is unique, holds for catches too.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{catch-commute-valid}
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d e) \in \repos, d' \in \catches, e' \in \catches .\\
 (\pair{d}{e} <-> \pair{e'}{d'}) => (\seq{c} e' d') \in \repos
 \end{array}$
\begin{Iexplanation}
If we have a valid repository (one in which the invariants are all
satisfied) and we commute two catches, then the result is also a valid
repository.
\end{Iexplanation}
\end{Iconjecture}

\begin{Iconjecture}[catch-commute-self-inverse]
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d e) \in \repos,
 \forall d' \in \catches, e' \in \catches .\\
 (\pair{d}{e} <-> \pair{e'}{d'}) <=> (\pair{e'}{d'} <-> \pair{d}{e})
 \end{array}$
\begin{Iexplanation}
This states that Axiom~\ref{axiom:patch-commute-self-inverse},
{\ie} that successful commute is self-inverting, holds for catches too.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{catch-commute-square}
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d) \in \repos, (\seq{c} e) \in \repos,
 \forall d' \in \catches, e' \in \catches .\\
 (\pair{d^}{e} <-> \pair{e'}{d'^}) <=> (\pair{e^}{d} <-> \pair{d'}{e'^})
 \end{array}$
\begin{Iexplanation}
This states that Axiom~\ref{axiom:patch-commute-square},
{\ie} that commute squares can be rotated, holds for catches too.
% XXX Why don't we start with cde?
\end{Iexplanation}
\end{Iconjecture}

\start{definition}{catch-conflicts}
If $\forall (\seq{c} d) \in \repos$ and $(\seq{c} e) \in \repos$,
We say $d$ conflicts with $e$ if and only if
$\pair{d^}{e} <-> \fail$.
\begin{Iexplanation}
XXX
% This mirrors Definition~\ref{definition:patch-conflicts}.
\end{Iexplanation}
\end{Idefinition}

\start{conjecture}{catch-commute-preserves-effect}
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d e) \in \repos,
 \forall d' \in \catches, e' \in \catches .\\
    (\pair{d}{e} <-> \pair{e'}{d'}) => \effectof{de} = \effectof{e'd'}
 \end{array}$
\begin{Iexplanation}
XXX
% This states that Axiom~\ref{axiom:patch-commute-preserves-effect},
% {\ie} that commute preserves total effect, holds for catches too.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{catch-commute-associates}
$\begin{array}[t]{@{}r@{~}l@{}}
 \multicolumn{2}{@{}l@{}}{
 \forall (\seq{c} d e f) \in \repos,
         d_e \in \catches, d_f \in \catches, d_{ef} \in \catches,
         e_d \in \catches, e_f \in \catches, e_{df} \in \catches,
         f_d \in \catches, f_e \in \catches, f_{de} \in \catches .}\\
    &(\pair{e}{f}           <-> \pair{f_e}{e_f})   \wedge
     (\pair{d}{e}           <-> \pair{e_d}{d_e}) \wedge
     (\pair{d_e}{f}         <-> \pair{f_d}{d_{ef}})\\
 <=>&(\pair{e_d}{f_d}       <-> \pair{f_{de}}{e_{df}}) \wedge
     (\pair{e_{df}}{d_{ef}} <-> \pair{d_f}{e_f}) \wedge
     (\pair{f_{de}}{d_f}    <-> \pair{d}{f_e})
 \end{array}$
\begin{Iexplanation}
This states that Axiom~\ref{axiom:patch-commute-associates},
{\ie} that commute associates, holds for catches too. Here's the diagram
again for convenience:\\
\begin{mfpic}{0}{3.6}{-0.8}{2.8}
    \tlabelsep{4pt}
    \pointdef{DEF}(0,0)
    \pointdef{DFE}(0,2)
    \pointdef{FDE}(1.8,2.8)
    \pointdef{FED}(3.6,2)
    \pointdef{EFD}(3.6,0)
    \pointdef{EDF}(1.8,-0.8)
    \point{\DEF,\DFE,\EDF,\EFD,\FDE,\FED}
    \tlabel[tr]\DEF{def}
    \tlabel[br]\DFE{dfe}
    \tlabel[bc]\FDE{fde}
    \tlabel[bl]\FED{fed}
    \tlabel[tl]\EFD{efd}
    \tlabel[tc]\EDF{edf}
    \lin{\DEF}{\DFE}
    \lin{\DFE}{\FDE}
    \lin{\FDE}{\FED}
    \lin{\FED}{\EFD}
    \lin{\EFD}{\EDF}
    \lin{\EDF}{\DEF}
\end{mfpic}
\end{Iexplanation}
\end{Iconjecture}

