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.
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 : the variable job is exactly , a literal job is , and the two wrappers are and with clamped to .