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

Doubly Reversed Flag


We show that   R   is a hidden -congruence.

We want to prove
( F0  F1  : Flag  )
            F0 R F1
       implies
            up? F0 = up? F1 .
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
f1 R f2   implies   (up? f1) R (up? f2) .

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.


BOBJ proof scoreLeft    Up    Down    Right   
 

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