sequence

An ordered list of values of a domain.

Can be defined using sequence (attributes) of <domain> The sequence must be bounded, so need a size or maxSize attribute.

Can also be explicitly defined by a list of values in round brackets as: letting x be sequence (1,2,5)

You can refer to individual values of a sequence using it’s index, which starts at one. The first element of a sequence, s is referred to be s(1).

Sequences with attributes are treated like a function, mapping the index to the corresponding value. Sequences can have

They are total by default, so don’t have a separate total attribute.

See this demonstrated here. Read more about sequence domains here.