-
Currently, the file `prosa.analysis.facts.busy_interval.pi` makes the assumption that the schedule is work-conserving (in the classic sense). Results from this file are used to bound the service inversion. Therefore, the service inversion file also relies on the classic work-conservation hypothesis, which is too limiting in some contexts. This patch removes the work-conservation hypothesis from some of the results in the PI file. Removing the work conservation hypothesis crucially requires strengthening two lemmas regarding preemption.
