Library prosa.analysis.facts.periodic.arrival_times

In this module, we'll prove the known arrival times of jobs that stem from periodic tasks.
Consider periodic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  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 periodic task tsk with a valid offset and period.
    Variable tsk : Task.
    Hypothesis H_valid_offset: valid_offset arr_seq tsk.
    Hypothesis H_valid_period: valid_period tsk.
    Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk.

We show that the nth job j of task tsk arrives at the instant task_offset tsk + n × task_period tsk.
  Lemma periodic_arrival_times:
     n (j : Job),
      arrives_in arr_seq j
      job_task j = tsk
      job_index arr_seq j = n
      job_arrival j = task_offset tsk + n × task_period tsk.

We show that for every job j of task tsk there exists a number n such that j arrives at the instant task_offset tsk + n × task_period tsk.
  Lemma job_arrival_times:
     j,
      arrives_in arr_seq j
      job_task j = tsk
       n, job_arrival j = task_offset tsk + n × task_period tsk.

If a job j of task tsk arrives at task_offset tsk + n × task_period tsk then the job_index of j is equal to n.
  Lemma job_arr_index:
     n j,
      arrives_in arr_seq j
      job_task j = tsk
      job_arrival j = task_offset tsk + n × task_period tsk
      job_index arr_seq j = n.

End PeriodicArrivalTimes.