The term order that is used for the resulting terms or formulas.
Substitution that is to be used underneath
Re-sort an object with a new
Simple substitutions work by simple replacement
Compare the order of this
Substitution with a given order.
Some kinds of substitutions can only be applied when pseudo-reduction is allowed to be performed.