Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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]
New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed. [ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed. New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed. [ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed. [ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed. [ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed. [ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed. [ambiguous-paths,coercions,default]
Notation "_ - _" was already used in scope distn_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]
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.elf_athep_bound. Require Export prosa.analysis.facts.model.rbf. (** * Bound on Higher-or-Equal Priority Workload under ELF 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 ELF scheduling (defined in [prosa.analysis.definitions.workload.elf_athep_bound]) is valid. *) Section ATHEPWorkloadBoundIsValidForELF. (** Consider any type of tasks, each characterized by a WCET [task_cost], a relative deadline [task_deadline], an arrival curve [max_arrivals], and a relative priority point, ... *) Context {Task : TaskType}. Context `{TaskCost Task}. Context `{MaxArrivals Task}. Context `{PriorityPoint 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}. (** 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. (* Consider any fixed-priority scheduling policy. *) Context (FP : FP_policy Task). (** 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 [delta] inside the busy interval ... *) Variable delta : duration. Hypothesis H_delta_in_busy : t1 + delta < t2. (** ... and the set of all arrivals between [t1] and [t1 + delta]. *) Let jobs := arrivals_between arr_seq t1 (t1 + delta). (** Now, we define a predicate to identify jobs from a given task that have priority higher than or equal to [j]. *) Let hep_job_from_tsk (tsk_o : Task) (jo : Job) := hep_job jo j && (job_task jo == 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 [ep_task_interfering_interval_length tsk tsk_o A] is bounded by delta. *) Hypothesis H_delta_ge : ((ep_task_interfering_interval_length tsk tsk_o A) <= delta%:R)%R. (** 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 the workload over the interval [[t1, t1 + ep_task_interfering_interval_length tsk tsk_o A]]. The intuition behind this inequality is that jobs that arrive after time instant [t1 + ep_task_interfering_interval_length tsk tsk_o A] have lower priority than job [j]. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R

ep_task tsk tsk_o -> workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta)) <= workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R

ep_task tsk tsk_o -> workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta)) <= workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o

workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta)) <= workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta

workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta)) <= workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta

workload_of_jobs (fun jo : Job => (hp_task (job_task jo) (job_task j) || hep_task (job_task jo) (job_task j) && hep_job jo j) && (job_task jo == tsk_o)) (arrivals_between arr_seq t1 (t1 + delta)) <= workload_of_jobs (fun jo : Job => (hp_task (job_task jo) (job_task j) || hep_task (job_task jo) (job_task j) && hep_job jo j) && (job_task jo == tsk_o)) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta

forall j0 : Job, j0 \in arrivals_between arr_seq t1 (t1 + delta) -> `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j0 -> ~~ ((hp_task (job_task j0) (job_task j) || hep_task (job_task j0) (job_task j) && hep_job j0 j) && (job_task j0 == tsk_o))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'

~~ ((hp_task (job_task j') (job_task j) || hep_task (job_task j') (job_task j) && hep_job j' j) && (job_task j' == tsk_o))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
TSKo: job_task j' = tsk_o

~ ~ hp_task (job_task j') (job_task j) -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
HEP: hep_job j' j
TSKo: job_task j' = tsk_o
false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
TSKo: job_task j' = tsk_o

~ ~ hp_task (job_task j') (job_task j) -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
TSKo: job_task j' = tsk_o
EP_tsk: hep_task tsk tsk_o && hep_task tsk_o tsk

~ ~ hp_task (job_task j') (job_task j) -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
TSKo: job_task j' = tsk_o
EP_tsk: hep_task tsk tsk_o && hep_task tsk_o tsk

~ ~ hep_task tsk_o (job_task j) && ~~ hep_task (job_task j) tsk_o -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
TSKo: job_task j' = tsk_o
EP_tsk: hep_task tsk tsk_o && hep_task tsk_o tsk

job_of_task tsk j -> ~ ~ hep_task tsk_o (job_task j) && ~~ hep_task (job_task j) tsk_o -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
TSKo: job_task j' = tsk_o
EP_tsk: hep_task tsk tsk_o && hep_task tsk_o tsk

~ ~ hep_task tsk_o tsk && ~~ hep_task tsk tsk_o -> false
by move: EP_tsk => /andP [-> ->].
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
ARR': `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= job_arrival j'
HEP: hep_job j' j
TSKo: job_task j' = tsk_o

false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
HEP: hep_job j' j
TSKo: job_task j' = tsk_o

`|Order.Def.max 0%R (t1%:R + ((A + 1)%:R + task_priority_point tsk - task_priority_point (job_task j')))%R| <= job_arrival j' -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
HEP: hep_job j' j
TSKo: job_task j' = tsk_o

`|Order.Def.max 0%R (t1%:R + ((A + 1)%:R + task_priority_point (job_task j) - task_priority_point (job_task j')))%R| <= job_arrival j' -> false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
H_tsko_in_ts: tsk_o \in ts
H_neq: tsk_o != tsk
H_delta_ge: (ep_task_interfering_interval_length tsk tsk_o A <= delta%:R)%R
EP_tsk: ep_task tsk tsk_o
BOUNDED: `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R| <= t1 + delta
j': Job
IN': j' \in arrivals_between arr_seq t1 (t1 + delta)
TSKo: job_task j' = tsk_o

((job_arrival j')%:R + task_priority_point (job_task j') <= (job_arrival j)%:R + task_priority_point (job_task j))%R -> `|Order.Def.max 0%R (t1%:R + ((A + 1)%:R + task_priority_point (job_task j) - task_priority_point (job_task j')))%R| <= job_arrival j' -> false
by clear; lia. Qed. End ShortenRange. (** Consider the jobs that have priority higher than or equal to [j] released by any task in the same priority band as [tsk] (excluding [tsk]). We prove that the workload of these jobs is at most [bound_on_ep_task_workload]. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_ep_task_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_ep_task_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) task_request_bound_function tsk_o (minn `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| delta)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk

workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_request_bound_function tsk_o (minn `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| delta)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
LEQ: delta <= `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|

workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_request_bound_function tsk_o delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
LEQ: delta <= `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|

workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_request_bound_function tsk_o delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
LEQ: delta <= `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|

workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_workload_between arr_seq tsk_o t1 (t1 + delta)
by apply: workload_of_jobs_weaken => ? /andP[].
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta

workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta

workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta

workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|) <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta

workload_of_jobs (fun jo : Job => hep_job jo j && (job_task jo == tsk_o)) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|) <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta

workload_of_jobs (fun jo : Job => hep_job jo j && (job_task jo == tsk_o)) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|) <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta
EQ: (0 <= ep_task_interfering_interval_length tsk tsk_o A)%R

workload_of_jobs (fun jo : Job => hep_job jo j && (job_task jo == tsk_o)) (arrivals_between arr_seq t1 `|Order.Def.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|) <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk_o: Task
INtsko: tsk_o \in ts
EP_tsk: ep_task tsk tsk_o
NEQT: tsk_o != tsk
GT: `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| <= delta
EQ: (0 <= ep_task_interfering_interval_length tsk tsk_o A)%R

workload_of_jobs (fun jo : Job => hep_job jo j && (job_task jo == tsk_o)) (arrivals_between arr_seq t1 (t1 + `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|)) <= task_request_bound_function tsk_o `|Order.Def.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)|
by apply: rbf_spec' => // ? /andP[]. } } Qed. (** Next, consider a workload of all jobs with priority higher than [j] released by any task in higher priority band. we establish that this workload is at most [bound_on_hp_task_workload]. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= total_hp_request_bound_function_FP ts tsk delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= \sum_(tsk_other <- ts | hp_task tsk_other tsk) task_request_bound_function tsk_other delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
IN': tsk' \in ts
HP_TSK: hp_task tsk' tsk

workload_of_jobs (hep_job_from_tsk tsk') jobs <= task_request_bound_function tsk' delta
by apply: rbf_spec' => // ? /andP[]. Qed. (** To help with further analysis, we establish a useful lemma on partitioning higher-or-equal priority workloads. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && hep_task i tsk && hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

forall x : Task, 'Under[ (x != tsk) && hep_task x tsk && hep_task tsk x ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | ?Goal i) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

forall x : Task, 'Under[ (x != tsk) && hep_task x tsk && hep_task tsk x ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task

'Under[ (tsk' != tsk) && hep_task tsk' tsk && hep_task tsk tsk' ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task

'Under[ hep_task tsk' tsk && hep_task tsk tsk' && (tsk' != tsk) ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task

'Under[ hep_task tsk tsk' && hep_task tsk' tsk && (tsk' != tsk) ]
over.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (fun tsk' : Task => hep_task tsk tsk' && hep_task tsk' tsk && (tsk' != tsk)) i) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs = 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | hep_task tsk i && hep_task i tsk && (i != tsk)) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs + 0 = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) workload_of_jobs (hep_job_from_tsk i) jobs = 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

forall i : Task, (i != tsk) && ~~ hep_task i tsk -> 'Under[ workload_of_jobs (hep_job_from_tsk i) jobs ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) ?Goal0 i = 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

forall i : Task, (i != tsk) && ~~ hep_task i tsk -> 'Under[ workload_of_jobs (hep_job_from_tsk i) jobs ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk

'Under[ workload_of_jobs (hep_job_from_tsk tsk') jobs ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk

'Under[ \sum_(j <- jobs | hep_job_from_tsk tsk' j) job_cost j ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk

forall x : Job, hep_job_from_tsk tsk' x = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
'Under[ 0 ]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk

forall x : Job, hep_job_from_tsk tsk' x = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
j': Job

hep_job_from_tsk tsk' j' = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
j': Job

(hep_task (job_task j') (job_task j) && ~~ hep_task (job_task j) (job_task j') || hep_task (job_task j') (job_task j) && hep_job j' j) && (job_task j' == tsk') = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
j': Job
Tsk_j': (job_task j' == tsk') = true

(hep_task (job_task j') (job_task j) && ~~ hep_task (job_task j) (job_task j') || hep_task (job_task j') (job_task j) && hep_job j' j) && true = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
j': Job

(hep_task tsk' (job_task j) && ~~ hep_task (job_task j) tsk' || hep_task tsk' (job_task j) && hep_job j' j) && true = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
j': Job

job_of_task tsk j -> (hep_task tsk' (job_task j) && ~~ hep_task (job_task j) tsk' || hep_task tsk' (job_task j) && hep_job j' j) && true = false
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk
j': Job

(hep_task tsk' tsk && ~~ hep_task tsk tsk' || hep_task tsk' tsk && hep_job j' j) && true = false
by move: HEP => /negbTE ->.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' != tsk
HEP: ~~ hep_task tsk' tsk

'Under[ 0 ]
over.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) (fun=> 0) i = 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) 0 == 0
by rewrite big_const_idem.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | hep_task tsk i && hep_task i tsk && (i != tsk)) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs + 0 = \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | hep_task tsk i && hep_task i tsk && (i != tsk)) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs = \sum_(tsk_o <- ts | hep_task tsk tsk_o && hep_task tsk_o tsk && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | hep_task tsk i && hep_task i tsk && (i != tsk)) workload_of_jobs (hep_job_from_tsk i) jobs + \sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs == \sum_(tsk_o <- ts | hep_task tsk tsk_o && hep_task tsk_o tsk && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(i <- ts | (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) workload_of_jobs (hep_job_from_tsk i) jobs == \sum_(tsk_o <- ts | hep_task tsk_o tsk && ~~ hep_task tsk tsk_o) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

(fun i : Task => (i != tsk) && hep_task i tsk && ~~ hep_task tsk i) =1 (fun tsk_o : Task => hep_task tsk_o tsk && ~~ hep_task tsk tsk_o)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task

(tsk' != tsk) && hep_task tsk' tsk && ~~ hep_task tsk tsk' = hep_task tsk' tsk && ~~ hep_task tsk tsk'
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: (tsk' != tsk) = false

false = hep_task tsk' tsk && ~~ hep_task tsk tsk'
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' = tsk

false = hep_task tsk' tsk && ~~ hep_task tsk tsk'
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
tsk': Task
NEQ: tsk' = tsk

false = hep_task tsk tsk && ~~ hep_task tsk tsk
by rewrite andbN. Qed. (** Finally, we establish that the workload of jobs with priority higher than or equal to [j] is at most [bound_on_athep_workload]. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_athep_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_athep_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_athep_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta + bound_on_ep_task_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
LT_HP: \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta + bound_on_ep_task_workload ts tsk A delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
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
delta: duration
H_delta_in_busy: t1 + delta < t2
jobs:= arrivals_between arr_seq t1 (t1 + delta): seq Job
hep_job_from_tsk:= fun (tsk_o : Task) (jo : Job) => hep_job jo j && (job_task jo == tsk_o): Task -> Job -> bool
LT_HP: \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta
LT_EP: \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_ep_task_workload ts tsk A delta

\sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs + \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs <= bound_on_hp_task_workload ts tsk delta + bound_on_ep_task_workload ts tsk A delta
by lia. 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]. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task

athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task

athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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 + delta)) <= bound_on_athep_workload ts tsk (job_arrival j - t1) delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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 + delta)) <= ?n
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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) delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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 + delta)) <= ?n
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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 + delta)

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: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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 + delta) | (hep_job^~ j) x && (job_task x == y)) job_cost x <= bound_on_athep_workload ts tsk (job_arrival j - t1) delta
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: PriorityPoint Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
PState: ProcessorState Job
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
FP: FP_policy Task
j: Job
t1: instant
delta: 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 + delta) | hep_job x j && (job_task x == y)) job_cost x <= bound_on_athep_workload ts tsk (job_arrival j - t1) delta
by apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload => //; apply /eqP. Qed. End ATHEPWorkloadBoundIsValidForELF.