Library prosa.analysis.facts.priority.classes

Require Export prosa.model.priority.classes.

In this section, we prove some basic properties about priority relations.
Section BasicLemmas.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

Consider a JLFP policy that indicates a higher-or-equal priority relation.
  Context `{JLFP_policy Job}.

First, we prove that another_hep_job relation is anti-reflexive.
  Lemma another_hep_job_antireflexive :
    ∀ j, ¬ another_hep_job j j.

We show that another_task_hep_job is "task-wise" anti-reflexive; that is, given two jobs j and j' from the same task, another_task_hep_job j' j is false.
  Lemma another_task_hep_job_taskwise_antireflexive :
    ∀ tsk j j',
      job_of_task tsk j →
      job_of_task tsk j' →
      ¬ another_task_hep_job j' j.

End BasicLemmas.