We show that the compiler spec 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