DERIVORis indeed a morphism from the
EQtheory of order sorted equations to the
TRIMtheory 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
25 February 1998