claimroutineinferred_dep

Predecessors of local edits and branches

Predecessors of local-edit and branch edges found by bounded case guessing
predecessor cases for the simplest instructions
Claim·§11.2 Program states and record bounds·inside lemGuarded local graph for terminal recipes

Statement (paper)

For a local-edit instruction, the predecessor candidates are obtained by guessing the bounded overwritten symbols, the preceding finite mode and the bounded head moves, and then testing the instruction forward, with a bounded number of cases. For a branch instruction, the predecessor candidates are obtained by performing the same fresh restoring query at the unchanged cursor and testing the guessed preceding symbols; the query is always restarted on its regenerated arguments, and its guards are checked before it is made, including for a candidate predecessor.

In plain English

For a local-edit instruction, the predecessor candidates come from guessing the bounded overwritten symbols, the preceding finite mode and the bounded head moves, then testing the instruction forward, using boundedly many cases. For a branch instruction, they come from running the same fresh restoring query at the unchanged cursor and testing the guessed preceding symbols; the query is restarted on regenerated arguments, with its guards checked first, even for a candidate predecessor.

Why it's here

This gives the predecessor-case part of the local graph lemma for the two simplest instruction types, showing that predecessors can be enumerated with a bounded number of case labels and one cursor. Because a branch re-runs the same restoring query only after its guards pass, the opaque query is never made on an unchecked argument. The later claim on canonical case codes and local incidence order builds on these candidate sets.
Classified routine:
Standard reversibility-style predecessor enumeration for local machine steps, in the spirit of Lange–McKenzie–Tapp's reversible space simulation: guess the bounded overwritten symbols and test the step forward. This is bookkeeping inside the paper's local graph lemma, building on the preceding claim.

Uses

claimGuarded deterministic finite graph keeps designated paths

Used by

claimCanonical case codes give local incidence order

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Predecessors of local edits and branches" rests on claim-lem-ctrl-local-graph-1