The Fox-coloring algorithm terminates and returns all colorings

Each crossing contributes one linear equation in the $a$ arc variables, so the algorithm forms a $c\times a$ matrix over ${\mathbb{F}}_p$. Addition and multiplication of residue classes are well-defined because congruence modulo $p$ is preserved by sums and products. If a residue $r$ is nonzero, then $\gcd (r,p)=1$, so integers $u,v$ satisfy $ur+vp=1$ and $u$ is the inverse of $r$ modulo $p$. The field hypothesis in [A1] therefore supplies every division used by the pivot instructions in [F1].

Every row operation in [F1] preserves the solution set of the homogeneous system. A row swap is reversible by the same swap; multiplying a row by a nonzero scalar is reversible by multiplying by its inverse; and adding a multiple of one row to another is reversible by subtracting the same multiple. Each transformed system is therefore equivalent to the preceding one.

The algorithm visits each of the $a$ columns once, and each pivot search inspects at most $c$ rows, for at most $ac$ pivot-search entry tests. There are at most $\min (a,c)$ pivots. If $c=0$, there are no pivots or row additions. If $c>0$, each pivot adds a multiple of its row to at most $c-1$ other rows, so at most $ac$ row additions occur; each addition updates at most $a$ coefficients, for at most $a^{2}c$ coefficient updates. Normalizing each pivot row divides at most $a$ entries, for at most $a^2$ divisions. The loops are finite and the chosen first nonzero entry makes the procedure deterministic.

At termination, each pivot column has a single $1$ in its pivot row and zeros in every other row; earlier pivot columns stay cleared because each later pivot row is zero in those columns. Each nonpivot column is free. The pivot equations uniquely determine the pivot variables from arbitrary free-variable values, and every such assignment satisfies the reduced system. By step 2.1 the reduced system has exactly the original solution set, so the returned assignments are exactly the Fox colorings.

There are exactly $p^f$ choices of the $f$ free variables, and each determines one distinct solution. If $a=0$, then $f=0$ and the empty diagram has its unique empty assignment; if $c=0$, every arc variable is free and all $p^a$ assignments are returned. The stated pivot, search, addition, update, and division bounds follow from step 2.2.