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` (6th statement)

groundedproofs/Lax470956Proofs/Construction1Reduce.lean · lax-470956

What this proof establishes

no assumptions

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

The constructed instance has one machine for each pair of colours and one more, and the number of colours is the last entry of the word; so the parameter of the image is a function of the parameter of the source alone. An unrecognized word is sent to a word with no machine at all.