One of the following:

NONE: do not rewrite equalities

ONLY-EXT: rewrite only those equalities that can be rewritten using

extensionality.

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.

© 1988-99, Carnegie Mellon University.