Intuitively, the first two conditions state that the covering normal term behaves like a value restriction (or box operator). Consider the term fvr(x), where fvr is the function symbol corresponding to the value restriction constructor for the role R.  Then fvR(x)
obviously satisfies the first two requirements for covering normal terms. Note that the second condition implies that the function induced by tf is monotonic, i.e., X C Y implies t Ψ ( X ) ⊆ t Ψ ( Y ). The third condition specifies the connection between the covering normal term and the function symbol it covers. With respect to elements of t H ( X ), the values of the functions f 2 ( X 1 , . . , X n ) and f 2 ( Y 1 , . . , Y n ) agree provided that their arguments agree on X . It is easy to see that fvR(x) is a covering normal term for the function symbols corresponding to the value, existential, and (qualified) number restrictions on the role R
(see Proposition 35 below).

Given covering normal terms tf for the function symbols f of a finite set of function symbols E , one can construct a term tE that is a covering normal term for all the elements of E.

Lemma 27. Suppose the ADS (L,M) has covering normal terms and L is based on a set of function symbols F. Denote by t f the covering normal term for the function symbol f, for all f ∈ F. Then, for every finite set E ⊆ F of function symbols, the term

$$t_{E}(x):=\bigwedge_{f\in E}t_{f}(x)$$

is a covering normal term for all f ∈ E . 4.2.2 CORRESPONDENCE TO NORMAL MODAL LOGICS The following result shows that any ADS in whi every function symbol is normal has covering normal terms. Hence, the notion of covering normal terms generalizes the notion of normality in modal logics.

Proposition 28. Let ( L, M ) be an ADS, and assume that f is a normal function symbol in (L, M). Then t f ( x ) := f ( x, L, . . , L ) ∧ f ( L, x, . . , L ) ∧ · · · ∧ f ( L, . . , L, x )
is a covering normal term for f. In particular, if f is nullary (unary), then tf(x) = T
(tf(x) = f(x)) is a covering normal term for f Proof.  The first two conditions in the definition of covering normal terms immediately follow from the definition of normal function symbols. Thus, we concentrate on the third condition. Assume, for simplicity, that f is binary. Suppose W ∈ M and X t X 1 , X 2 , Y 1 , Y 2 ⊆
W with X N X i = X N Y i for i = 1,2, and set F := f 20 . Then F (X N X 1 , X N X 2 ) =
F(X NY1, X NY2). Since F is normal, we know that F(X 
F(X ∩ Y 1 , X ∩ Y 2 ) = F(X, X) ∩ F(X, Y 2 ) ∩ F(Y 1 , X) ∩ F(Y 1 , Y 2 ),