Theorems

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.