CountingEquivalence

Sequence of valid first-order formulas about equivalent counting methods.

Consider the formula ∀z ∃^=1^i ∀x ∃y a_i(x,y,z), where ∃^=1^i is a quantifier that says that there exists exactly one i (in 0..n) such that ∀x ∃y a_i(x,y,z) is true.

This function returns the equivalence between two implementations of the formula: first, using a naive quadratic implementation; and second, using an O(n*log(n)) implementation with threshold formulas.