WIP: expose number of idle cores
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 exists j_other.
We could also keep both notions and establish equivalency of the two definitions (once for each processor model).