Proof of `Relations of the Scheduling Zoo that need an encoding` (1st statement)
groundedproofs/Lax434175Proofs/EncodingsFlow.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
A flow shop with two machines is a two-stage flexible flow shop as it stands. With one machine, every job gets an operation of length zero on a new first machine. Without machines every job completes at time zero, so the answer is known and is expressed by the threshold.