Unification and combination of iterative insertion strategies with one-step traversals.

Motivated by an ongoing project on the computer aided derivation of multiscale partial differential equation models, we introduce a class of term transformations that consists in navigation strategies and insertion of contexts. We define a unification and combination operations on this class which enjoy nice algebraic properties like associativity, congruence, and the existence of a neutral and an absorbing element. The main part of this paper is devoted to proving that the unification and combination operations are correct.