English
Under a confluence-like condition h, if a reduces to b and to c via r in one or more steps, there exists a common descendant d reachable from b and c; precisely, there exists d such that ReflGen r b d and ReflTransGen r c d, and from a one can reach b and c via ReflTransGen, which yields a join for b and c.
Русский
При условии сходности: если a может перейти к b и к c по отношению r, то существует общее продолжение d так, что b и c приводят к одному общему потомку d.
LaTeX
$$$\\\\forall a b c, (r a b \\\\rightarrow r a c \\\\rightarrow \\\\exists d \\, (\\\\operatorname{ReflGen} r b d \\\\land \\\\operatorname{ReflTransGen} r c d)) \\\\Rightarrow \\\\operatorname{ReflTransGen} r a b \\\\Rightarrow \\\\operatorname{ReflTransGen} r a c \\\\Rightarrow \\\\operatorname{Join}(\\\\operatorname{ReflTransGen} r) b c$$$$
Lean4
/-- A sufficient condition for the Church-Rosser property. -/
theorem church_rosser (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) (hab : ReflTransGen r a b)
(hac : ReflTransGen r a c) : Join (ReflTransGen r) b c := by
induction hab with
| refl => exact ⟨c, hac, refl⟩
| @tail d e _ hde ih =>
rcases ih with ⟨b, hdb, hcb⟩
have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
clear hcb
induction hdb with
| refl => exact ⟨e, refl, ReflGen.single hde⟩
| @tail f b _ hfb ih =>
rcases ih with ⟨a, hea, hfa⟩
cases hfa with
| refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
| single hfa =>
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
exact ⟨c, hea.trans hac, hbc⟩
rcases this with ⟨a, hea, hba⟩
cases hba with
| refl => exact ⟨b, hea, hcb⟩
| single hba => exact ⟨a, hea, hcb.tail hba⟩
