|page 1||1 2 3 x|
|We show that reversing a flag twice has no effect.
We want to prove
( F : Flag ) rev (rev F) = F .We use explicit coinduction to prove that it is a behavioral property of the input specification. For this, we use the following:
This coinduction proof, like many others, uses a default selection of the cobasis. This makes some parts of the proof automatic.
Because R is the identity on visible sorts, we need only show the congruence property for
the (single) operation in ; this explains the single formula to be proved on this