Require Export prosa.model.priority.edf.
[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]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_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]
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.definitions.workload.bounded.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.workload.edf_athep_bound.


(** * Bound on Higher-or-Equal Priority Workload under EDF Scheduling is Valid *)

(** In this file, we prove that the upper bound on interference
    incurred by a job from jobs with higher-or-equal priority that
    come from other tasks under EDF scheduling (defined in
    [prosa.analysis.definitions.workload.edf_athep_bound]) is
    valid. *)
Section ATHEPWorkloadBoundIsValidForEDF.

  (** Consider any type of tasks, each characterized by a WCET
      [task_cost], a relative deadline [task_deadline], and an arrival
      curve [max_arrivals], ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.
  Context `{MaxArrivals Task}.

  (** ... and any type of jobs associated with these tasks, where each
      job has a task [job_task], a cost [job_cost], and an arrival
      time [job_arrival]. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Consider any kind of processor model. *)
  Context `{PState : ProcessorState Job}.

  (** For brevity, let's denote the relative deadline of a task as [D]. *)
  Let D tsk := task_deadline tsk.

  (** Consider any valid arrival sequence [arr_seq] ... *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** ... with valid job costs. *)
  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

  (** We consider an arbitrary task set [ts] ... *)
  Variable ts : seq Task.

  (** ... and assume that all jobs stem from tasks in this task set. *)
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

  (** We assume that [max_arrivals] is a family of valid arrival
      curves that constrains the arrival sequence [arr_seq], i.e., for
      any task [tsk] in [ts], [max_arrival tsk] is an arrival bound of
      [tsk]. *)
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

  (** Let [tsk] be any task to be analyzed. *)
  Variable tsk : Task.

  (** Consider any schedule. *)
  Variable sched : schedule PState.

  (** Before we prove the main result, we establish some auxiliary lemmas. *)
  Section HepWorkloadBound.

    (** Consider an arbitrary job [j] of [tsk]. *)
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_of_task tsk j.
    Hypothesis H_job_cost_positive: job_cost_positive j.

    (** Consider the busy interval <<[t1, t2)>> of job [j]. *)
    Variable t1 t2 : duration.
    Hypothesis H_busy_interval : busy_interval arr_seq sched j t1 t2.

    (** Let's define [A] as a relative arrival time of job [j] (with
        respect to time [t1]). *)
    Let A := job_arrival j - t1.

    (** Consider an arbitrary shift [Δ] inside the busy interval ...  *)
    Variable Δ : duration.
    Hypothesis H_Δ_in_busy : t1 + Δ < t2.

    (** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
    Let jobs := arrivals_between arr_seq t1 (t1 + Δ).

    (** We define a predicate [EDF_from tsk]. Predicate [EDF_from tsk]
        holds true for any job [jo] of task [tsk] such that
        [job_deadline jo <= job_deadline j]. *)
    Let EDF_from (tsk : Task) (jo : Job) := EDF Job jo j && (job_task jo == tsk).

    (** Now, consider the case where [A + ε + D tsk - D tsk_o ≤ Δ]. *)
    Section ShortenRange.

      (** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
      Variable tsk_o : Task.
      Hypothesis H_tsko_in_ts: tsk_o \in ts.
      Hypothesis H_neq: tsk_o != tsk.

      (** And assume that [A + ε + D tsk - D tsk_o ≤ Δ]. *)
      Hypothesis H_Δ_ge : A + ε + D tsk - D tsk_o <= Δ.

      (** Then we prove that the total workload of jobs with
          higher-or-equal priority from task [tsk_o] over the interval
          [[t1, t1 + Δ]] is bounded by workload over the interval
          [[t1, t1 + A + ε + D tsk - D tsk_o]]. The intuition behind
          this inequality is that jobs that arrive after time instant
          [t1 + A + ε + D tsk - D tsk_o] have lower priority than job
          [j] due to the term [D tsk - D tsk_o]. *)
      Lemma total_workload_shorten_range :
        workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + Δ))
        <= workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + (A + ε + D tsk - D tsk_o))).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
workload_of_jobs (EDF_from tsk_o)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
workload_of_jobs (EDF_from tsk_o)
  (arrivals_between arr_seq t1
     (t1 + (A + 1 + D tsk - D tsk_o)))
      Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
workload_of_jobs (EDF_from tsk_o)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
workload_of_jobs (EDF_from tsk_o)
  (arrivals_between arr_seq t1
     (t1 + (A + 1 + D tsk - D tsk_o)))
        have BOUNDED: t1 + (A + ε + D tsk - D tsk_o) <= t1 + Δ by lia.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
workload_of_jobs (EDF_from tsk_o)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
workload_of_jobs (EDF_from tsk_o)
  (arrivals_between arr_seq t1
     (t1 + (A + 1 + D tsk - D tsk_o)))
        rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) // => j' IN'.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
t1 + (A + 1 + D tsk - D tsk_o) <= job_arrival j' ->
~~ EDF_from tsk_o j'
        rewrite /EDF_from  => ARR'.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
~~ (EDF Job j' j && (job_task j' == tsk_o))
        case: (eqVneq (job_task j') tsk_o) => TSK';
                                             last by rewrite andbF.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
TSK': job_task j' = tsk_o
~~ (EDF Job j' j && true)
        rewrite andbT; apply: contraT  => /negPn.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
TSK': job_task j' = tsk_o
EDF Job j' j -> false
        rewrite /EDF/edf.EDF/job_deadline/job_deadline_from_task_deadline.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
TSK': job_task j' = tsk_o
job_arrival j' + task_deadline (job_task j') <=
job_arrival j + task_deadline (job_task j) -> false
        move: H_job_of_tsk; rewrite TSK' /job_of_task => /eqP -> HEP.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
TSK': job_task j' = tsk_o
HEP: job_arrival j' + task_deadline tsk_o <=
job_arrival j + task_deadline tsk
false
        have LATEST: job_arrival j' <= t1 + A + D tsk - D tsk_o by rewrite /D/A; lia.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
TSK': job_task j' = tsk_o
HEP: job_arrival j' + task_deadline tsk_o <=
job_arrival j + task_deadline tsk
LATEST: job_arrival j' <= t1 + A + D tsk - D tsk_o
false
        have EARLIEST: t1 <= job_arrival j' by apply: job_arrival_between_ge.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_Δ_ge: A + 1 + D tsk - D tsk_o <= Δ
BOUNDED: t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + Δ)
ARR': t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
TSK': job_task j' = tsk_o
HEP: job_arrival j' + task_deadline tsk_o <=
job_arrival j + task_deadline tsk
LATEST: job_arrival j' <= t1 + A + D tsk - D tsk_o
EARLIEST: t1 <= job_arrival j'
false
        by case: (leqP (A + 1 + D tsk) (D tsk_o)); [rewrite /D/A|]; lia.
      Qed.

    End ShortenRange.

    (** Using the above lemma, we prove that the total workload of the
        tasks is at most [bound_on_total_hep_workload(A, Δ)]. *)
    Corollary sum_of_workloads_is_at_most_bound_on_total_hep_workload :
      \sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (EDF_from tsk_o) jobs
      <= bound_on_athep_workload ts tsk A Δ.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
   workload_of_jobs (EDF_from tsk_o) jobs <=
bound_on_athep_workload ts tsk A Δ
    Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
   workload_of_jobs (EDF_from tsk_o) jobs <=
bound_on_athep_workload ts tsk A Δ
      apply leq_sum_seq => tsko INtsko NEQT; fold (D tsk) (D tsko).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsko: Task
INtsko: tsko \in ts
NEQT: tsko != tsk
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko
  (minn (A + 1 + D tsk - D tsko) Δ)
      edestruct (leqP Δ (A + ε + D tsk - D tsko)) as [NEQ|NEQ]; [ | apply ltnW in NEQ].
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsko: Task
INtsko: tsko \in ts
NEQT: tsko != tsk
NEQ: Δ <= A + 1 + D tsk - D tsko
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko Δ
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsko: Task
INtsko: tsko \in ts
NEQT: tsko != tsk
NEQ: A + 1 + D tsk - D tsko <= Δ
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko
  (A + 1 + D tsk - D tsko)
      -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsko: Task
INtsko: tsko \in ts
NEQT: tsko != tsk
NEQ: Δ <= A + 1 + D tsk - D tsko
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko Δ exact: (workload_le_rbf' arr_seq tsko).
      -
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsko: Task
INtsko: tsko \in ts
NEQT: tsko != tsk
NEQ: A + 1 + D tsk - D tsko <= Δ
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko
  (A + 1 + D tsk - D tsko) eapply leq_trans; first by eapply total_workload_shorten_range; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: busy_interval arr_seq sched j t1 t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ < t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
EDF_from:= fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
tsko: Task
INtsko: tsko \in ts
NEQT: tsko != tsk
NEQ: A + 1 + D tsk - D tsko <= Δ
workload_of_jobs (EDF_from tsko)
  (arrivals_between arr_seq t1
     (t1 + (A + 1 + D tsk - D tsko))) <=
task_request_bound_function tsko
  (A + 1 + D tsk - D tsko)
        exact: workload_le_rbf'.
    Qed.

  End HepWorkloadBound.

  (** The validity of [bound_on_athep_workload] then easily follows
      from lemma [sum_of_workloads_is_at_most_bound_on_total_hep_workload]. *)
  Corollary bound_on_athep_workload_is_valid :
    athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk).
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
athep_workload_is_bounded arr_seq sched tsk
  (bound_on_athep_workload ts tsk)
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
athep_workload_is_bounded arr_seq sched tsk
  (bound_on_athep_workload ts tsk)
    move=> j t1 Δ POS TSK QT.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
TSK: job_of_task tsk j
QT: quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ
    eapply leq_trans.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
TSK: job_of_task tsk j
QT: quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + Δ)) <= ?n
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
TSK: job_of_task tsk j
QT: quiet_time arr_seq sched j t1
?n <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ
    +
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
TSK: job_of_task tsk j
QT: quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
  (arrivals_between arr_seq t1 (t1 + Δ)) <= ?n eapply reorder_summation => j' IN _.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
TSK: job_of_task tsk j
QT: quiet_time arr_seq sched j t1
j': Job
IN: j' \in arrivals_between arr_seq t1 (t1 + Δ)
job_task j' \in ?ys
      by apply H_all_jobs_from_taskset; eapply in_arrivals_implies_arrived; exact IN.
    +
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
TSK: job_of_task tsk j
QT: quiet_time arr_seq sched j t1
\sum_(y <- ts | y != job_task j)
   \sum_(x <- arrivals_between arr_seq t1 (t1 + Δ) | 
   (hep_job^~ j) x && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ move : TSK => /eqP TSK; rewrite TSK.
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: MaxArrivals Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
D:= [eta task_deadline]: Task -> duration
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals
  arr_seq ts
tsk: Task
sched: schedule PState
j: Job
t1: instant
Δ: duration
POS: job_cost_positive j
QT: quiet_time arr_seq sched j t1
TSK: job_task j = tsk
\sum_(y <- ts | y != tsk)
   \sum_(x <- arrivals_between arr_seq t1 (t1 + Δ) | 
   hep_job x j && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ
      by apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload => //; apply /eqP.
  Qed.

End ATHEPWorkloadBoundIsValidForEDF.