Set Basics

Fill in the six TODO assumptions in starter.tla so that every ASSUME statement is true, then click Run Model Checker. There's no state machine here — TLC checks each ASSUME once and tells you immediately if any of them is false, pointing at the exact line.

Given: Evens == {2, 4, 6, 8}, Odds == {1, 3, 5, 7}, All == 1..8.

1. 3 is not an even number.
2. Every element of Evens is also in All.
3. The union of Evens and Odds is exactly All.
4. Evens and Odds have nothing in common — their intersection is empty.
5. Removing Odds from All (set difference) leaves exactly Evens.
6. All has 8 elements.

If you get stuck on the wording of an operator, the previous lesson page has a full table of set notation and its TLA+ spelling.