Proof of `Relations of the Scheduling Zoo that need an encoding` (5th statement)
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.
Description
A schedule is translated by moving the jobs that are not just in time behind all others, where they are late; conversely a job that is on time in its window completes exactly at its due date.