Unification and combination of a class of traversal strategies made with pattern matching and fixed-points

Motivated by an ongoing project on computer aided derivation of asymptotic models governed by partial differential equations, we introduce a class of term transformations that consists of traversal strategies and insertion of contexts. We define unification and combination operations on this class which amount to merging transformations in order to obtain more complex ones. We show that the unification and combination operations enjoy nice algebraic properties like associativity, congruence and the existence of neutral elements. The main part of this paper is devoted to proving that the unification and combination operations are correct.