We show that reversing a flag twice has no effect.
We use coinduction to prove a behavioral property of the FLAG specification:
(F : Flag) rev rev F = F .
For this, we must define the following:
  1. the candidate relation R, for F1,F2 : Flag, by:
    F1 R F2   iff   up? F1 = up? F2
  2. the selector subsignature , to contain up?, and
  3. the generator subsignature , to contain up, dn, rev .
In each case, we have taken the default selection. Coinduction now requires us to do the following:
  1. show R is a hidden -congruence;
  2. show R is preserved by all operations in ; and
  3. show (rev rev F) R F .

23 November 1996