Monotone Boolean formulas -- proof internals

theorem Complexity.MonotoneFormula.eval_toBoolFormula_internal {N : ℕ} (formula : MonotoneFormula N) (input : BitString N) : BoolFormula.eval input.toTotal formula.toBoolFormula = eval input formula

theorem Complexity.MonotoneFormula.size_toBoolFormula_internal {N : ℕ} (formula : MonotoneFormula N) : formula.toBoolFormula.size = formula.size

theorem Complexity.MonotoneFormula.leaves_toBoolFormula_internal {N : ℕ} (formula : MonotoneFormula N) : formula.toBoolFormula.leaves = formula.leaves

theorem Complexity.MonotoneFormula.depth_toBoolFormula_internal {N : ℕ} (formula : MonotoneFormula N) : formula.toBoolFormula.depth = formula.depth

theorem Complexity.MonotoneFormula.eval_monotone_internal {N : ℕ} (formula : MonotoneFormula N) : IsMonotoneBoolFun fun (input : BitString N) => eval input formula

theorem Complexity.MonotoneFormula.eval_eq_of_agree_internal {N : ℕ} (formula : MonotoneFormula N) {x y : BitString N} (agree : ∀ index ∈ formula.vars, x index = y index) : eval x formula = eval y formula

theorem Complexity.MonotoneFormula.card_vars_le_leaves_internal {N : ℕ} (formula : MonotoneFormula N) : formula.vars.card ≤ formula.leaves

theorem Complexity.MonotoneFormula.leaves_le_two_pow_depth_internal {N : ℕ} (formula : MonotoneFormula N) : formula.leaves ≤ 2 ^ formula.depth

theorem Complexity.MonotoneFormula.essentialInputs_subset_vars_internal {N : ℕ} (formula : MonotoneFormula N) : (essentialInputs fun (input : BitString N) (x : Fin 1) => eval input formula) ⊆ formula.vars

theorem Complexity.MonotoneFormula.card_essentialInputs_le_leaves_internal {N : ℕ} (formula : MonotoneFormula N) : (essentialInputs fun (input : BitString N) (x : Fin 1) => eval input formula).card ≤ formula.leaves

theorem Complexity.MonotoneFormula.card_essentialInputs_le_leaves_of_computes_internal {N : ℕ} (formula : MonotoneFormula N) (function : BitString N → Bool) (computes : formula.Computes function) : (essentialInputs fun (input : BitString N) (x : Fin 1) => function input).card ≤ formula.leaves