Fixed-arity nonuniform Barrington families -- proof internals

theorem Complexity.fixedArityFormulaFamily_exists_bp_internal (F : FixedArityFormulaFamily) (hF : F.LogDepth) : ∃ (R : FixedArityBPFamily 5), R.PolynomialLength ∧ R.function = F.function

theorem Complexity.fixedArityBPFamily_exists_formula_internal (R : FixedArityBPFamily 5) (hR : R.PolynomialLength) : ∃ (F : FixedArityFormulaFamily), F.LogDepth ∧ F.function = R.function

theorem Complexity.formulaNC1_subset_width5BP_internal : FormulaNC1 ⊆ Width5BP

theorem Complexity.width5BP_subset_formulaNC1_internal : Width5BP ⊆ FormulaNC1