`DERIVOR`

is indeed a morphism from
the `EQ`

theory of order sorted equations to the `TRIM`

theory
of a term rewriting virtual machine.
Since the operator *d.sem* in
`DERIVOR`

defines the
translation, we check if *d.sem(e)* holds in the `TRIM`

theory for each `EQ`

sentence *e*.
Typically this involves quantifier elimination and reduction with occasional
use of lemma
introduction.

25 February 1998