Prime numbers sieve

Section 4.4.7 included a functional module specifying the sieve of Eratosthenes to calculate prime numbers.

  fmod SIEVE is
    protecting NAT .
    sort NatList .
    subsort Nat < NatList .
    ...
  endfm

The predefined module of natural numbers (see Section 7.2) is imported in protecting mode. This is justified because the elements of sort Nat are used to generate the lists of natural numbers by means of a subsort declaration and also as arguments of other operators. However, no new operator of result sort Nat is added in the SIEVE module, and all the equations in this module identify elements of sort NatList without identifying different natural numbers.