Negation-normal unbounded formulas -- proof internals

theorem Complexity.AC0Formula.eval_neg_internal {N : ℕ} (input : BitString N) (formula : AC0Formula N) : eval input formula.neg = !eval input formula

theorem Complexity.AC0Formula.evalAny_negForest_internal {N : ℕ} (input : BitString N) (formulas : AC0Forest N) : evalAny input (negForest formulas) = !evalAll input formulas

theorem Complexity.AC0Formula.evalAll_negForest_internal {N : ℕ} (input : BitString N) (formulas : AC0Forest N) : evalAll input (negForest formulas) = !evalAny input formulas

theorem Complexity.AC0Formula.size_neg_internal {N : ℕ} (formula : AC0Formula N) : formula.neg.size = formula.size

theorem Complexity.AC0Formula.forestSize_negForest_internal {N : ℕ} (formulas : AC0Forest N) : forestSize (negForest formulas) = forestSize formulas

theorem Complexity.AC0Formula.depth_neg_internal {N : ℕ} (formula : AC0Formula N) : formula.neg.depth = formula.depth

theorem Complexity.AC0Formula.forestDepth_negForest_internal {N : ℕ} (formulas : AC0Forest N) : forestDepth (negForest formulas) = forestDepth formulas

theorem Complexity.AC0Formula.evalAll_ofList_internal {N : ℕ} (input : BitString N) (formulas : List (AC0Formula N)) : evalAll input (AC0Forest.ofList formulas) = formulas.all (eval input)

theorem Complexity.AC0Formula.evalAny_ofList_internal {N : ℕ} (input : BitString N) (formulas : List (AC0Formula N)) : evalAny input (AC0Forest.ofList formulas) = formulas.any (eval input)

theorem Complexity.AC0Formula.forestSize_ofList_internal {N : ℕ} (formulas : List (AC0Formula N)) : forestSize (AC0Forest.ofList formulas) = (List.map size formulas).sum

theorem Complexity.AC0Formula.forestDepth_ofList_internal {N : ℕ} (formulas : List (AC0Formula N)) : forestDepth (AC0Forest.ofList formulas) = List.foldr (fun (formula : AC0Formula N) (rest : ℕ) => max formula.depth rest) 0 formulas