English
If L1 reduces to L2, then the two words have a common maximal reduction; hence their maximal reductions are equal: reduce(L1) = reduce(L2).
Русский
Если L1 редуцируется до L2, то их максимальные редукции совпадают: reduce(L1) = reduce(L2).
LaTeX
$$$$\text{If } \operatorname{Red}(L_1,L_2), \; \operatorname{reduce}(L_1) = \operatorname{reduce}(L_2).$$$$
Lean4
/-- If a word reduces to another word, then they have a common maximal reduction. -/
@[to_additive /-- If a word reduces to another word, then they have a common maximal reduction. -/
]
theorem eq_of_red (H : Red L₁ L₂) : reduce L₁ = reduce L₂ :=
let ⟨_L₃, HR13, HR23⟩ := Red.church_rosser reduce.red (Red.trans H reduce.red)
(reduce.min HR13).trans (reduce.min HR23).symm
