English
If words w1 and w2 reduce to w' and w'' respectively, then there exists a word w''' that both w' and w'' reduce to (joinable).
Русский
Если слова w1 и w2 редуцируются к w' и w'' соответственно, то существует слово w''' к которому редуцируются и w' и w''.
LaTeX
$$$\forall L_1,L_2:\; Red(L_1,L_2) \rightarrow Red(L_1,L_3) \rightarrow Join(Red)L_2,L_3$$$
Lean4
/-- **Church-Rosser theorem** for word reduction: If `w1 w2 w3` are words such that `w1` reduces
to `w2` and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4`
respectively. This is also known as Newman's diamond lemma. -/
@[to_additive /-- **Church-Rosser theorem** for word reduction: If `w1 w2 w3` are words such that `w1` reduces
to `w2` and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4`
respectively. This is also known as Newman's diamond lemma. -/
]
theorem church_rosser : Red L₁ L₂ → Red L₁ L₃ → Join Red L₂ L₃ :=
Relation.church_rosser fun _ b c hab hac =>
match b, c, Red.Step.diamond hab hac rfl with
| b, _, Or.inl rfl => ⟨b, by rfl, by rfl⟩
| _, _, Or.inr ⟨d, hbd, hcd⟩ => ⟨d, ReflGen.single hbd, hcd.to_red⟩
