Proof of `Per-Client Fairness Parameters at Treewidth Four` (4th 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 in normal form is sent to the code of the constructed instance, and the code determines the instance, so the question about the word is the question about the instance; every other word goes to the rejected word, which is in no language, and is not in the language of the normal form.