Lax Lean Archive

Version history

Submission versions

  1. lax-888481current version

    Interval Scheduling with Eligible Machine Sets

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version
  2. lax-470956viewing

    Interval Scheduling with Eligible Machine Sets

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceShown on this page

Proof of `The dynamic program for interval scheduling, and its state space` (3rd statement)

groundedproofs/Lax470956Proofs/DynamicProgram.lean · lax-470956

What this proof establishes

no assumptions

def✓Lax470956.DynamicProgram (3rd 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

Description

At the horizon every job has finished, so the only reachable state is the idle one, and the weight of the jobs started by then is the weight of the whole schedule.