Library prosa.analysis.facts.periodic.task_arrivals_size

In this file we prove some properties concerning the size of task arrivals in context of the periodic model.
Section TaskArrivalsSize.

Consider any type of 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.
We show that if an instant t is not an "arrival time" for task tsk then task_arrivals_at arr_seq tsk t is an empty sequence.
  Lemma task_arrivals_size_at_non_arrival:
     t,
      ( n, t task_offset tsk + n × task_period tsk)
      task_arrivals_at arr_seq tsk t = [::].

We show that at any instant t, at most one job of task tsk can arrive (i.e. size of task_arrivals_at arr_seq tsk t is at most one).
  Lemma task_arrivals_at_size_cases:
     t,
      size (task_arrivals_at arr_seq tsk t) = 0
        size (task_arrivals_at arr_seq tsk t) = 1.

We show that the size of task arrivals (strictly) between two consecutive arrival times is zero.
  Lemma size_task_arrivals_between_eq0:
     n,
      let l := (task_offset tsk + n × task_period tsk).+1 in
      let r := (task_offset tsk + n.+1 × task_period tsk) in
      size (task_arrivals_between arr_seq tsk l r) = 0.

In this section we show some properties of task arrivals in case of an infinite sequence of jobs.
Assume that we have an infinite sequence of jobs.
    Hypothesis H_infinite_jobs : infinite_jobs arr_seq.

We show that for any number n, there exists a job j of task tsk such that job_index of j is equal to n and j arrives at task_offset tsk + n × task_period tsk.
    Lemma jobs_exists_later:
       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.

We show that the size of task arrivals at any arrival time is equal to one.
    Lemma task_arrivals_at_size:
       n,
        let l := (task_offset tsk + n × task_period tsk) in
        size (task_arrivals_at arr_seq tsk l) = 1.

We show that the size of task arrivals up to task_offset tsk is equal to one.
We show that for any number n, the number of jobs released by task tsk up to task_offset tsk + n × task_period tsk is equal to n + 1.
    Lemma task_arrivals_up_to_size:
       n,
        let l := (task_offset tsk + n × task_period tsk) in
        let r := (task_offset tsk + n.+1 × task_period tsk) in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1.

We show that the number of jobs released by task tsk at any instant t and t + n × task_period tsk is the same for any number n.