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 intro

>> = in

>> in

>> decide(;;) = decide(;;) in

>> decide(inl();;) = in

`
`

Thu Sep 14 08:45:18 EDT 1995