Complete query blocks in finite decision trees -- proof internals

theorem Complexity.DecisionTree.On.assignmentFor_apply_of_mem_internal {N : ℕ} (queries : List (Fin N)) (input : BitString N) (index : Fin N) (hmem : index ∈ queries) : assignmentFor queries input index = some (input index)

theorem Complexity.DecisionTree.On.assignmentFor_apply_of_not_mem_internal {N : ℕ} (queries : List (Fin N)) (input : BitString N) (index : Fin N) (hmem : index ∉ queries) : assignmentFor queries input index = none

theorem Complexity.DecisionTree.On.assignmentFor_applyTo_internal {N : ℕ} (queries : List (Fin N)) (input : BitString N) : (assignmentFor queries input).applyTo input = input

theorem Complexity.DecisionTree.On.assignmentFor_reapply_internal {N : ℕ} (queries : List (Fin N)) (input fallback : BitString N) : assignmentFor queries ((assignmentFor queries input).applyTo fallback) = assignmentFor queries input

theorem Complexity.DecisionTree.On.assignmentOfPath_append_internal {N : ℕ} (left right : List (Fin N × Bool)) : assignmentOfPath (left ++ right) = (assignmentOfPath left).comp (assignmentOfPath right)

theorem Complexity.DecisionTree.On.assignmentOfPath_apply_of_not_mem_internal {N : ℕ} (path : List (Fin N × Bool)) (index : Fin N) (hindex : index ∉ List.map Prod.fst path) : assignmentOfPath path index = none

theorem Complexity.DecisionTree.On.assignmentOfPath_apply_eq_some_of_mem_internal {N : ℕ} (path : List (Fin N × Bool)) (hnodup : (List.map Prod.fst path).Nodup) (index : Fin N) (hindex : index ∈ List.map Prod.fst path) : ∃ (value : Bool), assignmentOfPath path index = some value

theorem Complexity.DecisionTree.On.assignmentOfPath_apply_of_mem_internal {N : ℕ} (path : List (Fin N × Bool)) (hnodup : (List.map Prod.fst path).Nodup) (query : Fin N × Bool) (hquery : query ∈ path) : assignmentOfPath path query.1 = some query.2

theorem Complexity.DecisionTree.On.assignmentOfPath_deepBlockPath_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : assignmentOfPath (deepBlockPath queries continuation) = deepBranch queries continuation

theorem Complexity.DecisionTree.On.deepPath_queryAll_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : (queryAll queries continuation).deepPath = deepBlockPath queries continuation ++ (continuation (deepBranch queries continuation)).deepPath

theorem Complexity.DecisionTree.On.map_fst_deepBlockPath_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) : List.map Prod.fst (deepBlockPath queries continuation) = queries

theorem Complexity.DecisionTree.On.deepBranch_apply_of_not_mem_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (index : Fin N) (hmem : index ∉ queries) : deepBranch queries continuation index = none

theorem Complexity.DecisionTree.On.deepBranch_apply_eq_some_of_mem_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (index : Fin N) (hmem : index ∈ queries) : ∃ (value : Bool), deepBranch queries continuation index = some value

theorem Complexity.DecisionTree.On.deepBranch_apply_of_mem_deepBlockPath_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (query : Fin N × Bool) (hquery : query ∈ deepBlockPath queries continuation) : deepBranch queries continuation query.1 = some query.2

theorem Complexity.DecisionTree.On.assignmentFor_deepBranch_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (fallback : BitString N) : assignmentFor queries ((deepBranch queries continuation).applyTo fallback) = deepBranch queries continuation

theorem Complexity.DecisionTree.On.eval_queryAll_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (input : BitString N) : eval input (queryAll queries continuation) = eval input (continuation (assignmentFor queries input))

theorem Complexity.DecisionTree.On.depth_queryAll_le_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (continuationDepth : ℕ) (hdepth : ∀ (restriction : Restriction.On N), (continuation restriction).depth ≤ continuationDepth) : (queryAll queries continuation).depth ≤ queries.length + continuationDepth

theorem Complexity.DecisionTree.On.vars_queryAll_subset_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (support : Finset (Fin N)) (hvars : ∀ (restriction : Restriction.On N), (continuation restriction).vars ⊆ support) : (queryAll queries continuation).vars ⊆ queries.toFinset ∪ support

theorem Complexity.DecisionTree.On.pathReadOnce_queryAll_internal {N : ℕ} (queries : List (Fin N)) (continuation : Restriction.On N → On N) (hnodup : queries.Nodup) (hreadOnce : ∀ (restriction : Restriction.On N), (continuation restriction).PathReadOnce) (hdisjoint : ∀ (restriction : Restriction.On N), Disjoint queries.toFinset (continuation restriction).vars) : (queryAll queries continuation).PathReadOnce