# 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 ...

... 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 periodic task tsk with a valid offset and period.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_period: valid_period 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_index arr_seq j = n
Proof.
elim⇒ [|n IHn].
{ intros j ARR TSK_IN ZINDEX.
exact: first_job_arrival ZINDEX.
}
{ intros j ARR TSK_IN JB_INDEX.
move : (H_task_respects_periodic_model j ARR) ⇒ PREV_JOB.
feed_n 2 PREV_JOB ⇒ //.
move : PREV_JOB ⇒ [pj [ARR' [IND [TSK ARRIVAL]]]].
specialize (IHn pj); feed_n 3 IHn ⇒ //; first by rewrite IND JB_INDEX; lia.
rewrite ARRIVAL IHn; lia.
}
Qed.

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
Proof.
movej ARR TSK.
(job_index arr_seq j).
specialize (periodic_arrival_times (job_index arr_seq j) j) ⇒ J_ARR.
by feed_n 3 J_ARR ⇒ //.
Qed.

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_index arr_seq j = n.
Proof.
have F : task_period tsk > 0 by auto.
elim⇒ [|n IHn].
+ movej ARR_J TSK ARR.
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] ⇒ //.
by apply periodic_arrival_times in SUCC ⇒ //; lia.
+ movej ARR_J TSK ARR.