On main canonical notion of $\delta$-reduction

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