Proof of `Raising the Number of Days and the Fairness Parameter` (10th statement)
groundedproofs/Lax117284Proofs/Machine/FreeFinal.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, a first pass over the table checks that every job takes some time and is not due before it starts, a second pass finds the largest processing time of the first day, and the numbers of the output are written — the old table, then the new day, whose due dates are that gap times one, two, and so on. A word that is not the code of such 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.