helphome pageduck scriptspecificationfirst proof pagepage 3page 2 1 2 3 xclosing page

Doubly Reversed Flag


Finally we show   (rev rev F) R F   .

We want to prove
( F  : Flag  ) (rev (rev F)) R F .
We take the following steps:

And thus the main goal is proved.

Explanation

1. Because the formula to be proved is universally quantified, our first step is to eliminate the quantifier, by introducing a new constant, f of sort Flag, to stand for the variable F .

2. After adding "= true " as its right side, and substituting  f for F, what remains to be proved is the equation

(rev rev f R f) = true .
For this, we use reduction, applying the current set of rewrite rules to each side, to see if these two terms reduce to the same thing, which they do.


BOBJ proof scoreLeft    Up    Down    Right   
 

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