Lokale Konfluenz und Konfluenz

• Lemma von Newman: SN∧WCR$\implies$CR
• Beweis (nach Henk Barendregt, zitiert in TeReSe)
  • wegen SN hat jedes a∈U wenigstens eine Nf.
  • wir zeigen: ...genau eine Nf. Daraus folgt CR.
    • Bezeichnung: a mehrdeutig (M(a)): hat ≥2 Nf.
    • zeigen: wenn M(a), dann exist b mit a→b und M(b).

      daraus folgt ¬∃a : M(a), sonst Widerspruch zu SN

    • Falls M(a), dann a→b₁→^*n₁ und a→b₂→^*n₂ mit n₁≠n₂ Nf.

      WCR: existiert c mit b₁→^*c←^*b₂ und c→^*n Nf.

      Dann n₁≠n oder n₂≠n, also M(b₁) oder M(b₂).