1 2 3 x
| page 2 | 1 2 3 x |
We show that
R
is a hidden  -congruence.
We want to prove (We take the following steps:
|
| Explanation
1. Because this formula is universally quantified, our first step is to eliminate the quantifiers, and introduce new constants, f1, f2, of sort Flag, to replace the variables F1, F2 . The resulting formula is 2. The topmost logical symbol of what remains is an implication, so our next step is implication elimination. This involves assuming the hypothesis of the implication as a new equation, with the new constants in it replacing the variables for which they stand, and with "= true" added as the right side (we have used first order predicate notation, but of course OBJ represents this as a Boolean-valued function). The assumed equation is f1 R f2 = true .which by the definition of R, is equivalent to (up? f1) = (up? f2) . 3. Again adding "= true" as the right side, what remains to be shown is the equation (up? f1) R (up? f2) = true .We do this by reduction, i.e., by applying the current set of equations as rewrite rules, including the new equation assumed under 2. above and the definition of R, to each side of the equation, to see if these two terms each reduce to the same thing. |
|
F0
F1
: Flag
)
