We show that
R
is a hidden
-congruence.
We use
quantifier elimination
,
implication elimination
, and
reduction
to show that
(
F1, F2 : Flag) F1 R F2
implies
(up? F1) R (up? F2) .
This involves the following steps:
introduce new
constants
f1, f2
of sort
Flag
;
assume
f1 R f2 = true
;
show
(up? f1) R (up? f2) = true
by
reduction
.
26 September 26 1996