A necessary and sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms

In this paper the canonical notion of $\delta$-reduction is considered. Typed $\lambda$-terms use variables of any order and constants of order $\leq 1$, where the constants of order $1$ are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notion of $\beta\delta$-reduction is the notion of $\delta$-reduction that is used in the implementation of functional programming languages. It is shown that for canonical notion of $\delta$-reduction SI-property is the necessary and sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms.