What do you think of this way of defining work-conservation in a way that transparently works for both uni- and multiprocessor platforms?
To me, this looks appealing. The only downside that I see is that in proofs one doesn't get to destruct the
exists j_other right away (i.e., we'd need a few helper lemmas to establish that
idle_in s == 0 implies
We could also keep both notions and establish equivalency of the two definitions (once for each processor model).