# Library prosa.analysis.facts.periodic.arrival_times

Require Export prosa.model.task.arrival.periodic_as_sporadic.
Require Export prosa.analysis.facts.periodic.max_inter_arrival.
Require Export prosa.analysis.facts.model.offset.
In this module, we'll prove the known arrival times of jobs that stem from periodic tasks.
Section PeriodicArrivalTimes.
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 ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... 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.