# Library prosa.analysis.facts.periodic.arrival_separation

In this section we show that the separation between job arrivals of a periodic task is some multiple of their corresponding task's period.
Consider periodic tasks with an offset ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals, ...
... and any task tsk that is to be analyzed.

Assume all tasks have a valid period and respect the periodic task model.
In this section we show that two consecutive jobs of a periodic task have their arrival times separated by their task's period.
Consider any two consecutive jobs j1 and j2 of task tsk.
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_consecutive_jobs: job_index arr_seq j2 = job_index arr_seq j1 + 1.

We show that if job j1 and j2 are consecutive jobs with j2 arriving after j1, then their arrival times are separated by their task's period.
In this section we show that for two unequal jobs of a task, there exists a non-zero multiple of their task's period which separates their arrival times.
Consider any two consecutive jobs j1 and j2 of task tsk that stem from the arrival sequence.
Variable j1 j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.

We'll assume that job j1 arrives before j2 and that their indices differ by an integer k.
Variable k : nat.
Hypothesis H_index_difference_k: job_index arr_seq j1 + k = job_index arr_seq j2 .
Hypothesis H_job_arrival_lt: job_arrival j1 < job_arrival j2.

We prove that arrival of unequal jobs of a task tsk are separated by a non-zero multiple of task_period tsk provided their index differs by a number k.
Consider any two distinct jobs j1 and j2 of task tsk that stem from the arrival sequence.
Variable j1 j2 : Job.
Hypothesis H_j1_neq_j2: j1 j2.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.