Operations on CNF and DNF -- definitions

Disjoining DNFs concatenates their term lists. Dually, conjoining CNFs concatenates their clause lists. These are the width-preserving operations used when one alternating formula layer is assembled from normal forms for its children.

def Complexity.DNF.disjoin {N : ℕ} (formulas : List (DNF N)) : DNF N

Disjoin a finite list of DNFs by concatenating all of their terms.

Equations

• Complexity.DNF.disjoin formulas = { terms := List.flatMap Complexity.DNF.terms formulas }

def Complexity.CNF.conjoin {N : ℕ} (formulas : List (CNF N)) : CNF N

Conjoin a finite list of CNFs by concatenating all of their clauses.

Equations

• Complexity.CNF.conjoin formulas = { clauses := List.flatMap Complexity.CNF.clauses formulas }