Proof of `Lemma 3` (4th statement)
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
The repaired step. Reading the profile at back to is a shift by , and the two branches differ by whether is added — which decrements the coordinate and needs a free machine, the capacity test being the sum of the whole profile.