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 `Construction 1` (5th statement)

groundedproofs/Lax470956Proofs/Construction1Reduce.lean · lax-470956

What this proof establishes

no assumptions

def✓Lax470956.Construction1 (5th 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

Either the map emits Construction 1's word, which presents the constructed instance and its threshold, or it emits the fixed word, which presents one job and the threshold one.