Library prosa.analysis.definitions.infinite_jobs
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.arrivals.
In this section we define the notion of an infinite release
of jobs by a task.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any arrival sequence.
We say that a task [tsk] releases an infinite number of jobs
if for every integer [n] there exists a job [j] of task [tsk]
such that [job_index] of [j] is equal to [n].