Теорема Чёрча-Россера

Если u → v₁ и u → v₂ - конечные редукционные цепочки,
то найдётся такой терм w, что v₁ → w и v₂ → w.

Следствие 1

Если v₁ = v₂, то найдётся такой терм w, что v₁ → w и v₂ → w.

Равенство означает существование редукционных цепочек в обоих направлениях (зигзагообразная линия в верхней части рисунка). Теорема Чёрча-Россера позволяет заполнить недостающие участки на краях диаграммы.