Church numeral zero test ($\mathsf{Zero}$)

The lambda termreturns the Church Boolean $\mathsf{T}$ on $c_0$ and $\mathsf{F}$ on every positive Church numeral. Zero iterations leave the initial true value, while at least one iteration replaces it by false. Normal-order beta reduction evaluates a numeral conditional without evaluating an unchosen branch.