Motivation, Plan

• eine Anwendung ist:
  • um x↔^*y zu entscheiden:
  • bestimme x→^*x'∈Nf, y→^*y'∈Nf, teste x' = y'
  funktioniert, falls UNC(→) und SN(→)
• Vorgehen:
  • WCR und SN abhängig vom konkreten → (später)
  • WCR∧SN⇒CR (Lemma von Newman)
  • CR⇒UNC
• CR ist auch bei ¬SN interessant, Bsp: Lambda-Kalkül,

  das ist auch der historische Hintergrund