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