On formalization of notion of $\delta$-reduction in monotonic models of typed $\lambda$-calculus

In this paper monotonic models of typed $\lambda$-calculus are examined. Formal definition of concept of a $\delta$-reduction is given. Strong $\delta$-normalization and strong $\beta\delta$-normalization of terms are proved. The concept of a natural $\delta$-reduction is defined and the necessary and sufficient condition for uniqueness of a $\beta\delta$-normal form for such concept of a $\delta$-reduction is resulted.