The rewrite package treats rewrite relations as first-order terms: the
two principal arguments of relations are expected to be supplied as subterms
rather than by application. If a relation term also takes additional
parameters as subterms, these should always be positioned before the
principal argument subterms. For example, the 
equality
relation has T as a parameter and has logical structure
equal(T;t;
).
Relations are most commonly typed-valued, but boolean-valued relations are also accepted by the rewrite package. When a boolean-valued relation is to be used in a context where a type-valued relation is expected, the relation should be wrapped in the assert abstraction which converts boolean-valued expressions to type-valued ones.
Equivalence relations should be declared by an invocation of
This declares the term with opid rnam to be an equivalence relation, and the term with opid stronger-rnam to be an immediately stronger equivalence relation. Commonly, stronger-rnam will be `equal`. Most often, there will be only one such declaration for each rnam. However, multiple declarations for a single rnam are sometimes needed and are quite acceptable.
Order relations are grouped into relation families . A family is a lattice of order and equivalence relations of form:
where weaker relations are higher in the lattice, and relations within a family satisfy
The converse of both strict and non-strict order relations R should always be defined directly in terms of R. For example, the definition of the abstraction rev_implies is
The package assumes that order relations can be inverted by folding and unfolding such definitions.
Family should be declared using an invocation of
Dummy terms (with structure dummy(), displaying as ?, and entered using dummy) should be used as placeholders when a member of a family is missing. A notational abbreviation has been defined for such invocations which can be entered by the name relfam. It displays as
Examples include for the standard order relations on the integers
and for the `divides' and `associate' relation in a theory of cancellation monoids [4]
If there are no defined order relations associated with an equivalence relation, then there is no need to include the equivalence relation in an order relation family. It is quite permissable (and not infrequent) that several order relation families share the same equivalence relation.
The partial order of strengths of relations is taken to be the reflexive transitive closure of the relation defined by the M-shaped graphs
for each family and the equivalence relation declarations. Additional relations between order relations can be noted by using
So far these methods of describing the partial order have been adequate, though the methods might well need reorganisation in the future.
These relation declarations should be inserted in ML objects that are positioned after the referred-to relations have been defined, but before they are used in any lemmas that might be accessed by the rewrite package.
In Nuprl 4.1, the relation declarations
were used. These are now obselete and should be replaced by the ones described above.