Q:\GREATEST\GT-IDX.TXT      2000 December 27

Theorem GT-IDX was initially met with a great deal of resistance due to
blocking by demodulators. After several very_verbose sessions the
problematic demodulators were identified and removed, and Otter then
quickly found a proof. The problem is essentially that we need to write
id(x) as restrict(Id,V,x) in order to be able to apply Theorem GT-RS.

Since id(x) can equally well be written as restrict(Id,x,x) or as
restrict(Id,x,V), or any number of other ways, it should not be
surprising that there are actually several different formulas for
GREATEST(id(x)), of which the one proposed in this theorem is perhaps
the simplest. Perhaps a proof would have been found more quickly had the
equations relating these various forms been available, especially the
inverse of the key formula

  equal(composite(id(P(x)),SINGLETON),composite(SINGLETON,id(x)))).

This is actually a special case of the more cumbersome identity

equal(composite(id(x),SINGLETON),
     composite(SINGLETON,id(U(intersection(x,R(SINGLETON)))))).  % SGIDX-CO

I also found that adding the inverse of this cumbersome formula was
essential to success when I was using the GOEDEL program.