Library prosa.implementation.refinements.arrival_curve_prefix

In this section, we prove some properties that every valid arrival curve prefix entails.
Consider a task set with valid arrivals ts, ...
  Variable ts : seq Task.
  Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.

... and a task tsk belonging to ts with positive cost and non-zero arrival bound.
  Variable tsk : Task.
  Hypothesis H_positive_cost : 0 < task_cost tsk.
  Hypothesis H_tsk_in_ts : tsk \in ts.
  Hypothesis H_positive_step : fst (head (0,0) (steps_of (get_arrival_curve_prefix tsk))) > 0.

First, we show that the arrival curve prefix of tsk is valid.
Next, we show that each time step of the arrival curve prefix must be positive.
Next, we show that even shifting the time steps by a positive offset, they remain positive.
  Lemma nonshifted_offsets_are_positive :
     A offs,
      A \in repeat_steps_with_offset tsk offs A > 0.

Finally, we show that the time steps are strictly increasing.