Library rt.restructuring.analysis.basic_facts.task_arrivals

From rt.restructuring.model.aggregate Require Export task_arrivals.

In this file we provide basic properties related to tasks on arrival sequences.
Section TaskArrivals.

Consider any type of job associated with any type of tasks.
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.

Consider any job arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Let tsk be any task.
  Variable tsk : Task.

We show that the number of arrivals of task can be split into disjoint intervals.
  Lemma num_arrivals_of_task_cat:
    ∀ t t1 t2,
      t1 ≤ t ≤ t2 →
      number_of_task_arrivals arr_seq tsk t1 t2 =
      number_of_task_arrivals arr_seq tsk t1 t + number_of_task_arrivals arr_seq tsk t t2.

End TaskArrivals.