First, we implement the Kronecker $\delta$-function, the $g$-rules for a crossing $(s,i,j)$, and the $g$-rules for a list of crossings $X$:

\nbpdfInput{Snips/Implementation/31.pdf}
We then let \verb$Xl$ be the three crossings in the left-hand-side of the R3b move, as in Figure~\ref{fig:R3}, we let \verb$Al$ be the $A^l$ term of~\eqref{eq:ABC}, and we let \verb$lhs$ be the result of applying the $g$-rules for the crossings in \verb$Xl$ to \verb$Al$. We print only a ``\verb$Short$'' version of \verb$lhs$ because the full thing would cover about 2.5 pages: 

\nbpdfInput{Snips/Implementation/32.pdf}
\nbpdfOutput{Snips/Implementation/33.pdf}
We do the same for $A^r$, except this time, without printing at all:

\nbpdfInput{Snips/Implementation/34.pdf}
We then compare \verb$lhs$ with \verb$rhs$. The output, \verb$True$, tells us that we have proven~\eqref{eq:R3A}:
{\def\nbpdfPostInput{\hfill}

\nbpdfInput{Snips/Implementation/35.pdf}
\nbpdfOutput{Snips/Implementation/36.pdf}
We show that $B^l=B^r$ by following exactly the same procedure. Note that we ignore the summation over $c_y$ and instead treat $c_y$ as a fixed crossing $(s,m,n)$. If an equality is proven for every fixed $c_y$, it is of course also proven for the sum over $c_y\in Y$.

\nbpdfInput{Snips/Implementation/37.pdf}
\nbpdfOutput{Snips/Implementation/38.pdf}
Similarly we prove that $C^l=C^r$, and this concludes the proof of Proposition~\ref{prop:R3}.

\nbpdfInput{Snips/Implementation/39.pdf}
\nbpdfOutput{Snips/Implementation/40.pdf}
}
\vskip -7mm
\ \endpar{\ref{prop:R3}}

\begin{remark} \label{rem:E} The computations above were carried out for generic $g_{\nu\alpha\beta}$ and for a generic $c_y=(s,m,n)$; namely, without specifying the knot diagrams in full, and hence without assigning specific values to $g_{\nu\alpha\beta}$, and without specifying $m$ and $n$. Under these conditions the three parts of~\eqref{eq:ABC} cannot mix (namely, terms from, say, $A^h$ cannot cancel terms in $B^h$ or $C^h$), and so it would have been enough to show that $E^l=E^r$, where $E^h$ combines $A^h$ and $B^h$ and $C^h$ (and a few harmless further terms) by adding $c_y$ to the summation corresponding to $A^h$:
\[
  E^h = \sum_{c\in\{c^h_1,c^h_2,c^h_3,c_y\}} F^h_1(c)
    + \sum_{c_0,c_1\in\{c^h_1,c^h_2,c^h_3,c_y\}} F^h_2(c_0,c_1).
\]
But that's a simpler computation:

\nbpdfInput{Snips/Implementation/41.pdf}
{\def\nbpdfPostInput{\hfill}

\nbpdfInput{Snips/Implementation/42.pdf}
\nbpdfOutput{Snips/Implementation/43.pdf}
}\end{remark}\endpar{\ref{rem:E}}