# Library prosa.analysis.facts.sporadic.arrival_times

# Job Arrival Times in the Sporadic Model

Consider sporadic tasks ...

... and any type of jobs associated with these tasks.

Consider any unique arrival sequence with consistent arrivals, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any sporadic task tsk that is to be analyzed.

Variable tsk : Task.

Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.

Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.

Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.

Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.

We first show that for any two jobs j1 and j2, j2 arrives after j1
provided job_index of j2 strictly exceeds the job_index of j1.

Lemma lower_index_implies_earlier_arrival:

∀ j1 j2,

arrives_in arr_seq j1 →

arrives_in arr_seq j2 →

job_task j1 = tsk →

job_task j2 = tsk →

job_index arr_seq j1 < job_index arr_seq j2 →

job_arrival j1 < job_arrival j2.

∀ j1 j2,

arrives_in arr_seq j1 →

arrives_in arr_seq j2 →

job_task j1 = tsk →

job_task j2 = tsk →

job_index arr_seq j1 < job_index arr_seq j2 →

job_arrival j1 < job_arrival j2.

In the following, consider (again) any two jobs from the arrival
sequence that stem from task tsk.
NB: The following variables and hypotheses match the premises of
the preceding lemma. However, we cannot move these
declarations before the prior lemma because we need
lower_index_implies_earlier_arrival to be ∀-quantified in
the next proof.

Variable j1 : Job.

Variable j2 : Job.

Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.

Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.

Hypothesis H_j1_task: job_task j1 = tsk.

Hypothesis H_j2_task: job_task j2 = tsk.

Variable j2 : Job.

Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.

Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.

Hypothesis H_j1_task: job_task j1 = tsk.

Hypothesis H_j2_task: job_task j2 = tsk.

As a corollary, we observe that distinct jobs cannot have equal arrival times.