| ⇒ u = u u = v ⇒ v = u u = v, v = w ⇒ u = w |
(рефлексивность) (симметричность) (транзитивность) |
| u = v ⇒ u w = v w | (введение операнда) |
| u = v ⇒ w u = w v | (введение оператора) |
| u →α v ⇒ u = v | (правило α) |
| u →β v ⇒ u = v | (правило β) |
| u = v ⇒ λx.u = λx.v | (правило ξ) |