pub fn cofactor_set(
n: usize,
clauses: &CanonClauses,
) -> BTreeSet<(usize, CanonClauses)>Expand description
The strict distinct-cofactor set: every (depth, cofactor) pair reachable by prefix-restricting
the fixed order 0..n. Its cardinality is distinct_width; quotienting it by a congruence can
only merge pairs, so every quotient_class_count is ≤ distinct_width and coarser congruences
give monotonically fewer classes — both are theorems about quotients of this one fixed set, and
therefore hold on every formula.