Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** * Always Higher Priority *)(** In this section, we define what it means for a job to always have a higher priority than another job. *)SectionAlwaysHigherPriority.(** Consider any type of jobs ... *)Context {Job : JobType}.(** ... and any JLDP policy. *)Context `{JLDP_policy Job}.(** We say that a job [j1] always has higher priority than job [j2] if, at any time [t], the priority of job [j1] is strictly higher than the priority of job [j2]. *)Definitionalways_higher_priority (j1j2 : Job) :=
forallt, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1.EndAlwaysHigherPriority.(** We note that, under a job-level fixed-priority policy, the property is trivial since job priorities by definition do not change in this case. *)SectionUnderJLFP.(** Consider any type of jobs ... *)Context {Job : JobType}.(** ... and any JLFP policy. *)Context `{JLFP_policy Job}.(** The property [always_higher_priority j j'] is equivalent to a statement about [hep_job]. *)