For this, we must define the following:(F : Flag) rev rev F = F .

- the
candidate relation
*R*, for*F1,F2 : Flag*, by: *F1 R F2*iff*up? F1 = up? F2*

- the
candidate relation
- the
selector subsignature , to contain
*up?*, and - the
generator subsignature , to contain
*up, dn, rev*.

- show
*R*is a hidden -congruence; - show
*R*is preserved by all operations in ; and - show
*(rev rev F) R F .*

23 November 1996