Jumping and escaping: Modular termination and the abstract path ordering

Combinatorial commutation properties for reordering a sequence consisting of two kinds of steps, and for separating the well-foundedness of their combination into well-foundedness of each, are investigated. A weak commutation property, called “jumping”, along with a weakened version of the lifting property, called “escaping” and requiring only an eventual lifting, are used for proving well-foundedness of a generic, abstract version of the recursive path orderings.