Parity on a finite support -- proof internals

theorem Complexity.Schnorr.xorOn_empty_internal {N : ℕ} (input : BitString N) : xorOn ∅ input = false

theorem Complexity.Schnorr.xorOn_insert_internal {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (hindex : index ∉ support) (input : BitString N) : xorOn (insert index support) input = xorOp (input index) (xorOn support input)

theorem Complexity.Schnorr.xorOn_update_of_not_mem_internal {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (hindex : index ∉ support) (value : Bool) (input : BitString N) : xorOn support (Function.update input index value) = xorOn support input

theorem Complexity.Schnorr.xorOn_update_false_eq_erase_internal {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (input : BitString N) : xorOn support (Function.update input index false) = xorOn (support.erase index) input

theorem Complexity.Schnorr.xorOn_flip_internal {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (hindex : index ∈ support) (input : BitString N) : xorOn support (Function.update input index !input index) = !xorOn support input

theorem Complexity.Schnorr.xorOn_applyTo_internal {N : ℕ} (support : Finset (Fin N)) (restriction : Restriction.On N) (input : BitString N) : xorOn support (restriction.applyTo input) = xorOp (xorOn support (restriction.applyTo fun (x : Fin N) => false)) (xorOn ({index ∈ support | restriction index = none}) input)

theorem Complexity.Schnorr.xorOn_univ_eq_xorBool_internal {N : ℕ} (input : BitString N) : xorOn Finset.univ input = xorBool N input

theorem Complexity.Schnorr.xorBool_applyTo_internal {N : ℕ} (restriction : Restriction.On N) (input : BitString N) : xorBool N (restriction.applyTo input) = xorOp (xorBool N (restriction.applyTo fun (x : Fin N) => false)) (xorOn restriction.freeVariables input)

theorem Complexity.Schnorr.card_support_le_depth_internal {N : ℕ} (tree : DecisionTree.On N) (support : Finset (Fin N)) (computes : ∀ (input : BitString N), DecisionTree.On.eval input tree = xorOn support input) : support.card ≤ tree.depth

theorem Complexity.Schnorr.card_support_le_depth_offset_internal {N : ℕ} (tree : DecisionTree.On N) (support : Finset (Fin N)) (offset : Bool) (computes : ∀ (input : BitString N), DecisionTree.On.eval input tree = xorOp offset (xorOn support input)) : support.card ≤ tree.depth

theorem Complexity.Schnorr.freeVariables_card_le_depth_of_restricted_xor_internal {N : ℕ} (tree : DecisionTree.On N) (restriction : Restriction.On N) (computes : ∀ (input : BitString N), DecisionTree.On.eval input tree = xorBool N (restriction.applyTo input)) : restriction.freeVariables.card ≤ tree.depth