The descending-diagram procedure terminates on admissible finite codes

The polygonal drawing has finitely many bends. If the basepoint is a bend in the geometric interior of its edge, choose a short forward segment within that edge containing no crossing or other bend and move the basepoint into its interior. The adjusted point satisfies the algorithm's input condition. Moving the point within the same oriented edge crosses no crossing vertex, so it changes neither the cyclic order of crossing encounters nor the first branch reached at any crossing. Thus the adjustment leaves the crossing-change list and updated code independent of its choice. The code has finitely many edges and crossing records by [F1]. Following its coherent half-edge pairings from the basepoint returns to the starting edge after finitely many incidences, so the traversal terminates. It visits each crossing record once at first encounter, giving exactly $c$ processing operations.

Each operation either leaves the over/under label unchanged or exchanges the two labels once. It does not change vertices, edges, cyclic orders, branch pairings, orientations, or the rational drawing certificate; hence all validity conditions in [F1] remain satisfied. The resulting list has at most $c$ entries, and every recorded first underpass has become an overpass while first overpasses remain over.