Proof of `Just-in-Time Scheduling on Unrelated Machines as Day-Independent Due Dates` (5th statement)
groundedproofs/Lax117284Proofs/Machine/JitFinal.lean · lax-117284
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
The reduction is a word RAM program on the zeros and ones of its input: a one-pass tokenizer reads the numbers of the instance — the counts, the due dates and the processing times machine by machine —, a pass over the table of processing times checks that every job takes some time and is not due before it starts, and the numbers of the image are written cell by cell, each cell being the processing time of its job on its machine and the due date of that job, found from the cell's index by division. The counts are the same, and the parameter is . A word that is not the code of an instance is answered with the rejected word. The numbers may be exponential in the length of the input, which the word length of a polynomial-time word RAM accommodates, and polynomial time on the word RAM transfers to a Turing machine.