Lax Lean Archive

Proof of `Preprocessing an Interval Scheduling Instance Down to a Bounded Number of Live Jobs` (2nd statement)

groundedproofs/Lax888481Proofs/Preprocessing.lean · lax-888481

What this proof establishes

no assumptions

def✓Lax888481.Preprocessing (2nd statement)

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

In the paper

  • page 5 of this submission's paper

Description

One inequality is immediate, since a schedule using only kept jobs is a schedule. The other is the exchange argument: any feasible schedule can be rewritten, one discarded job at a time, into one of no smaller weight that uses only kept jobs.