The parent antichain contains no clause included in H or any petal P_a, since that would already be a strict subset of a selected clause. Thus child A inserts a new H, and child B inserts at least M^j distinct width-j petals. No petal contains a variable from H because the selected clauses are non-tautological; the added units NOT l therefore do not subsume petals. Already-present units are retained but not counted as new. Every old clause removed during this normalization contains a newly inserted strict subset. These facts let the analysis charge deletions to insertions, rather than incorrectly bounding only the clauses currently visible.