Beweisverfahren für Termination

• syntaktisch: Bsp. für {ba→ab}:

  aus u→v folgt | u| = | v| und u > lexv für b > a

  Vorsicht: für {ba→aabb} gilt auch u > lexv

• semantisch: Bsp. für {ba→ab}:

  Anzahl der Inversionen f (w) : = |{(i, j) | i < j∧w_i > w_j}|

  ist eine Schrittfunktion (aus u→v folgt f (u) > f (v))

• Transformation: Bsp. für {aa→aba}:

  jeder Buchstabe markiert mit seinem rechten Nachbarn

  {a_aa_a→a_bb_aa_a, a_aa_b→a_bb_aa_b}, Anzahl d. a_a ist Schrittfkt.

• Modularität: SN(R₁)∧SN(R₂)∧ weitere Bedingungen $\implies$SN(R₁∪R₂). Vorsicht: R₁ = {a→b}, R₂ = {b→a}