REWRITE-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.
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

© 1988-99, Carnegie Mellon University.

TPS homepage