Proof of `The Fairness Parameter One Below the Number of Days` (3rd statement)
groundedproofs/Lax117284Proofs/WordCorrect.lean · lax-117284
What this proof establishes
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 word encoding an instance one parameter below its number of days is sent to the code of its formula; every other word goes to the code of an unsatisfiable formula, and the code determines the formula.