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.