A term rewriting rule is a pair of terms, commonly written as formula_103, to indicate that the left-hand side can be replaced by the right-hand side . A term rewriting system is a set of such rules. A rule formula_103 can be applied to a term if the left term matches some subterm of , that is, if formula_105 for some position in and some substitution formula_106. The result term of this rule application is then obtained as formula_107; see picture 1. In this case, formula_108 is said to be rewritten in one step, or rewritten directly, to formula_109 by the system formula_65, formally denoted as formula_111, formula_112, or as formula_113 by some authors.