Sequence Basics

Fill in the six TODO assumptions in starter.tla so that every ASSUME statement is true, then click Run Model Checker.

Given: Q == <<10, 20, 30>>.

1. The first element of Q is 10.
2. Everything after the first element is <<20, 30>>.
3. Q has 3 elements.
4. Appending 40 to Q gives <<10, 20, 30, 40>>.
5. Concatenating Q with <<40, 50>> gives <<10, 20, 30, 40, 50>>.
6. Q is a sequence of natural numbers.