TLA+ Wiki

Nat, Int, Real
+, −, ∗, /, ^
<=, >=, >, <
..
Infinity

The Sequences module defines operations on finite sequences. We represent a finite sequence as a tuple, so the sequence of three numbers 3, 2, 1 is the triple <<3, 2, 1>>. The Sequences module defines the following operators on sequences:

s \o t: The sequence obtained by concatenating the sequences s and t.
- Example: <<3, 7>> \o <<3>> is equal to <<3, 7, 3>>.
Head(s): The first element of the sequence s.
- Example: Head(<<3,2,1>>) is equal to 3
SelectSeq(s, Test): The subsequence of s consisting of the elements s[i] such that Test(s[i]) equals true.
- Example:
```
PosSubSeq(s) == LET IsPos(n) == n > 0
                in SelectSeq(s, IsPos)
```
  defines PosSubSeq(<<0, 3, −2, 5>>) to be equal to <<3, 5>>
SubSeq(s, m, n): The subsequence <<s[m], s[m + 1], . . . , s[n]>> consisting of the mth through nth elements of s. It is undefined if m < 1 or n > Len(s), except that it equals the empty sequence if m > n.
Append(s, e): The sequence obtained by appending element e to the tail of sequence s.
- Example: Append(<<3, 7>>, 3) equals <<3, 7, 3>>.
Len(s): The length of sequence s.
- Example: Len(<<1,2,3>>) is equal to 3.
Seq(S): The set of all sequences of elements of the set S .
- Example: Seq({3,7}) is equal to <<3, 7>>.
Tail(s): The tail of sequence s, which consists of s with its head element removed.
- Example: Tail(<<3, 7>>) equals <<7>>.

IsFiniteSet(s): A set is finite iff there is a finite sequence containing all its elements.
- Example: IsFiniteSet({1,2,3}) is equal to TRUE
Cardinality(s): The number of elements in the set s. It's only defined for finite sets.
- Example: Cardinality({1,2}) is equal to 2.