Q:\GREATEST\GT-IM-PC.TXT     2000 December 28

Theorem GT-IM-PC was first discovered on 2000 December 24 using the
GOEDEL program. The Otter proof of this theorem was obtained by using
the very_verbose feature of Otter to carefully block certain standard
demodulators which ordinarily prevent an image from being rewritten as
the range of a restriction. These demodulators include the definition of
image, which occurs in the list of demodulators for the Axiom B group,
and a related demodulator found in the demodulator list for the group
IM\1. Here we do wish expressly to rewrite the image as a restriction in
order to take advantage of the equation for GREATEST(restrict(x,y,z)).
But we do not want that equation to be used as a demodulator, because
that would not permit the application of Theorem GT-RA, which is also
needed here. This is why I also blocked the demodulator list for the
GREATEST group. I was especially gratified to see that the demodulator
for fix(restrict(x,y,z)) that had been added only yesterday was used in
this proof.