Require Export prosa.analysis.facts.model.ideal.schedule.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.deadlines.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.definitions.schedulability.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.priority.edf.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.schedule.edf.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.schedule.priority_driven.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Import prosa.model.readiness.basic.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Import prosa.model.preemption.fully_preemptive.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** * Equivalence of EDF Definitions *)

(** Recall that we have defined "EDF schedules" in two ways.

    The generic way to define an EDF schedule is by using the EDF priority
    policy defined in [model.priority.edf] and the general notion of
    priority-compliant schedules defined in [model.schedule.priority_driven].

    Another, more straight-forward way to define an EDF schedule is the standalone
    definition given in [model.schedule.edf], which is less general but simpler
    and used in the EDF optimality proof.

    In this file, we show that both definitions are equivalent assuming:

    (1) ideal uniprocessor schedules,

    (2) the classic Liu & Layland model of readiness without jitter and
    without self-suspensions, where pending jobs are always ready, and

    (3) that jobs are fully preemptive. *)

Section Equivalence.

  (** We assume the basic (i.e., Liu & Layland)
      readiness model under which any pending job is ready. *)
  #[local] Existing Instance basic_ready_instance.

  (** We assume that jobs are fully preemptive. *)
  #[local] Existing Instance fully_preemptive_job_model.

  (** For any given type of jobs, each characterized by an arrival time,
      an execution cost, and an absolute deadline, ... *)
  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

  (** ...consider a given valid job arrival sequence ... *)
  Variable arr_seq: arrival_sequence Job.
  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

  (** ...and a corresponding schedule. *)
  Variable sched : schedule (ideal.processor_state Job).

  (** Suppose jobs don't execute after their completion, ... *)
  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

  (** ...all jobs come from the arrival sequence [arr_seq], ...*)
  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.

  (** ...and jobs from [arr_seq] don't miss their deadlines. *)
  Hypothesis H_no_deadline_misses: all_deadlines_of_arrivals_met arr_seq sched.

  (** We first show that a schedule that satisfies the standalone
      [EDF_schedule] predicate is also compliant with the generic notion of EDF
      policy defined in Prosa, namely the [respects_policy_at_preemption_point]
      predicate. *)
  Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
    EDF_schedule sched ->
    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job)
  Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job)
    move=> EDF j' j t ARR PREEMPTION BL SCHED.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
hep_job_at t j j'
    have suff: exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
(exists t' : nat,
   t <= t' < job_deadline j' /\
   scheduled_at sched j' t') -> hep_job_at t j j'
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
((exists t' : nat,
    t <= t' < job_deadline j' /\
    scheduled_at sched j' t') -> 
 hep_job_at t j j') -> 
hep_job_at t j j'
    {
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
(exists t' : nat,
   t <= t' < job_deadline j' /\
   scheduled_at sched j' t') -> hep_job_at t j j' move=> [t' [/andP [LE _] SCHED']].
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
t': nat
LE: t <= t'
SCHED': scheduled_at sched j' t'
hep_job_at t j j'
      apply: (EDF t); [done | exact LE | exact SCHED' |].
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
t': nat
LE: t <= t'
SCHED': scheduled_at sched j' t'
job_arrival j' <= t
      by apply: (backlogged_implies_arrived sched j' t). }
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
((exists t' : nat,
    t <= t' < job_deadline j' /\
    scheduled_at sched j' t') -> hep_job_at t j j') ->
hep_job_at t j j'
    apply; apply: incomplete_implies_scheduled_later;
      first by apply: H_no_deadline_misses => //.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF: EDF_schedule sched
j', j: Job
t: instant
ARR: arrives_in arr_seq j'
PREEMPTION: preemption_time sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t
~~ completed_by sched j' t
    by apply: (backlogged_implies_incomplete sched j' t).
  Qed.

  (** Conversely, the reverse direction also holds: a schedule that satisfies
      the [respects_policy_at_preemption_point] predicate is also an EDF
      schedule in the sense of [EDF_schedule]. *)
  Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) ->
    EDF_schedule sched.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job) -> EDF_schedule sched
  Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job) -> EDF_schedule sched
    move=> H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
job_deadline j_hp <= job_deadline j
    case (boolP (j == j_hp)); first by move /eqP => EQ; subst.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
j != j_hp -> job_deadline j_hp <= job_deadline j
    move /neqP => NEQ.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
job_deadline j_hp <= job_deadline j
    exploit (H_priority_driven j j_hp t) => //.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
preemption_time sched t
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
backlogged sched j t
    {
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
arrives_in arr_seq j by apply (H_from_arr_seq _ _ SCHED'). }
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
preemption_time sched t
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
backlogged sched j t
    {
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
preemption_time sched t by rewrite /preemption_time; destruct (sched t). }
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
backlogged sched j t
    {
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
backlogged sched j t apply /andP; split => //.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
job_ready sched j t
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ scheduled_at sched j t
      -
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
job_ready sched j t
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ scheduled_at sched j t apply /andP; split => //.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ completed_by sched j t
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ scheduled_at sched j t
        apply (incompletion_monotonic _ j _ _ LEQ).
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ completed_by sched j t'
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ scheduled_at sched j t
        by apply scheduled_implies_not_completed.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ scheduled_at sched j t
      -
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
~~ scheduled_at sched j t apply /negP; move => SCHED''.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
H_priority_driven: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
t: instant
j_hp: Job
SCHED: scheduled_at sched j_hp t
t': instant
j: Job
LEQ: t <= t'
SCHED': scheduled_at sched j t'
EARLIER_ARR: job_arrival j <= t
NEQ: j <> j_hp
SCHED'': scheduled_at sched j t
False
        by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
  Qed.

  (** From the two preceding lemmas, it follows immediately that the two EDF
      definitions are indeed equivalent, which we note with the following
      corollary. *)
  Corollary EDF_schedule_equiv:
    EDF_schedule sched <-> respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF_schedule sched <->
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job)
  Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF_schedule sched <->
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job)
    split.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job) -> EDF_schedule sched
    -
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job) -> EDF_schedule sched by apply EDF_schedule_implies_respects_policy_at_preemption_point.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job) -> EDF_schedule sched
    -
Job: JobType
H: JobCost Job
H0: JobDeadline Job
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arr_seq_valid: valid_arrival_sequence arr_seq
sched: schedule (ideal.processor_state Job)
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
H_from_arr_seq: jobs_come_from_arrival_sequence sched
  arr_seq
H_no_deadline_misses: all_deadlines_of_arrivals_met
  arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
  (EDF Job) -> EDF_schedule sched by apply respects_policy_at_preemption_point_implies_EDF_schedule.
  Qed.

End Equivalence.