claimroutineinferred_dep

Canonical case codes give local incidence order

Canonical case codes give each predecessor edge one description and local order
yields ordered duplicate-free incidences
Claim·§11.2 Program states and record bounds·inside lemGuarded local graph for terminal recipes

Statement (paper)

Each edge is labelled by its finite instruction case and bounded erased symbols, and its forward instruction determines a canonical reverse case code, so that an inverse probe accepts only that code and no duplicate descriptions of the same predecessor edge arise, without comparing two retained addresses. The finite case codes give a fixed local order and a bounded incidence token, and a forward edge knows its reverse token.

In plain English

Each edge carries a finite instruction case code and bounded erased symbols, and its forward instruction fixes a canonical reverse case code that an inverse probe alone accepts, so each predecessor edge has exactly one description and no two retained addresses need comparing. The finite case codes give a fixed local order and a bounded incidence token, and each forward edge knows its reverse token.

Why it's here

This turns the predecessor candidate sets for local edits, branches and cursor steps into a well-defined ordered list of incident edges, with no duplicates. The ordering and the paired forward and reverse tokens let the graph be traversed locally with bounded labels and one cursor.
Classified routine:
This is a bookkeeping step that canonicalizes edge labels by finite case codes so the local graph has a fixed rotation order with paired forward and reverse tokens. It is the standard technique of reversible or rotation-map local graph constructions (as in reversible-space simulations of Lange–McKenzie–Tapp and Reingold-style rotation maps), applied to the predecessor sets from the two preceding claims.

Uses

claimPredecessors of local edits and branchesclaimCursor-step predecessors via paired inverse

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.2 Program states and record bounds
Page
—
Label
—
Line
sections/implementation.tex:398
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Canonical case codes give local incidence order" rests on claim-lem-ctrl-local-graph-2
  • info
    inferred_dep
    outline: "Canonical case codes give local incidence order" rests on claim-lem-ctrl-local-graph-3