Lax Lean Archive

Proof of `The Reduction from (3,4)-Satisfiability to [2,3]-Bounded 3-SAT` (1st statement)

groundedproofs/Lax345332Proofs/BBuild.lean · lax-345332

What this proof establishes

no assumptions

def✓Lax345332.Copies (1st statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 5 of this submission's paper

Description

Two positions carrying the same literal lie on the same side, cycle or clause, by the sign pattern and the injectivity of the copy and successor maps, and there they coincide.