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$:

\noindent\nbpdfInput{Snips/Implementation/32.pdf}

We then let \verb$Xl$ be the three crossings in the left-hand-side of the R3 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: 

\noindent\nbpdfInput{Snips/Implementation/33.pdf}

\noindent\nbpdfOutput{Snips/Implementation/34.pdf}

We do the same for $A^r$, except this time, without printing at all:

\noindent\nbpdfInput{Snips/Implementation/35.pdf}

We then compare \verb$lhs$ with \verb$rhs$. The output, \verb$True$, tells us that we have proven~\eqref{eq:R3A}:

\noindent\nbpdfInput{Snips/Implementation/36.pdf}

\noindent\nbpdfOutput{Snips/Implementation/37.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 it as fixed. If an equality is proven for every fixed $c_y$, it is of course also proven for the sum over $c_y\in Y$. Note also that we repeat the test twice, for the two choices of the sign of $c_y$:

\noindent\nbpdfInput{Snips/Implementation/38.pdf}

\noindent\nbpdfOutput{Snips/Implementation/39.pdf}

Similarly we prove that $C^l=C^r$, and this concludes the proof of Proposition~\ref{prop:R3}.

\noindent\nbpdfInput{Snips/Implementation/40.pdf}

\noindent\nbpdfOutput{Snips/Implementation/41.pdf}

\ \qed

\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,2,3,y}\}} F^h_1(c)
    + \sum_{c_0,c_1\in\{c^h_{1,2,3,y}\}} F^h_2(c_0,c_1).
\]
But that's a simpler computation:

\noindent\nbpdfInput{Snips/Implementation/42.pdf}

\noindent\nbpdfOutput{Snips/Implementation/43.pdf}

\end{remark}

