Version history

Submission versions

  1. lax-888481current version

    Interval Scheduling with Eligible Machine Sets

  2. lax-470956viewing

    Interval Scheduling with Eligible Machine Sets

    GitHub sourceShown on this page

Proof of `Preprocessing an interval scheduling instance down to a bounded number of live jobs` (1st statement)

groundedproofs/Lax470956Proofs/Preprocessing.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 kept jobs alive at tt are covered by the intervals [dd−pp,dd)[dd - pp, dd) with dd∈(t,t+pmax]dd ∈ (t, t + p_max] and pp∈[1,pmax]pp ∈ [1, p_max], and each such interval keeps at most mm jobs per machine.