²We denote by $⟦\zeta ⟧(𝜃,t)$ the results of evaluating the strategy expression $\zeta$ in the term $t$ with a variable context substitution $𝜃$, by $matches(P,t,C,𝜃)$ the matches of the term $t$ into the pattern $P$ satisfying the condition $C$ and extending the bindings of the previous substitution $𝜃$, and by $Defs$ the set of strategy definitions. In the remainder of this section, we will explain in detail all these combinators.