Actually, the two formulas
/\ sem = 1 /\ sem' = sem - 1 /\ sem' = 0 /\ sem' = 0are equivalent only under the assumption that
sem is a
number. That assumption is justified in the puzzle, because we
are showing that the original algorithm and the one obtained with the
different Lock operation are equivalent by showing that their
lock actions are equivalent. To do that, it
suffices to show that the two formulas are equivalent for every
reachable state of the algorithms, and sem is a number in
every reachable state of each algorithm. However, while the
first formula implies that sem is a number, the second
formula by itself doesn't.
How can sem not be a number? After all, in
high-school algebra, you learned how to solve the pair of equations in
the second formula and deduce that sem equals 1.
However, the reasoning used to solve those two equations is based on the
assumption that sem and sem' are numbers.
The second equation says that sem' equals 0, which is
a number. But the equation
sem' = sem - 1
does not imply that sem is a number. TLA+ defines the
meaning of subtraction only of numbers. It doesn't define what
sem - 1 equals—or doesn't equal—if
sem is not a number.
For example, it doesn't say that "xyz" - 1 does not
equal 0. If it does equal 0, then sem = "xyz" and
sem' = 0 satisfies the second formula but not the first,
so the two formulas aren't equivalent.