Compiling finite decision trees to CNF and DNF -- proof internals

theorem Complexity.DecisionTree.On.eval_toDNF_internal {N : ℕ} (tree : On N) (input : BitString N) : tree.toDNF.eval input = eval input tree

theorem Complexity.DecisionTree.On.eval_toCNF_internal {N : ℕ} (tree : On N) (input : BitString N) : tree.toCNF.eval input = eval input tree

theorem Complexity.DecisionTree.On.width_toDNF_le_depth_internal {N : ℕ} (tree : On N) : tree.toDNF.width ≤ tree.depth

theorem Complexity.DecisionTree.On.width_toCNF_le_depth_internal {N : ℕ} (tree : On N) : tree.toCNF.width ≤ tree.depth

theorem Complexity.DecisionTree.On.complexity_toDNF_le_numLeaves_internal {N : ℕ} (tree : On N) : tree.toDNF.complexity ≤ tree.numLeaves

theorem Complexity.DecisionTree.On.complexity_toCNF_le_numLeaves_internal {N : ℕ} (tree : On N) : tree.toCNF.complexity ≤ tree.numLeaves

theorem Complexity.DecisionTree.On.complexity_toDNF_le_two_pow_depth_internal {N : ℕ} (tree : On N) : tree.toDNF.complexity ≤ 2 ^ tree.depth

theorem Complexity.DecisionTree.On.complexity_toCNF_le_two_pow_depth_internal {N : ℕ} (tree : On N) : tree.toCNF.complexity ≤ 2 ^ tree.depth

theorem Complexity.DecisionTree.On.eval_anyDNF_internal {N : ℕ} (trees : List (On N)) (input : BitString N) : (anyDNF trees).eval input = trees.any fun (tree : On N) => eval input tree

theorem Complexity.DecisionTree.On.eval_allCNF_internal {N : ℕ} (trees : List (On N)) (input : BitString N) : (allCNF trees).eval input = trees.all fun (tree : On N) => eval input tree

theorem Complexity.DecisionTree.On.width_anyDNF_le_internal {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (anyDNF trees).width ≤ bound

theorem Complexity.DecisionTree.On.width_allCNF_le_internal {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (allCNF trees).width ≤ bound

theorem Complexity.DecisionTree.On.complexity_anyDNF_le_internal {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (anyDNF trees).complexity ≤ trees.length * 2 ^ bound

theorem Complexity.DecisionTree.On.complexity_allCNF_le_internal {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (allCNF trees).complexity ≤ trees.length * 2 ^ bound