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