Theorems

2D OVERLAP-QUERY CORRECTNESS THEOREM: If the operation is idempotent, then four corner blocks of size 2^kr x 2^kc return the correct answer on a static half-open rectangle.
AMORTIZED APPEND THEOREM FOR DYNAMIC ARRAYS: If a dynamic array grows its capacity geometrically on overflow, then a sequence of n appends runs in O(n), so the amortized cost of one append is O(1).
KD OVERLAP-QUERY CORRECTNESS THEOREM: If the operation is idempotent, then 2^d corner hyperblocks chosen by the level vector return the correct answer on a static half-open hyperrectangle.
LOOP INVARIANT CORRECTNESS THEOREM: If an invariant is true before the loop, is preserved by every iteration, and together with the termination condition implies the postcondition, then the loop is partially correct.
MASTER THEOREM: For recurrences of the form T(n) = aT(n/b) + f(n), the asymptotic behavior is determined by comparing f(n) with n^(log_b a) when the theorem conditions hold.
SET EQUALITY THEOREM Open article: Two sets are equal if and only if each of them is a subset of the other.
SET UNION DECOMPOSITION THEOREM Open article: The union of two sets can be decomposed into elements that belong only to the first set, only to the second set, and to both sets.
SPARSE TABLE OVERLAP-QUERY CORRECTNESS THEOREM: If the operation is idempotent, then two overlapping blocks of length 2^k chosen with k = floor(log2(length)) return the correct answer on the static range [left, right].