Proof of `Construction 2` (7th statement)
groundedproofs/Lax470956Proofs/Reduce.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 well-formed formula this is the pair of size bounds already proved of the construction; on any other word the fixed instance has one job of processing time one and weight one.