Q:\CR\JOBS.TXT            

1995 September 12

The lex command was not examined very carefully when the theorems
about complementary relations were proved.  In particular, no attempt
was made to include the new functor compreln(*,*) in the lex list.

In addition, in some cases the lex command may not have the correct
number of Skolem constants; this also needs to be checked.  This may
be true in other directories as well; it may be worthwhile to write a
program that computes the correct number, and automatically generates
the correct lex command!

It was unclear what would be the best order of presentation.  It has
not been investigated carefully whether the theorems could be proved
more quickly if presented in a different order.

Theorem CR-6 is essentially a form of the DeMorgan law.  It had the
longest proof, and took about 6 seconds.  Otter disposed of the other
theorems in one or two seconds.

1997 November 30

The position of compreln(x) in the lex order should probably be right
before complement(x), and after restrict(x,x,x).  In the file ALL.POS
we placed it between intersection(x,x) and complement(x).

It was noticed that we never proved the analog of the other DeMorgan law: