Operations on CNF and DNF -- proof internals

theorem Complexity.DNF.eval_disjoin_internal {N : ℕ} (formulas : List (DNF N)) (input : BitString N) : (disjoin formulas).eval input = formulas.any fun (formula : DNF N) => formula.eval input

theorem Complexity.DNF.width_disjoin_le_internal {N : ℕ} (formulas : List (DNF N)) (bound : ℕ) (hbound : ∀ formula ∈ formulas, formula.width ≤ bound) : (disjoin formulas).width ≤ bound

theorem Complexity.DNF.complexity_disjoin_internal {N : ℕ} (formulas : List (DNF N)) : (disjoin formulas).complexity = (List.map complexity formulas).sum

theorem Complexity.CNF.eval_conjoin_internal {N : ℕ} (formulas : List (CNF N)) (input : BitString N) : (conjoin formulas).eval input = formulas.all fun (formula : CNF N) => formula.eval input

theorem Complexity.CNF.width_conjoin_le_internal {N : ℕ} (formulas : List (CNF N)) (bound : ℕ) (hbound : ∀ formula ∈ formulas, formula.width ≤ bound) : (conjoin formulas).width ≤ bound

theorem Complexity.CNF.complexity_conjoin_internal {N : ℕ} (formulas : List (CNF N)) : (conjoin formulas).complexity = (List.map complexity formulas).sum