For leaf nodes L and any BDDs φ and e (where e is a conjunction of variables), the following holds:

- Forall(L,φ) = φ
- Forall(e,L) = L
- Forall(e,φ) = (xφ ? Forall(e,φ1) : Forall(e,φ0) ) : if D(xφ)>D(xe)
- Forall(e,φ) = Apply(&,Forall(e1,φ1) : Forall(e1,φ0) ) : if D(xφ)=D(xe)
- Forall(e,φ) = Forall(e1,φ) : if D(xφ)=D(xe)

where in the last three cases, we have φ = (xφ ? φ1 : φ0) and e = (xe ? e1 : e0).