Proof of `Construction 2` (4th statement)

groundedproofs/Lax888481Proofs/Construction2.lean · lax-888481

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.

Read the Lean proof on GitHub

Description

The largest processing time is a supremum over the jobs, and every one of the four kinds of job has a processing time of at most 2525: the variable job is exactly 2525, a literal job is 11, and the two wrappers are dl−1dl - 1 and 25−dl25 - dl with dldl clamped to [2,24][2, 24].