Library prosa.analysis.facts.priority.sequential

In this section, we prove that, given two jobs j1 and j2, if job j1 arrives earlier than job j2 and j1 always has higher priority than j2, then j2 is scheduled only after j1 is completed.
Section SequentialJLFP.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is transitive.
Next, consider any ideal uni-processor schedule of this arrival sequence, ...
... allow for any work-bearing notion of job readiness, ...
... and assume that the schedule is valid.
In addition, we assume the existence of a function mapping jobs to their preemption points ...
  Context `{JobPreemptable Job}.

... and assume that it defines a valid preemption model.
Next, we assume that the schedule respects the scheduling policy at every preemption point....
... and that jobs must arrive to execute.
We show that, given two jobs j1 and j2, if job j1 arrives earlier than job j2 and j1 always has higher priority than j2, then j2 is scheduled only after j1 is completed.
  Lemma early_hep_job_is_scheduled :
     j1 j2,
      arrives_in arr_seq j1
      job_arrival j1 < job_arrival j2
      always_higher_priority j1 j2
       t,
        scheduled_at sched j2 t
        completed_by sched j1 t.

End SequentialJLFP.