Proof of `Theorem 4`
groundedproofs/Lax496464Proofs/Ram/T4Final.lean · lax-496464
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.
In the paper
- page 7 of this submission's paper
Description
The greedy of Section 6.1 as a word RAM program: read the word, sort the jobs by start time (), then consider the jobs in that order, keeping the running jobs in two maximum trees over the job numbers — one keyed by due date (whose root gives the job to drop) and one by (whose root gives the next job to end) — and counting the members of the set that have already ended. Every step costs , so the whole run is within . The statement is exactly the concept's, including its positive-processing-time clause (the paper's standing assumption for Lemma 4).