Proof of `Scheduling on one machine as batching`
groundedproofs/Lax434175Proofs/BatchingZeroSetup.lean · lax-434175
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
Put every job in a batch of its own, numbered in the order of the schedule; with setup time the batches are processed exactly as the jobs. Conversely, split every serial batch into its jobs, processed in the order of their numbers from the start of the batch.