Stack-free streams for finite Boolean folds — proof internals

theorem Complexity.BoolFormula.rightFoldSize_nil_internal : rightFoldSize [] = 1

theorem Complexity.BoolFormula.rightFoldSize_cons_internal (formula : BoolFormula) (formulas : List BoolFormula) : rightFoldSize (formula :: formulas) = formula.size + rightFoldSize formulas + 1

theorem Complexity.BoolFormula.rightFoldSize_eq_size_conjs_internal (formulas : List BoolFormula) : rightFoldSize formulas = (conjs formulas).size

theorem Complexity.BoolFormula.rightFoldSize_eq_size_disjs_internal (formulas : List BoolFormula) : rightFoldSize formulas = (disjs formulas).size

theorem Complexity.BoolFormula.compileRaw_conjs_eq_rightFold_internal (available : ℕ) (formulas : List BoolFormula) : compileRaw available (conjs formulas) = compileRawRightFold AndOrOp.and true available formulas

theorem Complexity.BoolFormula.compileRaw_disjs_eq_rightFold_internal (available : ℕ) (formulas : List BoolFormula) : compileRaw available (disjs formulas) = compileRawRightFold AndOrOp.or false available formulas

theorem Complexity.BoolFormula.length_rightFoldConnectors_internal (op : AndOrOp) (available : ℕ) (formulas : List BoolFormula) : List.length (rightFoldConnectors op available formulas) = formulas.length

theorem Complexity.BoolFormula.length_compileRawRightFold_internal (op : AndOrOp) (identity : Bool) (available : ℕ) (formulas : List BoolFormula) : List.length (compileRawRightFold op identity available formulas) = rightFoldSize formulas