Why does $y \downarrow x$ imply $ x \leftrightarrow^* y$?

Question

In Baader's Term rewriting and all that:

Definition 2.1.3 A reduction $\rightarrow$ is called Church-Rosserf iff $ x \leftrightarrow^* y \Rightarrow y \downarrow x$

Because $y \downarrow x$ implies $ x \leftrightarrow^* y$, the Church-Rosser property can also be phrased as an equivalence: $x \leftrightarrow^* y \Leftrightarrow x \downarrow y$.

Why does $y \downarrow x$ imply $ x \leftrightarrow^* y$? (In other words, why if y and x have a common successor, then they are equivalent?)

For the definitions, also see https://en.wikipedia.org/wiki/Rewriting#Normal_forms,_joinability_and_the_word_problem

Thanks.

Answer 1

The definition of symmetric closure, $\ \leftrightarrow\ :=\ \rightarrow \cup \leftarrow\ =\ \rightarrow \cup \ (\rightarrow)^{-1}\ $, means that two objects satisfy this relation if either $x \rightarrow y$ or $y \rightarrow x$. Hence $x \leftrightarrow^* y$ can be interpreted as "either $x=y$ or there exists a path, regardless of arrow direction, connecting $x$ and $y$."

The implication $\exists z(x \rightarrow^* z \leftarrow^* y) \Rightarrow x \leftrightarrow^* y$ should now make sense intuitively.