[jonsen]

> At every place X in the following expression, introduce a boolean negation if there isn’t one (or, equivanently remove one if there is), and

I think it should read:

At every place X in the following expression, introduce a boolean negation if there isn’t one and remove one if there is, and

Maybe even better:

At every place X in the following expression, introduce a boolean negation. If you get two concecutive NOT's, they can be removed.

Next, I don't see how

  timespent <= duration

is the negation of

  duration > time_spent

?