Sequences

A sequence is a function from 1..n

You already have everything you need for this: a sequence of length n is just a function whose domain is 1..n. <<10, 20, 30>> is a function mapping 1 to 10, 2 to 20, 3 to 30 — which is exactly why indexing a sequence looks like function application:

Q == <<10, 20, 30>>
Q[2] = 20   \* true — same [ ] syntax as any other function

The sequence operators below all live in the Sequences standard module, so you'll need EXTENDS Sequences (alongside Naturals, if you're using numbers) to use them.

The core operators

Head(Q) = 10
Tail(Q) = <<20, 30>>
Len(Q) = 3
Append(Q, 40) = <<10, 20, 30, 40>>
Q \o <<40, 50>> = <<10, 20, 30, 40, 50>>

The empty sequence is <<>>, with Len(<<>>) = 0.

Seq(S): the set of all sequences over S

Seq(S) is every possible finite sequence whose elements come from S — length 0, length 1, length 2, all of them. You can check whether one specific sequence belongs to it, same as any other set membership:

Q \in Seq(Nat)   \* true

Here's the catch, and it's worth knowing before you trip over it: for any nonempty S, Seq(S) is infinite — there's no longest sequence. TLC can check whether one concrete sequence is in Seq(S) (that's decidable — just check every element is in S), but it cannot enumerate Seq(S) to check a quantifier over it:

\E s \in Seq(Nat) : Len(s) = 3
\* Error: TLC encountered a non-enumerable quantifier bound Seq(Nat)

Contrast this with 1..8 or SUBSET {1,2} from earlier chapters — both finite, both fully enumerable. Seq(S) for nonempty S never is. You'll use Seq(S) constantly as a type — "this variable holds a sequence of naturals" — just never as something to quantify over directly.

What you'll do in this exercise

Same pattern one more time: fill in ASSUME statements about a concrete sequence, run TLC, fix what it flags. This closes out the Foundations part — everything from here on builds on sets, logic, functions, and sequences to describe systems that actually change over time.