Proof of `The Reduction from (3,4)-Satisfiability to [2,3]-Bounded 3-SAT` (5th statement)
groundedproofs/Lax345332Proofs/BFinal.lean · lax-345332
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.
In the paper
- page 5 of this submission's paper
Description
A word RAM program computes the zeros and ones of the second step: the scan of the first program decodes the (3,4) formula into arrays, and the header, the cycle clauses and the copied clauses are written in the self-delimiting binary code, within a fourth-degree polynomial number of instructions. Polynomial time on the word RAM transfers to a Turing machine.