Finite-arity decision trees -- proof internals

theorem Complexity.DecisionTree.On.eval_toDecisionTree_internal {N : ℕ} (input : BitString N) (tree : On N) : DecisionTree.eval input.toTotal tree.toDecisionTree = eval input tree

theorem Complexity.DecisionTree.On.depth_toDecisionTree_internal {N : ℕ} (tree : On N) : tree.toDecisionTree.depth = tree.depth

theorem Complexity.DecisionTree.On.numLeaves_toDecisionTree_internal {N : ℕ} (tree : On N) : tree.toDecisionTree.numLeaves = tree.numLeaves

theorem Complexity.DecisionTree.On.numLeaves_le_two_pow_depth_internal {N : ℕ} (tree : On N) : tree.numLeaves ≤ 2 ^ tree.depth

theorem Complexity.DecisionTree.On.card_vars_le_arity_internal {N : ℕ} (tree : On N) : tree.vars.card ≤ N

theorem Complexity.DecisionTree.On.eval_neg_internal {N : ℕ} (input : BitString N) (tree : On N) : eval input tree.neg = !eval input tree

theorem Complexity.DecisionTree.On.depth_neg_internal {N : ℕ} (tree : On N) : tree.neg.depth = tree.depth

theorem Complexity.DecisionTree.On.numLeaves_neg_internal {N : ℕ} (tree : On N) : tree.neg.numLeaves = tree.numLeaves

theorem Complexity.DecisionTree.On.vars_neg_internal {N : ℕ} (tree : On N) : tree.neg.vars = tree.vars

theorem Complexity.DecisionTree.On.eval_restrict_internal {N : ℕ} (restriction : Restriction.On N) (input : BitString N) (tree : On N) : eval input (restrict restriction tree) = eval (restriction.applyTo input) tree

theorem Complexity.DecisionTree.On.depth_restrict_le_internal {N : ℕ} (restriction : Restriction.On N) (tree : On N) : (restrict restriction tree).depth ≤ tree.depth

theorem Complexity.DecisionTree.On.vars_restrict_subset_filter_internal {N : ℕ} (restriction : Restriction.On N) (tree : On N) : (restrict restriction tree).vars ⊆ {index ∈ tree.vars | restriction index = none}

theorem Complexity.DecisionTree.On.restrict_empty_internal {N : ℕ} (tree : On N) : restrict Restriction.On.empty tree = tree

theorem Complexity.DecisionTree.On.restrict_comp_internal {N : ℕ} (first second : Restriction.On N) (tree : On N) : restrict second (restrict first tree) = restrict (first.comp second) tree