| page 1 | 1 2 3 x |
| We show that reversing a flag twice has no effect.
We want to prove (We use explicit coinduction to prove that it is a behavioral property of the input specification. For this, we use the following:
 =
{up? }
.
|
| Explanation
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 |
|
F
: Flag
)
rev (rev F) = F .
; this explains the single formula to be proved on this
tatami.
