Kauffman bracket state-sum procedure properties

If $c=\mathrm{\mid }C(D)\mathrm{\mid }$, every state is a function from a $c$-element set to a two-element set, so the state set has exactly $2^c$ elements. This is finite, including the case $c=0$, where there is exactly one empty assignment. The algorithm processes every such function once and has no other loop.

For each visited state, the prescribed smoothing produces a finite crossingless union of circles. By [F2], $\mathrm{\mid }S\mathrm{\mid }-1$ is a nonnegative integer, so $A^{a(S)-b(S)}{\delta }^{\mathrm{\mid }S\mathrm{\mid }-1}$ is defined in $\mathbb{Z}[A^{\pm 1}]$. After any initial segment of the visits, the accumulator is the sum of exactly the terms already visited, by induction on the number of updates. After all $2^c$ visits it is the displayed state sum, which is returned. Therefore execution terminates with exactly the asserted output.