Does this predicate really hold for nonpreemptive fixed-priority scheduling?
https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/model/schedule/uni/basic/platform.v#L51-56