Proof of `The Explicit Graphs Are Subcubic`
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Identify the executable graph with path replacement. Each port has two path neighbors and at most one paired neighbor.