Skip to content

Refactor assumptions in a lemma about RBF

Sergey Bozhko requested to merge sbozhko/rt-proofs:clean-up into master

Lemma about task_rbf ε >= task_cost tsk assumes that there exists a job of tsk. However, the only goal of assuming the existence of a job is to obtain the fact that max_arrivals tsk ε > 0. One can directly assume that the arrival curve is positive and hence remove the superfluous dependency.

Merge request reports