Logic Basics

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

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

1. 3 is odd or 3 is even (at least one must hold).
2. If 6 is even, then 6 is in All.
3. If 100 is even, then 1 = 2. (This one is true — think about why before you decide it looks wrong.)
4. 4 is even if and only if 4 is not odd.
5. Every element of Evens is actually an even number.
6. Some element of Odds is greater than 5.
7. The last ASSUME is already written and already true — but it won't parse. Add parentheses to fix it without changing what it claims.

If you get a "Precedence conflict" error, that's not a bug in the exercise — re-read the gotcha section on this lesson's page.