Proof of `Construction 1` (4th statement)
groundedproofs/Lax470956Proofs/Construction1Reduce.lean · lax-470956
What this proof establishes
no assumptions
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
On a word that is a graph the claim is the correctness of Construction 1, transported along the encoding on the right and along the choice of instance on the left; on any other word both sides are false, the left because there is no graph and the right because the word the map emits has a job it cannot run.