Reasoning principles for ideal schedules
While fixing the proofs in order to implement !54 (merged) I realized that we end up repeating simple case analyses on
sched t which then requires using unfolding lemmas to relate
sched t to the fact that some job is scheduled/receiving service at t. I believe that we could formulate a lemma to streamline this process.
Unfortunately I don't have the time to work on this right now but I'll use this issue to collect my experiments once I get to it.