Proof of `The reduction from satisfiability to (3,4)-satisfiability` (3rd statement)
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
Padding makes every clause three literals long. Below the padding base the occurrence counts are those of the split formula, at most three; above it a variable belongs to one gadget of one clause, where it occurs at most four times, the forced variable three times in the gadget and once as padding.