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 coinduction to prove that it is a behavioral property of the input specification. For this, we must define the following:

F1,F2

Flag

F1 R F2

up? F1 == up? F2

{ up? }

Coinduction now requires us to do the following:

( F : Flag) (rev (rev F)) R F

This page was generated by Kumo on Fri Jul 02 14:09:28 PDT 1999.