Library prosa.analysis.definitions.work_bearing_readiness
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.model.priority.classes.
Work-Bearing Readiness
Consider any type of job associated with any type of tasks ...
... and any kind of processor state.
Further, allow for any notion of job readiness.
Consider any job arrival sequence, ...
... any schedule of these jobs, ...
... and a JLFP policy that indicates a higher-or-equal priority relation.
If a job [j] is pending at a time instant [t], then (even if it
is not ready at time [t]) there is a job [j_hp] with
higher-or-equal priority that is ready at time instant [t].