Die Variablensubstitution α t 1 , … , t k x 1 , … , x k {\displaystyle {}\alpha {\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}} für einen S {\displaystyle {}S} -Ausdruck α {\displaystyle {}\alpha } , wobei x 1 , … , x k {\displaystyle {}x_{1},\ldots ,x_{k}} Variablen und t 1 , … , t k {\displaystyle {}t_{1},\ldots ,t_{k}} fixierte S {\displaystyle {}S} -Terme seien.
