# Library prosa.implementation.refinements.arrival_curve_prefix

Require Export prosa.implementation.refinements.arrival_curve.
In this section, we prove some properties that every valid arrival curve prefix entails.
Section ValidArrivalCurvePrefixFacts.
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.
Lemma has_valid_arrival_curve_prefix_tsk :
has_valid_arrival_curve_prefix tsk.
Next, we show that each time step of the arrival curve prefix must be positive.
Lemma steps_are_positive_if_first_step_is_positive :
∀ st,
st \in get_time_steps_of_task tsk → st > 0.
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.
Lemma time_steps_sorted :
sorted ltn (get_time_steps_of_task tsk).
End ValidArrivalCurvePrefixFacts.