Modulare SN-Beweise, relative Termination

• Def: →₁/→₂ ist die Relation →₁⋅→₂^*
• Satz: SN(→₁/→₂)∧SN(→₂)$\implies$SN(→₁∪→₂).

  Sprechweise SN(→₁/→₂): →₁ terminiert relativ zu →₂.

• Beweis (indirekt): jede gemischte Ableitung enthält nur endlich viele →₁, nach dem letzten nur endlich viele →₂.
• Def: wfmA (D, > ,[⋅]) schwach kompatibel mit S: ∀(l, r)∈S, x∈D : [l](x)≥[r](x)
• Satz: Wenn ex. wfmA D: D ist kompatibel mit R und D ist schwach kompatibel mit S, dann SN(→_R/→_S).
• Bsp: SN({c→aabb, ab→ba}), D zählt die c.