Reusable SUM, PROD, and COUNT quantifiers

[harrytallbelt]

We cannot define SUM, PROD, and COUNT quantifiers for all possible
inner expression/predicate structure, because Simplify does not support
function- and predicate-variables. For example (SUM k : Q(k) : a[k])
cannot be defined with the same axiom as (SUM k : Q(k) : a[k]*b[k]).

To solve this we might change any quantifier (SUM k : Q(k) : f(k, <outer-var-list>))
into (SUM k : Q(k) : @a[k]) while adding a condition that (A k : Q(k) : @a[k] = f(k, ...)).
This way we can only define SUM, PROD and COUNT for an array.
(In fact, COUNT can be defined as (N k : Q(k) : P(k, ...)) == (SUM k : Q(k) : a[k]),
where (A k : Q(k) : P(k, ...) ^ @a[k] = 1 | ~P(k, ...) ^ @a[k] = 0).)

One complication might be name generation (for @a), because the id format
for Simplify (Modula-3) is the same as for our predicates, so we cannot use any
symbols, we know wouldn't be in the predicate. If we generate a random name,
we'll probably still want to check if it isn't already used in predicate. We also can
concatenate all the names in predicate (UPD: or just find the longest one and
make sure the generated name is longer) and add a number in the end for each
new array. It might not be a big part of the task, as we will (probably) need
to change the implication premises.

The last issue is does this all mean that our system becomes extremely Simplify-oriented?
UPD: This is probably not an issue, because all the feature code will be in
the exact part of the system responsible for working with Simplify.