Kritische Paare

Für ein Termersetzungssystem R über $ \Sigma$: falls Ein kritisches Paar (s, t) heißt zusammenführbar, falls $ \exists$u : s$ \to_{R}^{*}$u $ \wedge$ t$ \to_{R}^{*}$u.

Satz: ein Termersetzungssystem ist genau dann lokal konfluent, wenn alle kritische Paare zusammenführbar sind.



Johannes Waldmann 2007-01-30