We show that reversing a flag twice has no effect.
We want to prove
            ( F : Flag) rev (rev F) = F
We use coinduction to prove that it is a behavioral property of the input specification. For this, we must define the following:
  1. the observation relation R for F1,F2 : Flag , by
  2. the cobasis  : { up? } .
Coinduction now requires us to do the following:
This page was generated by Kumo on Fri Jul 02 14:09:28 PDT 1999.