Equivalence of EDF Predicates

This MR connects the two ways with which one can specify that a schedule is an EDF schedule in PROSA: the EDF_schedule predicate and the respects_policy_at_preemption_point - given the EDF priority policy - predicate. We connect these two predicates by showing that they're equivalent. We then restate the optimality proof of EDF schedules using the proven equivalence.