Require Import 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 "_ + _" 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 Import prosa.model.task.absolute_deadline.
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]

(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.

  (** Consider any type of tasks with relative deadlines ... *)
  Context {Task : TaskType}.
  Context `{TaskDeadline Task}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** EDF respects sequential tasks hypothesis. *)
  Lemma EDF_respects_sequential_tasks:
    policy_respects_sequential_tasks.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
policy_respects_sequential_tasks
  Proof.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
policy_respects_sequential_tasks
    intros j1 j2 TSK ARR.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
TSK: job_task j1 == job_task j2
ARR: job_arrival j1 <= job_arrival j2
hep_job j1 j2
    move: TSK => /eqP TSK.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
ARR: job_arrival j1 <= job_arrival j2
TSK: job_task j1 = job_task j2
hep_job j1 j2
    unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
ARR: job_arrival j1 <= job_arrival j2
TSK: job_task j1 = job_task j2
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
      by rewrite leq_add2r.
  Qed.

End PropertiesOfEDF.

(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply it automatically. *)
Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.


Require Export prosa.model.task.sequentiality.
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.facts.busy_interval.priority_inversion.
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.facts.priority.sequential.
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]

(** In this section, we prove that EDF priority policy 
    implies that tasks are sequential. *)
Section SequentialEDF.  

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.

  (** ... with a bound on the maximum non-preemptive segment length.
      The bound is needed to ensure that, at any instant, it always 
      exists a subsequent preemption time in which the scheduler can, 
      if needed, switch to another higher-priority job. *)
  Context `{TaskMaxNonpreemptiveSegment Task}.
  
  (** Further, consider any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.
  
  (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
  Variable sched : schedule (ideal.processor_state Job).
  
  (** ... allow for any work-bearing notion of job readiness, ... *)
  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

  (** ... and assume that the schedule is valid. *)
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
  
  (** 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 with
      bounded non-preemptive segments. *)
  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

  (** Next, we assume that the schedule respects the policy defined by
      the [job_preemptable] function (i.e., jobs have bounded
      non-preemptive segments). *)
  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

  (** To prove sequentiality, we use lemma
      [early_hep_job_is_scheduled]. Clearly, under the EDF priority
      policy, jobs satisfy the conditions described by the lemma
      (i.e., given two jobs [j1] and [j2] from the same task, if [j1]
      arrives earlier than [j2], then [j1] always has a higher
      priority than job [j2], and hence completes before [j2]);
      therefore EDF implies sequential tasks. *)
  Lemma EDF_implies_sequential_tasks:
    sequential_tasks arr_seq sched.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
sequential_tasks arr_seq sched
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
sequential_tasks arr_seq sched
    intros ? ? ? ARR1 ARR2 SAME LT.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
scheduled_at sched j2 t -> completed_by sched j1 t
    eapply early_hep_job_is_scheduled => //; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
transitive_priorities
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
transitive_priorities
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2 by rt_auto.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2 move : H_valid_model_with_bounded_nonpreemptive_segments => [VALID _]; apply VALID.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2
    -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2 clear t; intros ?.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
t: instant
hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1
      move: SAME => /eqP SAME.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1
      apply /andP.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
hep_job_at t j1 j2 /\ ~~ hep_job_at t j2 j1
      rewrite /hep_job_at /JLFP_to_JLDP /hep_job /edf.EDF /job_deadline
               /absolute_deadline.job_deadline_from_task_deadline SAME.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2) /\
~~
(job_arrival j2 + task_deadline (job_task j2) <=
 job_arrival j1 + task_deadline (job_task j2)) 
      split.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
~~
(job_arrival j2 + task_deadline (job_task j2) <=
 job_arrival j1 + task_deadline (job_task j2))
      +
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
~~
(job_arrival j2 + task_deadline (job_task j2) <=
 job_arrival j1 + task_deadline (job_task j2)) by rewrite leq_add2r ltnW.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
~~
(job_arrival j2 + task_deadline (job_task j2) <=
 job_arrival j1 + task_deadline (job_task j2))
      +
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched 
  (EDF Job)
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
LT: job_arrival j1 < job_arrival j2
t: instant
SAME: job_task j1 = job_task j2
~~
(job_arrival j2 + task_deadline (job_task j2) <=
 job_arrival j1 + task_deadline (job_task j2)) by rewrite -ltnNge ltn_add2r. 
  Qed.

End SequentialEDF.