Proof of `Raising the Number of Days and the Fairness Parameter` (8th statement)
groundedproofs/Lax117284Proofs/Machine/BlockFinal.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, and that the parameter is one, a second pass finds the largest due date, and the numbers of the output are written cell by cell, the closed form of every cell of the new table being computed from its row and column. An instance without clients is answered with the instance without clients and one more day, and 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.