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:
the observation relation
R
for
F1,F2
:
Flag
, by
F1 R F2
iff
up? F1 == up? F2
.
the cobasis :
{ up? }
.
Coinduction now requires us to do the following:
Show
R
is -congruence.Show
( F : Flag) (rev (rev F)) R F
.
This page was generated by Kumo on Fri Jul 02 14:09:28 PDT 1999.