quantifier elimination problem

I'm learning how quantifier elimination method from model theory works in relational database field. For example, formula

Exists i | Emp[i].name == 'Smith'

could be rewritten quantifier free as

Emp[ index('Smith') ].name == 'Smith'

As usual, additional function is required, and, not surprisingly, it is an index.

Now, how could I rewrite quantifier free the following formula

Forall i,j | (i==j or Emp[i].name!=Emp[j].name)

(this is unique key constraint:-) Can index function still be employed, or some new function (Eeek!) needs to be introduced?

Thank you for your time,
Vadim Received on Thu Mar 08 2001 - 04:28:32 CET