REWRITE-EQUALITIES : FLAGREWRITE-EQUALITIES is a flag or parameter.
One of the following:
NONE: do not rewrite equalities
ONLY-EXT: rewrite only those equalities that can be rewritten using
LEIBNIZ: rewrite all equalities using the Leibniz definition.
ALL: rewrite all equalities, to an equivalence for those of type OOO,
to the extensional form
[lambda f(AB) lambda g(AB) forall x(B) f x = g x]
for those of type O(AB)(AB), and to the Leibniz form
[lambda x(A) lambda y(A) forall q(OA). q x implies q y]
for those of type OAA.
LAZY2: As for ALL, but keeping a duplicate leaf as in the LAZY2
setting of the flag REWRITE-DEFNS.
PARITY1: Uses the parity to determine whether equalities should be
rewritten as the setting LEIBNIZ or as the setting ALL. For example,
using PARITY1 when trying to prove the wff
A(OI) = B(OI) implies C
the equality is expaned using Leibniz, and when trying to prove the wff
D implies A(OI) = B(OI)
the equality is expanded using extensionality. The heuristic
is that we often use the substitutivity property when we use an equation
and use extensionality to show an equation.
REWRITE-EQUALITIES takes values of type REWRITE-DEFNS.
It belongs to subjects MS98-1 MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 IMPORTANT WFF-PRIMS MATING-SEARCH .
Its default value is ALL
Its current value is ALL.
ETPS documentation homepage