Reidemeister enumeration is only a semidecision

Fix a code $C$ with $c$ crossings. The neighbor procedure uses bound $c+2$. By [F2] and [F3], this yields a finite candidate list containing every normalized connected one-component code with at most $c+2$ crossings. Each candidate has finitely many crossing labels, edge labels, and local edge intervals; the number of relabelings, subsets of at most three local crossings, boundary orders, and move variants is finite. Each candidate validation terminates by [F4]. Thus the neighbor list is finite and its local comparisons terminate.

If the neighbor procedure returns $(E,\mu )$, its certificate $\mu$ records either a code relabeling or a local code replacement matching one of the oriented Reidemeister variants, so [F4] and [F5] identify the represented diagrams up to planar isotopy and that one local move. Conversely, any single R1, R2, or R3 move changes the crossing count by at most two. Its result therefore appears among the candidates bounded by $c+2$ by [F3]. The move disk has two, four, or six boundary endpoints and at most three local crossing records; these are among the finite sites and variants checked by [F1]. Relabeling its finite code data is also among the finite bijections tested. Hence every one-move neighbor is returned.

The initial breadth frontier is a singleton. If a frontier is finite, [F1] and step 1.1 give a finite neighbor list for each of its members; a finite union of finite lists is finite. By induction every layer is finite and is processed in finite time, including an empty layer, which the algorithm repeats without returning a negative answer.

If the search returns a path, every adjacent pair has a certificate from [F1]. By step 2.1 each such pair differs by planar isotopy or one oriented Reidemeister move; concatenating the finitely many certificates gives a finite move sequence between the input diagrams. The easy direction of [F7] therefore gives ambient isotopy.

If the represented oriented knots are ambient-isotopic, [A1] and [F7] give a finite sequence of planar isotopies and oriented Reidemeister moves. By [F5], each intermediate diagram has a valid normalized code class. By step 2.1, the code class after each move appears in the corresponding neighbor list. Induction on the finite path length therefore places the target code class in a finite breadth layer; by step 2.2 that layer finishes, and [F6] returns the path.

The algorithm has no negative-output branch by [F6]. If no finite move path exists, it never returns Found(path); any finite-depth run that has not found the target establishes only that no path of that bounded length was found. The finite enumeration proves no decision or complexity-class conclusion. Finite neighbor generation and breadth-layer processing are choice-free; ${\mathrm{A}\mathrm{C}}_{\omega }$ is used only in [F5] and [F7] to interpret code and ambient-isotopy equivalence.