Es sei S {\displaystyle {}S} ein Symbolalphabet, s 1 , … , s n , t 1 , … , t n {\displaystyle {}s_{1},\ldots ,s_{n},t_{1},\ldots ,t_{n}} seien S {\displaystyle {}S} -Terme, x 1 , … , x n {\displaystyle {}x_{1},\ldots ,x_{n}} verschiedene Variablen und α {\displaystyle {}\alpha } sei ein S {\displaystyle {}S} -Ausdruck.
Dann ist
ableitbar.
ein
Symbolalphabet,
seien
-Terme,
verschiedene Variablen und 
sei ein
-Ausdruck.
