\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{../lib/tex/naproche}

\newcommand{\reduces}[1]{\to_{#1}}
\newcommand{\reducesTC}[1]{\to_{#1}^{+}}
\newcommand{\reducesTCR}[1]{\to_{#1}^{*}}



\title{Newman's lemma}
\author{Andrei Paskevich (2007), \\
Steffen Frerix and Peter Koepke (2018), \\
Adrian De Lon (typesetting, 2021)}
\date{}

\begin{document}
  \pagenumbering{gobble}

  \maketitle

  \begin{forthel}
    [synonym element/-s]
    [synonym system/-s]
    [synonym reduct/-s]
    [synonym term/-s]

    \begin{signature}
      An term is an object.
    \end{signature}

    \begin{signature}
      A rewriting system is a notion.
    \end{signature}

    Let $a,b,c,d,u,v,w,x,y,z$ denote terms.

    Let $R$ denote a rewriting system.

    \begin{signature}[Reduct]
      A reduct of $x$ in $R$ is a term.
    \end{signature}

    Let $x \reduces{R} y$ stand for $y$ is a reduct of $x$ in $R$.

    \begin{signature}
      $x \reducesTC{R} y$ is a relation.
    \end{signature}

    \begin{axiom}
      $x \reducesTC{R} y$ iff $x \reduces{R} y$
      or there exists a term $z$ such that
      $x \reduces{R} z \reducesTC{R} y$.
    \end{axiom}

    \begin{axiom}
      If $x \reducesTC{R} y \reducesTC{R} z$ then $x \reducesTC{R} z$.
    \end{axiom}

    \begin{definition}
      $x \reducesTCR{R} y$ iff $x = y$ or $x \reducesTC{R} y$.
    \end{definition}

    \begin{lemma}
      If $x \reducesTCR{R} y \reducesTCR{R} z$ then $x \reducesTCR{R} z$.
    \end{lemma}

    \begin{definition}
      $R$ is confluent iff for all $a,b,c$ such that $a \reducesTCR{R} b,c$ there exists $d$ such that $b,c \reducesTCR{R} d$.
    \end{definition}

    \begin{definition}
      $R$ is locally confluent iff for all $a, b, c$ such that
      $a \reduces{R} b, c$
      there exists $d$ such that $b, c \reducesTCR{R} d$.
    \end{definition}

    \begin{definition}[Terminating]
      $R$ is terminating iff
      for all $a, b$ such that $a \reducesTC{R} b$ we have $b \prec a$.
    \end{definition}

    \begin{definition}
      A normal form of $x$ in $R$ is a term $y$ such that
      $x \reducesTCR{R} y$ and $y$ has no reducts in $R$.
    \end{definition}

    \begin{lemma}
      Let $R$ be a terminating rewriting system.
      Every term $x$ has a normal form in $R$.
    \end{lemma}
    \begin{proof}[by induction]
    \end{proof}


    \begin{lemma}[Newman]
      Every locally confluent terminating rewriting system is confluent.
    \end{lemma}
    \begin{proof}
      Let $R$ be a rewriting system. Assume $R$ is locally confluent and
      terminating.

      Let us demonstrate by induction that for all $a,b,c$ such that $a \reducesTCR{R} b,c$ there exists $d$ such that $b,c \reducesTCR{R} d$.
        Let $a,b,c$ be terms. Assume $a \reducesTC{R} b,c$.

        Take $u$ such that $a \reduces{R} u \reducesTCR{R} b$.
        Take $v$ such that $a \reduces{R} v \reducesTCR{R} c$.
        Take $w$ such that $u,v \reducesTCR{R} w$.
        Take a normal form $d$ of $w$ in $R$.

        $b \reducesTCR{R} d$. Indeed take $x$ such that $b,d \reducesTCR{R} x$. 
        $c \reducesTCR{R} d$. Indeed take $y$ such that $c,d \reducesTCR{R} y$.
      End.
    \end{proof}
  \end{forthel}

\end{document}
