cnf_satisfiable_of_append
theoremverified
If the concatenation `f1 ++ f2` of two CNF formulas is satisfiable (`CnfSatisfiable (f1 ++ f2)`), then both `f1` and `f2` are satisfiable (`CnfSatisfiable f1 ∧ CnfSatisfiable f2`).
Statement
theorem cnf_satisfiable_of_append {V : Type*} {f1 f2 : List (List (CnfLit V))} (h : CnfSatisfiable (f1 ++ f2)) : CnfSatisfiable f1 ∧ CnfSatisfiable f2
- Source
- folklore
- Verified
- 07 Sep 2026
- Axioms
- none — Lean reports it depends on no axioms
- Built on 3
- CnfSatisfiableA CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains…
- cnf_satisfiable_subsetIf every clause of a CNF formula `f1` is contained in a CNF formula `f2` (that is, `f1 ⊆ f2`), and `f2` is satisfiable (`CnfSatisfiable…
- CnfLitA CNF literal over a variable type V is either a positive variable or a negated variable.
- Used by 1
- cnf_satisfiable_append_sum_iffLet f be a CNF formula over a variable type V and g a CNF formula over a variable type W. Replace every literal of f by the literal of the…
Read back from the Lean
For any type V and any two CNF formulas f1 and f2 (represented as lists of lists of literals over V), if the concatenation f1 ++ f2 is satisfiable (CnfSatisfiable), then f1 is satisfiable and f2 is satisfiable.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- If a concatenated CNF formula f1 ++ f2 is satisfiable, then both f1 and f2 are satisfiable. -/ theorem cnf_satisfiable_of_append {V : Type*} {f1 f2 : List (List (CnfLit V))} (h : CnfSatisfiable (f1 ++ f2)) : CnfSatisfiable f1 ∧ CnfSatisfiable f2 := ⟨cnf_satisfiable_subset (List.subset_append_left f1 f2) h, cnf_satisfiable_subset (List.subset_append_right f1 f2) h⟩