%\[\tikzfig{gateUsurgateU}\ \to\ \tikzfig{bsUhUbbs}\]
%and putting $L'''$ (and ${L'''}^{-1}$) in stair form again, we get a diagram with $\nopbs(D)+\noneg(D)-1$ PBS and no negations, which is equivalent to $D$.
\end{proof}

\section{Existence\Acom{construction ?} of the normal form: proof of Theorem \ref{existenceNF}}\label{proofexistenceNF}

We prove %this
by structural induction on $D$ that it can be put in normal form.
%\Acom{dans les swaps et BS, décider si on met le label du haut à l'intérieur ou à l'extérieur quand on a la place}
\Acom{harmoniser la taille des labels : pour l'instant 0.9 dans stikzfig, 0.925 dans sgtikzfig et 1 dans ntikzfig}

\begin{itemize}
\item \ntikzfig{diagrammevide-s}, \ntikzfig{cfilcourtR-s}, \ntikzfig{cfilcourtB-s}, \sgtikzfig{cnegRB}, \sgtikzfig{cnegBR}, \sgtikzfig{cgateUR}, \sgtikzfig{cgateUB}, \stikzfig{beamsplitterNRwB}, \stikzfig{beamsplitterRNBw}, \stikzfig{swapRR-s-label}, \stikzfig{swapBB-s-label}, \stikzfig{swapRB-s-label} and \stikzfig{swapBR-s-label} are already in normal form.

\item The normal forms of \stikzfig{filcourt}, \stikzfig{beamsplitterwBNR}, \stikzfig{beamsplitterBwRN}, \stikzfig{beamsplitter}, \stikzfig{beamsplitterNRRN-s-label}, \stikzfig{beamsplitterRNNR-s-label}, \stikzfig{beamsplitterNNBB-s-label} and \stikzfig{beamsplitterBBNN-s-label} are given by Equation \eqref{bsbssplitmerge}, \eqref{bsxcol}, \eqref{xbscol}, \eqref{bsbigebre}, \eqref{bsnrrn}, \eqref{bsrnnr}, \eqref{bsnnbb} and \eqref{bsbbnn} respectively.

\item The normal forms of \sgtikzfig{neg}, \sgtikzfig{gateU}, \stikzfig{swap}, \stikzfig{swapnoirR-s-label}\nolinebreak, \stikzfig{swapRnoir-s-label}, \stikzfig{swapnoirB-s-label} and \stikzfig{swapBnoir-s-label} are obtained as follows:\bigskip

\begin{xtabular}{RCL}\tikzfig{neg}&\eqeqref{bsbssplitmerge}&\tikzfig{negbsRBbs}\\\\

\begin{xtabular}{RCL}\tikzfig{gateU}&\eqeqref{bsbssplitmerge}&\tikzfig{UbsRBbs}\\\\
\[\tikzfig{swap}\ \eqeqref{bsbssplitmerge}\ \tikzfig{swapNF}\]
\[\tikzfig{swapnoirR-label}\ \eqeqref{bsbssplitmerge}\ \tikzfig{swapnoirRNF-label}\]
\[\tikzfig{swapRnoir-label}\ \eqeqref{bsbssplitmerge}\ \tikzfig{swapRnoirNF-label}\]
\[\tikzfig{swapnoirB-label}\ \eqeqref{bsbssplitmerge}\ \tikzfig{swapnoirBNF-label}\]
\[\tikzfig{swapBnoir-label}\ \eqeqref{bsbssplitmerge}\ \tikzfig{swapBnoirNF-label}\]

\item If $D=D_1\oplus D_2$, then by induction hypothesis there exist two diagrams in normal form $N_1$ and $N_2$ such that $\CPBS\vdash D_1=N_1$ and $\CPBS\vdash D_2=N_2$. Then $\CPBS\vdash D=N_1\oplus N_2$ and it is easy to see that $N_1\oplus N_2$ is in normal form.

\item If $D=D_2\circ D_1$, then by induction hypothesis, let $N_1$ and $N_2$ be two diagrams in normal form such that $\CPBS\vdash D_1=N_1$ and $\CPBS\vdash D_2=N_2$. Let us decompose them as $N_1=M_1\circ P_1\circ F_1\circ G_1\circ S_1$ and $N_2=M_2\circ P_2\circ F_2\circ G_2\circ S_2$, following \cref{defNFcoloree}. One has $\CPBS\vdash D=N_2\circ N_1=M_2\circ P_2\circ F_2\circ G_2\circ S_2\circ M_1\circ P_1\circ F_1\circ G_1\circ S_1$. \Cref{bsbsmergesplit} makes $S_2\circ M_1$ equal to a parallel composition of red and blue identity wires, so that $\CPBS\vdash D=M_2\circ P_2\circ F_2\circ G_2\circ P_1\circ F_1\circ G_1\circ S_1$. By naturality of the swap, one has $G_2\circ P_1=P_1\circ G'_2$, where $G'_2$ is a parallel composition of %sequences of
coloured non-identity gates and identity wires (obtained by permuting the %sequences
generators\Acom{trouver une meilleure formulation ?} of $G_2$). One has $\eqref{neguRB}\vdash G'_2\circ F_1=F_1\circ G''_2$, where $G''_2$ is still a parallel composition of %sequences of gates
coloured non-identity gates and identity wires (obtained by changing some colours in $G'_2$). Hence, $\CPBS\vdash D=M_2\circ P_2\circ F_2\circ P_1\circ F_1\circ G''_2\circ G_1\circ S_1$. By naturality of the swap, one has $F_2\circ P_1=P_1\circ F'_2$, where $F'_2$ is a parallel composition of coloured identities and negations (obtained by permuting $F_2$). One has $\eqref{negnegRBR},\eqref{negnegBRB}\vdash F'_2\circ F_1=F''$, where $F''$ is still a parallel composition of coloured identities and negations. Finally, $\eqref{fusionUVR},\eqref{idboxR}\vdash G''_2\circ G_1=G'''$, where $G'''$  is still a parallel composition of coloured non-identity gates and identity wires.\Acom{mettre ça avant ?} Thus,  $\CPBS\vdash D=M_2\circ (P_2\circ P_1)\circ F''\circ G'''\circ S_1$, with $S_1$, $G'''$, $F''$, $(P_2\circ P_1)$ and $M_2$ respectively of the forms described in \cref{defNFcoloree}, so that their composition is in normal form. This gives us the result.

\item If $D=Tr_\vtype(D'):X\to Y$, then by induction hypothesis, let $N'$ be a diagram in normal form such that $\CPBS\vdash D'=N'$. Let us decompose it as $N'=M'\circ P'\circ F'\circ G'\circ S'$, following \cref{defNFcoloree}. Since $N'$ is of type $X\oplus\vtype\to Y\oplus\vtype$, $S'$ (resp. $M'$) is of the form $S\oplus\ntikzfig{cfilcourtR-s}$ (resp. $M\oplus\ntikzfig{cfilcourtR-s}$) where $S$ (resp. $M$) is a parallel composition of coloured identity wires and copies of $\xstikzfig{beamsplitterNRwB}$ (resp. $\xstikzfig{beamsplitterRNBw}$). Using the structural congruence, one can write $P'$ in the form $\ntikzfig{PsurfilR}$ or $\ntikzfig{permswaprougeenbas}$, where $P$, or $P_1$, $P_2$ and $P_3$, are permutations of the wires. In the first case, $Tr_\vtype(N')$ can be written in the form \[\ntikzfig{SGFPMsurbouclevideUR}\] with $S$, $G$, $F$ and $M$ of the forms demanded by \cref{defNFcoloree} (note that $F'$ cannot have a negation on its bottom wire since this would prevent $N'$ from being of type $X\oplus\vtype\to Y\oplus\vtype$), so that $\eqref{bouclevideUR}\vdash Tr_\vtype(N')=\ntikzfig{SGFPM}$, which is in normal form. In the second case, $Tr_\vtype(N')$ can be written in the form \[\ntikzfig{SGFP1P2P3M}\] where $\xntikzfig{negpotentielRa}$ is either $\ntikzfig{cfilcourtR-s}$ or $\xntikzfig{cnegRB}$. Then by yanking, one can write it in the form \[\ntikzfig{SGFP1P2P3Metire}.\] Finally, by naturality of the swap, one can slide the gate $U$ and the possible negation through $P_1$, then by \cref{neguRB}, one can move the gates $U$ to the other side of $F$, which gives us a diagram in normal form. \Acom{changer ``one'' en ``we'' ?}

\item The case $D=Tr_\htype(D'):X\to Y$ is analogous to the previous case. %The use of \cref{bouclevideRnonbornee,bouclevideUR} is %adapted as follows:
%replaced by the following sequence of transformations:
Equations \eqref{neguRB} and \eqref{bouclevideUR} are replaced by the following variants:
\begin{equation}\label{bouclevideUB}\ptikzfig{bouclevideUB-label}{0.65}{0.74286}{1}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
\begin{equation}\label{neguBR}\tikzfig{UnegBR-label}\ =\ \tikzfig{negBRU-label}\end{equation}
which are derived from the equations of \cref{axiomsCPBS} as follows:\medskip

\begin{xtabular}{RCL}\ptikzfig{bouclevideUB-label}{0.65}{0.74286}{1}&\eqeqref{negnegBRB}&\ptikzfig{bouclevideUBnegneg-label}{0.65}{0.74286}{1}\\\\

%\[\ptikzfig{bouclevideU1BUmB-label}{0.65}{0.74286}{1}\ \eqeqref{negnegBRB}\ \ptikzfig{bouclevideU1BUmBnegneg-label}{0.65}{0.74286}{1}\ =\ \ptikzfig{bouclevidenegU1BUmBneg-label}{0.65}{0.74286}{1}\]
%\[\qquad\qquad\eqdeuxeqref{neguRB}{negnegRBR}\ \ptikzfig{bouclevideU1RUmR-label}{0.65}{0.74286}{1}\ \eqeqref{bouclevideRnonbornee}\ \ptikzfig{bouclevideU1RsursurbouclevideUmR-label}{0.65}{0.74286}{1}\ \eqeqref{bouclevideUR}\ \ptikzfig{diagrammevide}{1}{0.5}{0.5}\]
%while %the uses of \cref{neguRB} are %adapted as follows:
%each use of \cref{neguRB} is
%replaced by the following sequence of transformations:
%\[\tikzfig{negBRU-label}\ \eqeqref{negnegRBR}\ \tikzfig{negUnegnegBRBR}\ \eqeqref{neguRB}\ \tikzfig{negnegUnegBRBR}\ \eqeqref{negnegBRB}\ \tikzfig{UnegBR-label}\]

\begin{xtabular}{RCL}\tikzfig{negBRU-label}&\eqeqref{negnegRBR}&\tikzfig{negUnegnegBRBR}\\

\item If $D=Tr_\top(D'):X\to Y$, then by induction hypothesis, let $N'$ be a diagram in normal form such that $\CPBS\vdash D'=N'$. $Tr_\top(N')$ can be written in the form $\ntikzfig{tracebsNRwBNsecondebsRNBw}$, which by dinaturality and \cref{bsbsmergesplit}, can be transformed into $\ntikzfig{traceRBNseconde}$. It suffices then to apply the previous two cases to get a diagram in normal form.
\end{itemize}

\section{Derivation of equations %\eqref{mergegatesRB}
\eqref{fusionUVB} to \eqref{mergegatesBB}}\label{preuveequationsgateoptproc}
\Acom{mettre au bon endroit}

To prove \cref{fusionUVB}, we have:\medskip

\begin{xtabular}{RCL}
\tikzfig{gateUgateVbleu-t}&\eqdeuxeqref{negnegBRB}{neguRB}&\tikzfig{neggateUgateVrougeneg-t}\\\\
\end{xtabular}\medskip

To prove \cref{fusionUV}, we have:\medskip

\begin{xtabular}{RCL}
\tikzfig{gateUgateVbis}&\eqdeuxeqref{bsbssplitmerge}{ubscol}&\tikzfig{NbsRBgateUgateVRBbsN}\\\\
\end{xtabular}\medskip

To prove \cref{mergegatesRB}, we have:\medskip

\begin{xtabular}{RCL}
\tikzfig{gateURsurgateUB-label}&\eqeqref{bsbsmergesplit}&\tikzfig{bsbsgateURsurgateUB}\\\\
\end{xtabular}\medskip

To prove \cref{mergegatesBR}, we have:\medskip

\begin{xtabular}{RCL}
\tikzfig{gateUBsurgateUR-label}&=&\tikzfig{xgateURsurgateUBx}\\\\
\end{xtabular}\medskip

To prove \cref{mergegatesRR}, we have:\medskip

\begin{xtabular}{RCL}
\tikzfig{gateURsurgateUR-label}&\eqdeuxeqref{negnegRBR}{neguRB}&\tikzfig{gateURsurneggateUBneg}\\\\
\end{xtabular}\medskip

To prove \cref{mergegatesBB}, we have:\medskip

\begin{xtabular}{RCL}
\tikzfig{gateUBsurgateUB-label}&\eqdeuxeqref{negnegBRB}{neguRB}&\tikzfig{neggateURnegsurgateUB}\\\\
\end{xtabular}

\section{PGT procedure}\label{PBSoptprocillustree}

\subsection{Full description of the procedure}

\begin{enumerate}
\setcounter{enumi}{-1}
\item During all the procedure, every time there are two consecutive negations, we remove them using Equation \eqref{negnegRBR}, \eqref{negnegBRB} or their all-black version:
\begin{equation}\label{negnegnoir}\tikzfig{negneg}\ =\ \tikzfig{filcourt}\end{equation}
\item Deform $D_0$ to put it in the form \eqref{snail} with $P$ gate-free. The goal of the following steps is to put $P$ in %the desired
stair form.
\item Split all %saturated beam splitters (that is,
PBS of the form $\stikzfig{abbeamsplitter}$ %)
into combinations of %the unsaturated beam splitters
$\stikzfig{beamsplitterNRwB}$, $\stikzfig{beamsplitterwBNR}$, $\stikzfig{beamsplitterRNBw}$ and $\stikzfig{beamsplitterBwRN}$, using %\cref{bsbigebre,bsnrrn,bsrnnr,bsnnbb,bsbbnn}
Equations \eqref{bsbigebre} to \eqref{bsbbnn}.
\item As long as there are two PBS connected by a black wire, with possibly black negations on this wire, %cancel them together. More precisely, %use Equations \eqref{bsxcol} and/or \eqref{xbscol} if necessary,
cancel the negations together using %the all-black variant of Equations \eqref{negnegRBR} and \eqref{negnegBRB}:
%\begin{equation}\label{negnegnoir}\tikzfig{negneg}\ =\ \tikzfig{filcourt}\end{equation}
Equation \eqref{negnegnoir},
push the possibly remaining negation out using Equation \eqref{nbscol}, and cancel the PBS together using Equation \eqref{bsbsmergesplit}. It may be necessary to flip the PBS upside down using \eqref{bsxcol} and/or \eqref{xbscol} in order to be able to apply Equations \eqref{nbscol} and \eqref{bsbsmergesplit}. Note also that to cancel the two PBS together one may have to use dinaturality:
\[\ptikzfig{tracebsNRwBgapbsRNBw-raccourci}{0.5}{0.8}1\ =\ \ptikzfig{traceBdanstraceRgap-label-raccourci}{0.5}{0.8}1\]
%\[\tikzfig{tracebsNRwBgapbsBwRN}\ =\ \tikzfig{traceBdanstraceRgapswap-label}\]
When there are not two such PBS anymore, all black wires are connected to at least one side of $P$ (possibly through negations), and the PBS are connected together with red and blue wires with possibly negations on them.
%\item %Remove all double negations
%Reduce all chains of negations using Equations \eqref{negnegRBR}, \eqref{negnegBRB} and \eqref{negnegnoir}%their all-black version%, or the following variant: \begin{tabularx}{11em}{X}\\[-5em]\begin{equation}\tikzfig{negneg}\ =\ \stikzfig{filcourt}\end{equation}\\[-4em]\end{tabularx}
%, to zero or one negation.
\item Remove all loops using %Equation \eqref{bouclevideR} and its %blue or black version
%following variants:\\
%\begin{equation}\label{bouclevideB}\tikzfig{bouclevideB-label}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
%&\begin{equation}\label{bouclevide}\tikzfig{bouclevide}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
%&\begin{equation}\label{bouclevideneg}\tikzfig{bouclevideneg}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
the following equations:
\begin{equation}\label{bouclevideR}\tikzfig{bouclevideR-label}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
\begin{equation}\label{bouclevideB}\tikzfig{bouclevideB-label}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
\begin{equation}\label{bouclevide}\tikzfig{bouclevide}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
\begin{equation}\label{bouclevideneg}\tikzfig{bouclevideneg}\ =\ \ptikzfig{diagrammevide}1{0.5}{0.5}\end{equation}
Note that since $D_0$ is query-optimal, there cannot be loops containing gates at this point.
%\Acom{rajouter la boucle noire avec negation}
\item %By deforming $P$ and using Equations \eqref{bsxcol} and \eqref{xbscol} wherever necessary,
Deform $P$ to put it in the form \eqref{stairs} with $\sigma_1$ and $\sigma_2$ being wire permutations and the $C_i$ being trace-free and connected. Up to additional deformation of $P$ to reorder the input and output wires of the $C_i$, and to using Equations \eqref{bsxcol} and \eqref{xbscol}, the $C_i$ are each of %the form
%\[\tikzfig{escalierbsnegpotentielsIO}, \tikzfig{escalierbsnegpotentielsO}, \tikzfig{escalierbsnegpotentielsI}\text{ or }\tikzfig{escalierbsnegpotentiels},\]
one of the following forms:
\[%\tikzfig{escalierbsnegpotentielsIO}
\tikzfig{escalierbsnegpotentielsIOalenvers}\qquad\quad\ \ \tikzfig{escalierbsnegpotentielsO}\quad\ \ \]
\[\tikzfig{escalierbsnegpotentielsI}\quad\quad\tikzfig{escalierbsnegpotentiels}\]
where $\ptikzfig{negpotentiel-m}{0.4}{0.8}1$ is either %$\ptikzfig{filcourt}{0.4}{0.8}1$
$\ntikzfig{cfilcourt-s}$ or %$\ptikzfig{neg}{0.4}{0.8}1$
$\sgtikzfig{cneg}$ with $a\in\{\vtype,\htype\}$, $\stikzfig{bs3pattessymsplit}$ is either $\stikzfig{beamsplitterNRwB}$ or $\stikzfig{beamsplitterwBNR}$ and $\stikzfig{bs3pattessymmerge}$ is either $\stikzfig{beamsplitterRNBw}$ or $\stikzfig{beamsplitterBwRN}$.
\item\label{pushnegationsillustree} Remove the negations in the middle of the $C_i$ by pushing them to the bottom by means of Equation \eqref{nbscol} and its following variants (%that can be summarised by
all of the form ``a three-wire PBS with a negation on one of the three wires is equal to this PBS reflected vertically with negations on the other two wires''):
%\begin{equation}\label{nbswBNRcomm}\tikzfig{nbswBNR}\ =\ \tikzfig{bsNRwBnn}\end{equation}\\
%\begin{equation}\label{bsRNBwncomm}\tikzfig{bsRNBwn}\ =\ \tikzfig{nnbsBwRN}\end{equation}&
%\begin{equation}\label{bsBwRNncomm}\tikzfig{bsBwRNn}\ =\ \tikzfig{nnbsRNBw}\end{equation}\\
%\begin{equation}\label{bsNRwBnhcomm}\tikzfig{bsNRwBnh}\ =\ \tikzfig{nbswBNRnb}\end{equation}&
%%\begin{equation}\tikzfig{bsNRwBnb}\ =\ \tikzfig{nbswBNRnh}\end{equation}\\
%\begin{equation}\label{bswBNRnhcomm}\tikzfig{bswBNRnh}\ =\ \tikzfig{nbsNRwBnb}\end{equation}%&
%%\begin{equation}\tikzfig{bswBNRnb}\ =\ \tikzfig{nbsNRwBnh}\end{equation}
%\begin{equation}\label{nhbsRNBwcomm}\tikzfig{nhbsRNBw}\ =\ \tikzfig{nbbsBwRNn}\end{equation}&
%%\begin{equation}\tikzfig{nbbsRNBw}\ =\ \tikzfig{nhbsBwRNn}\end{equation}\\
%\begin{equation}\label{nhbsBwRNcomm}\tikzfig{nhbsBwRN}\ =\ \tikzfig{nbbsRNBwn}\end{equation}%&
%%\begin{equation}\tikzfig{nbbsBwRN}\ =\ \tikzfig{nhbsRNBwn}\end{equation}
\begin{equation}\label{nbswBNRcomm}\tikzfig{nbswBNR}\ =\ \tikzfig{bsNRwBnn}\end{equation}
\begin{equation}\label{bsRNBwncomm}\tikzfig{bsRNBwn}\ =\ \tikzfig{nnbsBwRN}\end{equation}
\begin{equation}\label{bsBwRNncomm}\tikzfig{bsBwRNn}\ =\ \tikzfig{nnbsRNBw}\end{equation}
\begin{equation}\label{bsNRwBnhcomm}\tikzfig{bsNRwBnh}\ =\ \tikzfig{nbswBNRnb}\end{equation}
%\begin{equation}\tikzfig{bsNRwBnb}\ =\ \tikzfig{nbswBNRnh}\end{equation}
\begin{equation}\label{bswBNRnhcomm}\tikzfig{bswBNRnh}\ =\ \tikzfig{nbsNRwBnb}\end{equation}
%\begin{equation}\tikzfig{bswBNRnb}\ =\ \tikzfig{nbsNRwBnh}\end{equation}
\begin{equation}\label{nhbsRNBwcomm}\tikzfig{nhbsRNBw}\ =\ \tikzfig{nbbsBwRNn}\end{equation}
%\begin{equation}\tikzfig{nbbsRNBw}\ =\ \tikzfig{nhbsBwRNn}\end{equation}
\begin{equation}\label{nhbsBwRNcomm}\tikzfig{nhbsBwRN}\ =\ \tikzfig{nbbsRNBwn}\end{equation}
%\begin{equation}\tikzfig{nbbsBwRN}\ =\ \tikzfig{nhbsRNBwn}\end{equation}
%\item Step \ref{pushnegationsillustree} may have created (black) double negations on the sides of the $C_i$. Remove them using the all-black variant of Equations \eqref{negnegRBR} and \eqref{negnegBRB}.
\item %Transform each $C_i$, which is now, u
Up to deforming $P$ to flip the $C_i$ upside down, and to using Equations \eqref{bsxcol} and \eqref{xbscol} wherever necessary, the $C_i$ are each of one of the following forms:%\\
\begin{eqnabc}\label{formeRR}\tikzfig{escalierbs3pattesRR}\end{eqnabc}

\begin{eqnabc}\label{formeBRI}\tikzfig{escalierbs3pattesBRI}\end{eqnabc}

\begin{eqnabc}\label{formeBRO}\tikzfig{escalierbs3pattesBRO}\end{eqnabc}

\begin{eqnabc}\label{formeN}\tikzfig{escalierbs3pattesN}\end{eqnabc}

\begin{eqnabc}\label{formeBB}\tikzfig{escalierbs3pattesBB}\end{eqnabc}
Transform each of them into one of the five kind of stairs depicted in Definition \ref{defNMF}, depending on its type:
%Merge the beam splitters to put the $D_i$ in the forms given in \cref{defNMF}, as follows, depending on their form:
\begin{itemize}
\item If $C_i$ is of type $\top^{\oplus k}\oplus\vtype\to\vtype\oplus\top^{\oplus k}$, $\htype\oplus\top^{\oplus k}\oplus\vtype\to\top^{\oplus k+1}$ or $\top^{\oplus k+1}\to\htype\oplus\top^{\oplus k}\oplus\vtype$ for some $k$, that is, if it is of the form \eqref{formeRR}, \eqref{formeBRI} or \eqref{formeBRO}, then repeatedly apply \cref{bsnrrn} to put it in the form \ptikzfig{escalierbsrouge-label}{0.5}{0.8}1\nolinebreak, \ptikzfig{escalierbsrougemerge-label}{0.5}{0.8}1 or\smallskip \ptikzfig{escalierbsrougemergeinverse-label}{0.5}{0.8}1 respectively.
\item If $C_i$ is of the form \eqref{formeBB}, then repeatedly apply the following equation:
\begin{equation}\label{bsxNBBN}\tikzfig{defbsxNBBN}\ =\ \tikzfig{bsxNBBN-label}\end{equation}
to put it in the form \ptikzfig{escalierbsbleu-label}{0.5}{0.8}1.
\item If $C_i$ is of the form \eqref{formeN}, then repeatedly apply the following variant of Equation \eqref{bsbsmergesplit}:
\begin{equation}\label{bsbsmergesplitRBBR}
\tikzfig{RBbsNbsBR}\ =\ \tikzfig{swapRB-label}
\end{equation}
and Equation \eqref{bsbigebre}, as follows% in order to put it in the form \ptikzfig{escalierbsnoir}{0.5}{0.8}1:

\begingroup
\par
\parshape0
\begin{xtabular}{RCL}
\tikzfig{motifhautformeN}&\eqeqref{bsbsmergesplitRBBR}&\tikzfig{motifhautformeNmodifie}\\\\
\end{xtabular}\medskip\par
\endgroup
%\Scom{dire qu'il faut utiliser C.12 à la fin}
and finally apply \cref{bsbssplitmerge} once, in order to put it in the form \ptikzfig{escalierbsnoir}{0.5}{0.8}1\nolinebreak.

\end{itemize}
%To do so, deform it and apply Equations \eqref{bsxcol} and \eqref{xbscol} appropriately, and repeatedly apply the appropriate equation among \eqref{bsnrrn}, \eqref{bsrnnr}, \eqref{bsnnbb}, and a variant of \eqref{bsbigebre}. This gives us $D_1$.
This gives us the desired diagram $D_1$ and finishes the procedure.
\end{enumerate}

\subsection{Derivation of the ancillary equations}

It remains to derive Equations \eqref{negnegnoir} to \eqref{bsbsmergesplitRBBR} from the equations of Figure \ref{axiomsCPBS}. In order to %be able to use some of these equations as lemmas in the derivation of others,
benefit from some dependencies between the derivations, we treat the equations in the following order: \eqref{nbswBNRcomm}, \eqref{negnegnoir}, \eqref{bouclevideB}, \eqref{bouclevide}, \eqref{bsbsmergesplitRBBR}, \eqref{bouclevideneg}, \eqref{bsRNBwncomm}, \eqref{bsBwRNncomm}, \eqref{bsNRwBnhcomm}, \eqref{bswBNRnhcomm}, \eqref{nhbsRNBwcomm}, \eqref{nhbsBwRNcomm}, \eqref{bsxNBBN}.

For Equation \eqref{nbswBNRcomm}, the derivation is the following:\medskip

\begin{xtabular}{RCL}\tikzfig{nbswBNR}&\eqeqref{bsxcol}&\tikzfig{nbsNRwBx}\\\\

For Equation \eqref{negnegnoir}:\medskip

\begin{xtabular}{RCL}\tikzfig{negneg}&\eqeqref{bsbssplitmerge}&\tikzfig{nnbsRBbs}\\\\

For Equation \eqref{bouclevideR}:\medskip

\begin{xtabular}{RCL}\tikzfig{bouclevideR-label}&\eqeqref{idboxR}&\tikzfig{bouclevideIR-label}\\\\

For Equation \eqref{bouclevideB}:\medskip

\begin{xtabular}{RCL}\tikzfig{bouclevideB-label}&\eqeqref{negnegBRB}&\tikzfig{bouclevidenegnegBRB}\\\\

For Equation \eqref{bouclevide}:\medskip

\begin{xtabular}{RCL}\tikzfig{bouclevide}&\eqeqref{bsbssplitmerge}&\tikzfig{bouclevidebsRBbs}\\\\

For Equation \eqref{bsbsmergesplitRBBR}:\medskip

\begin{xtabular}{RCL}\tikzfig{RBbsNbsBR}&\eqeqref{bsxcol}&\tikzfig{RBbsbsRBx}\\\\

For Equation \eqref{bouclevideneg}:\medskip

\begin{xtabular}{RCL}\tikzfig{bouclevideneg}&\eqeqref{bsbssplitmerge}&\tikzfig{bouclevidenegbsRBbs}\\\\

For Equation \eqref{bsRNBwncomm}:\medskip

\begin{xtabular}{RCL}\tikzfig{bsRNBwn}&\eqeqref{bsbssplitmerge}&\tikzfig{RBbsnNbsRBbs}\\\\

For Equation \eqref{bsBwRNncomm}:\medskip

\begin{xtabular}{RCL}\tikzfig{bsBwRNn}&=&\tikzfig{xxbsBwRNn}\\\\

For Equation \eqref{bsNRwBnhcomm}:\medskip

\begin{xtabular}{RCL}\tikzfig{bsNRwBnh}&\eqeqref{negnegBRB}&\tikzfig{bsNRwBnhnbnb}\\\\

For Equation \eqref{bswBNRnhcomm}:\medskip

\begin{xtabular}{RCL}\tikzfig{bswBNRnh}&\eqeqref{negnegRBR}&\tikzfig{bswBNRnhnbnb}\\\\

For Equation \eqref{nhbsRNBwcomm}:\medskip

\begin{xtabular}{RCL}\tikzfig{nhbsRNBw}&\eqeqref{negnegBRB}&\tikzfig{nhnbnbbsRNBw}\\\\

For Equation \eqref{nhbsBwRNcomm}:\medskip

\begin{xtabular}{RCL}\tikzfig{nhbsBwRN}&\eqeqref{negnegRBR}&\tikzfig{nhnbnbbsBwRN}\\\\

For Equation \eqref{bsxNBBN}:\medskip

\begin{xtabular}{RCL}\tikzfig{defbsxNBBN}&=&\tikzfig{defbsNNBBx}\\\\

\end{document}