Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Correctness of the Algorithm`

groundedproofs/Lax117284Proofs/TwoSAT/Correct.lean · lax-117284

What this proof establishes

no assumptions

thm✓Lax117284.TwoSatCorrectness

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

Description

The width check accepts exactly the 2-CNF formulas without an empty clause; for an occurring variable the search computes reachability in the implication graph, since the iterates are a chain in the finite set of nodes and every edge ends in a node; a variable that does not occur is never contradictory. The criterion Bridge.satisfiableiffBridge.satisfiable_iff finishes the proof.