Library prosa.analysis.facts.model.task_arrivals

Require Export prosa.model.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.