This involves the following steps:(F1, F2 : Flag) F1 R F2implies

(up F1) R (up F2)and(dn F1) R (dn F2)and

(rev F1) R (rev F2).

- introduce new
constants
*f1, f2*of sort*Flag*. - assume
*f1 R f2 = true*. - 4. show
*(up f1) R (up f2) = true*,*(dn f1) R (dn = f2) = true*, and*(rev f1) R (rev f2) = true*, separately by reduction.

September 26, 1996