Car Talk is a U.S. radio program about car repair. Each show includes a puzzle, which is often a little mathematical problem. Usually, those problems are easy for a mathematically sophisticated listener to solve. However, I was not able immediately to see how to solve the puzzle from the 22 October 2011 program. I decided to specify the problem in TLA+ and let TLC (the TLA+ model checker) compute the solution. This is the specification I wrote. (I have tried to explain in comments all TLA+ notation that is not standard mathematical notation.) Once TLC had found the solution, it was not hard to understand why it worked.
Here is the problem. A farmer has a 40 pound stone and a balance scale. How can he break the stone into 4 pieces so that, using those pieces and the balance scale, he can weigh out any integral number of pounds of corn from 1 pound through 40 pounds.
The following statement imports the standard operators of arithmetic such as + and =< (less than or equals). It also defines the operator .. so that i..j is the set of all integers k with i =< k =< j.