We show that R is preserved by all operations in .
We use quantifier elimination, implication elimination, conjunction elimination, and reduction to show that
(F1, F2 : Flag) F1 R F2  implies
        (up F1) R (up F2)   and   (dn F1) R (dn F2)   and
        (rev F1) R (rev F2).
This involves the following steps:
  1. introduce new constants f1, f2 of sort Flag.
  2. assume f1 R f2 = true.
  3. 4.  show (up f1) R (up f2) = true,   (dn f1) R (dn = f2) = true,  and  (rev f1) R (rev f2) = true, separately by reduction.

September 26, 1996