helphome pageduck scriptspecificationfirst proof pagepage 1 1 2 3 xpage 2

Doubly Reversed Flag

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: Coinduction now requires us to do the following:
  1. Show R is -congruence.
  2. Show ( F  : Flag  ) (rev (rev F)) R F .


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 tatami.

BOBJ proof scoreLeft    Up    Down    Right   

       This page was generated by Kumo on Tue Feb 13 17:33:10 PST 2001.