The reduction rules define how a noncanonical
term may be reduced.
Figure gives a list of the noncanonical forms.
The variables denoted by a (possibly subscripted)
** e** indicate so-called * argument places*,
which must be occupied by canonical terms of the appropriate type
before any sense can be made of the term.
In the rules which follow we will use to denote the canonical ` int` term
whose value is **n**.
As an example consider the rule for addition:

We use to indicate that the term on the left (the * redex* )
reduces to the term on the right (the * contractum* ).
Note that the form of the contractum depends on the values of the canonical
terms appearing in the argument places of the redex.
This is a property of all the rules.
The rules for the other arithmetic operators are almost identical
and can be obtained by replacing both occurrences of **+** with the appropriate
operator.
The rest of the rules are listed in figure .

**Figure:** The Nonarithmetic Reduction Rules

These rules embody the content of the computation rules
of the Nuprl
logic.
One somewhat anomalous term is the ` term_of()` term.
This term evaluates to the term extracted from
the given theorem.

Thu Sep 14 08:45:18 EDT 1995