|page 3||1 2 3 x|
|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.
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.