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 ...
  Context {Task : TaskType}.
  Context `{PeriodicModel Task}.

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

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

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_j1_of_task: job_task j1 = tsk.
    Hypothesis H_j2_of_task: job_task j2 = tsk.
    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.
    Hypothesis H_j1_of_task: job_task j1 = tsk.
    Hypothesis H_j2_of_task: job_task j2 = tsk.

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.
  Hypothesis H_j1_of_task: job_task j1 = tsk.
  Hypothesis H_j2_of_task: job_task j2 = tsk.

Without loss of generality, we assume that job j1 arrives before job j2.
We generalize the above lemma to show that any two unequal jobs of task tsk are separated by a non-zero multiple of task_period tsk.
  Lemma job_sep_periodic:
     n,
      n > 0
      job_arrival j2 = job_arrival j1 + n × task_period tsk.

End JobArrivalSeparation.