Fresh variable

For example, in term rewriting, before applying a rule ${\displaystyle l\to r}$ to a given term ${\displaystyle t}$, each variable in ${\displaystyle l\to r}$ should be replaced by a fresh one to avoid clashes with variables occurring in ${\displaystyle t}$.^{[citation needed]} Given the rule $${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))}$$ and the term $${\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} )),}$$ attempting to find a matching substitution of the rule's left-hand side, ${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)}$, within ${\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))}$ will fail, since ${\displaystyle y}$ cannot match ${\displaystyle \operatorname {cons} (y,\mathrm {nil} )}$. However, if the rule is replaced by a fresh copy^[a] $${\displaystyle \operatorname {append} (\operatorname {cons} (v_{1},v_{2}),v_{3})\to \operatorname {cons} (v_{1},\operatorname {append} (v_{2},v_{3}))}$$ before, matching will succeed with the answer substitution $${\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}.}$$