While this submission is a draft, it cannot be used by other submissions.

Proof of `Construction 2` (4th statement)

groundedproofs/Lax470956Proofs/Construction2.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.

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 dl1dl - 1 and 25dl25 - dl with dldl clamped to [2,24][2, 24].