Another major difference between the Lambda--prl rules and the Nuprl rules is the treatment of equality and simplification. The logic of Lambda--prl is sufficiently simple that all equality reasoning can be lumped into a single rule. Similarly, simplification of terms is handled by a single rule. The two are combined, together with some elementary arithmetic reasoning, into a decision procedure called arith which handles nearly all of the low--level details of Lambda--prl proofs. However, the additional expressiveness of the Nuprl logic prevents such a simple solution. For each term constructor there is a rule of equality, for each elimination form there is a computation rule, and there is a general rule of substitution.
For instance, the equality rule for inl is as follows.
>> inl() = inl() in | by introFor decide there are two equality rules: the basic equality rule for the constructor and a computation rule. The goals are, respectively,
>> = in
>> decide(;;) = decide(;;) inand
>> decide(inl();;) = inEquations obtained with these rules can be used by the equality and substitution rules.