1 2 3 x
| page 3 | 1 2 3 x |
| Finally we show
(rev rev F) R F
.
We want to prove (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. |
|
F
: Flag
)
(rev (rev F)) R F .
