Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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 ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.analysis.facts.behavior.arrivals. Require Export prosa.analysis.definitions.request_bound_function. Require Export prosa.analysis.facts.model.task_arrivals. (** * Lemmas about Workload of Sets of Jobs *) (** In this file, we establish basic facts about the workload of sets of jobs. *) Section WorkloadFacts. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** To begin with, we establish an auxiliary rewriting lemma that allows us to introduce a [filter] on the considered set of jobs, provided the filter predicate [P2] is implied by the job-selection predicate [P1]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall (P1 P2 : pred Job) (jobs : seq Job), (forall j : Job, j \in jobs -> P1 j -> P2 j) -> workload_of_jobs P1 jobs = workload_of_jobs P1 [seq j <- jobs | P2 j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall (P1 P2 : pred Job) (jobs : seq Job), (forall j : Job, j \in jobs -> P1 j -> P2 j) -> workload_of_jobs P1 jobs = workload_of_jobs P1 [seq j <- jobs | P2 j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j

workload_of_jobs P1 jobs = workload_of_jobs P1 [seq j <- jobs | P2 j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j

\sum_(i <- jobs | (i \in jobs) && P1 i) job_cost i = \sum_(i <- jobs | [&& i \in jobs, P2 i & P1 i]) job_cost i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job

(j \in jobs) && P1 j = [&& j \in jobs, P2 j & P1 j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
IN: j \in jobs

true && P1 j = [&& true, P2 j & P1 j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
IN: j \in jobs

P1 j = P2 j && P1 j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
IN: j \in jobs
P1j: ~~ P1 j

false = P2 j && false
by rewrite andbF. Qed. (** We establish that if the predicate [P1] implies the predicate [P2], then the cumulative workload of jobs that respect [P1] is bounded by the cumulative workload of jobs that respect [P2]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall (P1 P2 : pred Job) (jobs : seq Job), (forall j : Job, P1 j -> P2 j) -> workload_of_jobs P1 jobs <= workload_of_jobs P2 jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall (P1 P2 : pred Job) (jobs : seq Job), (forall j : Job, P1 j -> P2 j) -> workload_of_jobs P1 jobs <= workload_of_jobs P2 jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPLIES: forall j : Job, P1 j -> P2 j

\sum_(j <- jobs | P1 j) job_cost j <= \sum_(j <- jobs | P2 j) job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPLIES: forall j : Job, P1 j -> P2 j
j': Job

P1 j' -> P2 j'
by apply: IMPLIES. Qed. (** The cumulative workload of jobs from an empty sequence is always zero. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall P : pred Job, workload_of_jobs P [::] = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall P : pred Job, workload_of_jobs P [::] = 0
by move => ?; rewrite /workload_of_jobs big_nil. Qed. (** The workload of a set of jobs can be equivalently rewritten as sum over their tasks. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall (P : pred Job) (Q : pred Task) (js : seq Job) (ts : seq Task), {in js, forall j : Job, job_task j \in ts} -> {in js, forall j : Job, P j -> Q (job_task j)} -> uniq js -> uniq ts -> let P_and_job_of := fun (tsk_o : Task) (j : Job) => P j && (job_task j == tsk_o) in workload_of_jobs P js = \sum_(tsk_o <- ts | Q tsk_o) workload_of_jobs (P_and_job_of tsk_o) js
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job

forall (P : pred Job) (Q : pred Task) (js : seq Job) (ts : seq Task), {in js, forall j : Job, job_task j \in ts} -> {in js, forall j : Job, P j -> Q (job_task j)} -> uniq js -> uniq ts -> let P_and_job_of := fun (tsk_o : Task) (j : Job) => P j && (job_task j == tsk_o) in workload_of_jobs P js = \sum_(tsk_o <- ts | Q tsk_o) workload_of_jobs (P_and_job_of tsk_o) js
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts

workload_of_jobs P js = \sum_(tsk_o <- ts | Q tsk_o) workload_of_jobs (fun j : Job => P j && (job_task j == tsk_o)) js
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts

\sum_(j <- js | P j) job_cost j = \sum_(i <- [seq x <- ts | Q x]) workload_of_jobs (fun j : Job => P j && (job_task j == i)) js
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts
j: Job
IN: j \in js
Px: P j

job_task j \in [seq x <- ts | Q x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts
j: Job
IN: j \in js
Px: P j

Q (job_task j)
by apply: PQ. Qed. (** In this section we state a lemma about splitting the workload among tasks of different priority relative to a job [j]. *) Section WorkloadPartitioningByPriority. (** Consider any JLFP policy. *) Context `{JLFP_policy Job}. (** Consider the workload of all the jobs that have priority higher-than-or-equal-to the priority of [j]. This workload can be split by task into the workload of higher-or-equal priority jobs from the task of [j] and higher-or-equal priority jobs from all tasks except for the task of [j]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job

forall (jobs : seq Job) (j : Job), workload_of_jobs (another_hep_job^~ j) jobs = workload_of_jobs (another_task_hep_job^~ j) jobs + workload_of_jobs (another_hep_job_of_same_task^~ j) jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job

forall (jobs : seq Job) (j : Job), workload_of_jobs (another_hep_job^~ j) jobs = workload_of_jobs (another_task_hep_job^~ j) jobs + workload_of_jobs (another_hep_job_of_same_task^~ j) jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j: Job

workload_of_jobs (another_hep_job^~ j) jobs = workload_of_jobs (another_task_hep_job^~ j) jobs + workload_of_jobs (another_hep_job_of_same_task^~ j) jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j: Job

\sum_(j0 <- jobs | another_hep_job j0 j) job_cost j0 = \sum_(j0 <- jobs | another_task_hep_job j0 j) job_cost j0 + \sum_(j0 <- jobs | another_hep_job_of_same_task j0 j) job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job

another_hep_job jo j = another_task_hep_job jo j || another_hep_job_of_same_task jo j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
~~ (another_task_hep_job jo j && another_hep_job_of_same_task jo j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job

another_hep_job jo j = another_task_hep_job jo j || another_hep_job_of_same_task jo j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job

hep_job jo j && (jo != j) = hep_job jo j && (job_task jo != job_task j) || hep_job jo j && (jo != j) && (job_task jo == job_task j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ2: (jo != j) = false
EQ3: (job_task jo != job_task j) = true

true && false = true && true || true && false && (job_task jo == job_task j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ3: (job_task jo != job_task j) = true
EQ2: jo = j

true && false = true && true || true && false && (job_task jo == job_task j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ2: jo = j
EQ3: (job_task j != job_task j) = true

true && false = true && true || true && false && (job_task jo == job_task j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ2: jo = j

(job_task j != job_task j) <> true
by apply /negP /negPn /eqP.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job

~~ (another_task_hep_job jo j && another_hep_job_of_same_task jo j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job

~~ [&& hep_job jo j && (job_task jo != job_task j), hep_job jo j && (jo != j) & job_task jo == job_task j]
by case (hep_job jo j) eqn: EQ1; case (jo != j) eqn: EQ2; case (job_task jo != job_task j) eqn: EQ3; try lia. Qed. End WorkloadPartitioningByPriority. (** Consider any arrival sequence with consistent arrivals. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_consistent : consistent_arrival_times arr_seq. (** In this section, we prove a few useful properties regarding the predicate of [workload_of_jobs]. *) Section PredicateProperties. (** Consider a sequence of jobs [jobs]. *) Variable jobs : seq Job. (** First, we show that workload of [jobs] for an unsatisfiable predicate is equal to [0]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job

workload_of_jobs pred0 jobs = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job

workload_of_jobs pred0 jobs = 0
by rewrite /workload_of_jobs; apply big_pred0. Qed. (** Next, consider two arbitrary predicates [P] and [P']. *) Variable P P' : pred Job. (** We show that [workload_of_jobs] conditioned on [P] can be split into two summands: (1) [workload_of_jobs] conditioned on [P /\ P'] and (2) [workload_of_jobs] conditioned on [P /\ ~~ P']. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job

workload_of_jobs P jobs = workload_of_jobs (fun j : Job => P j && P' j) jobs + workload_of_jobs (fun j : Job => P j && ~~ P' j) jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job

workload_of_jobs P jobs = workload_of_jobs (fun j : Job => P j && P' j) jobs + workload_of_jobs (fun j : Job => P j && ~~ P' j) jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job

\sum_(i <- jobs) (if P i then job_cost i else 0) = \sum_(i <- jobs) ((if P i && P' i then job_cost i else 0) + (if P i && ~~ P' i then job_cost i else 0))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
j': Job
IN: j' \in jobs

(if P j' then job_cost j' else 0) = (if P j' && P' j' then job_cost j' else 0) + (if P j' && ~~ P' j' then job_cost j' else 0)
by destruct (P _), (P' _); simpl; lia. Qed. (** We show that if [P] is indistinguishable from [P'] on set [jobs], then [workload_of_jobs] conditioned on [P] is equal to [workload_of_jobs] conditioned on [P']. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job

{in jobs, P =1 P'} -> workload_of_jobs P jobs = workload_of_jobs P' jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job

{in jobs, P =1 P'} -> workload_of_jobs P jobs = workload_of_jobs P' jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
EQUIV: {in jobs, P =1 P'}

workload_of_jobs P jobs = workload_of_jobs P' jobs
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
EQUIV: {in jobs, P =1 P'}

\sum_(i <- jobs) (if P i then job_cost i else 0) = \sum_(i <- jobs) (if P' i then job_cost i else 0)
by apply: eq_big_seq => j' IN; rewrite EQUIV. Qed. End PredicateProperties. (** In this section, we bound the workload of jobs of a particular task by the task's [RBF]. *) Section WorkloadRBF. (** Consider an arbitrary task. *) Variable tsk : Task. (** Consider a valid arrival curve that is respected by the task [tsk]. *) Context `{MaxArrivals Task}. Hypothesis H_task_repsects_max_arrivals : respects_max_arrivals arr_seq tsk (max_arrivals tsk). (** Suppose all arrivals have WCET-compliant job costs. *) Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq. (** Consider an instant [t1] and a duration [Δ]. *) Variable t1 : instant. Variable Δ : duration. (** We prove that the workload of jobs of a task [tsk] in any interval is bound by the request bound function of the task in that interval. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

\sum_(j <- arrivals_between arr_seq t1 (t1 + Δ) | job_task j == tsk) job_cost j <= task_cost tsk * size [seq j <- arrivals_between arr_seq t1 (t1 + Δ) | job_task j == tsk]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration
j: Job
IN: j \in arrivals_between arr_seq t1 (t1 + Δ)
TSK: job_task j == tsk

job_cost j <= task_cost tsk
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration
j: Job
IN: j \in arrivals_between arr_seq t1 (t1 + Δ)
TSK: job_task j == tsk

valid_job_cost j
exact/H_valid_job_cost/in_arrivals_implies_arrived.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= max_arrivals tsk (t1 + Δ - t1)
by apply H_task_repsects_max_arrivals; lia. } Qed. (** For convenience, we combine the preceding bound with [workload_of_jobs_weaken], as the two are often used together. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

forall P : Job -> bool, workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration

forall P : Job -> bool, workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration
P: Job -> bool

workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_request_bound_function tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
t1: instant
Δ: duration
P: Job -> bool
LEQ: forall ar : seq Job, workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) ar <= workload_of_jobs (job_of_task tsk) ar

workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) (arrivals_between arr_seq t1 (t1 + Δ)) <= task_request_bound_function tsk Δ
by apply/(leq_trans (LEQ _))/workload_le_rbf. Qed. End WorkloadRBF. (** In this section, we prove one equality about the workload of a job. *) Section WorkloadOfJob. (** Assume there are no duplicates in the arrival sequence. *) Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq. (** We prove that the workload of a job in an interval <<[t1, t2)>> is equal to the cost of the job if the job's arrival is in the interval and [0] otherwise. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq

forall (j : Job) (t1 t2 : instant), arrives_in arr_seq j -> workload_of_job arr_seq j t1 t2 = (if t1 <= job_arrival j < t2 then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq

forall (j : Job) (t1 t2 : instant), arrives_in arr_seq j -> workload_of_job arr_seq j t1 t2 = (if t1 <= job_arrival j < t2 then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

workload_of_job arr_seq j t1 t2 = job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false
workload_of_job arr_seq j t1 t2 = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

workload_of_job arr_seq j t1 t2 = job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

\sum_(j0 <- arrivals_between arr_seq t1 t2 | j0 == j) job_cost j0 = job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

j \in arrivals_between arr_seq t1 t2
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
uniq (arrivals_between arr_seq t1 t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
eq_op^~ j =1 pred1 j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

j \in arrivals_between arr_seq t1 t2
by apply arrived_between_implies_in_arrivals => //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

uniq (arrivals_between arr_seq t1 t2)
by done.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true

eq_op^~ j =1 pred1 j
by move => j'; rewrite /pred1 //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false

workload_of_job arr_seq j t1 t2 = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false

workload_of_job arr_seq j t1 t2 = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false
IN: j \in arrivals_between arr_seq t1 t2

False
by apply job_arrival_between in IN => //. } Qed. End WorkloadOfJob. (** In the following section, we relate three types of workload: workload of a job [j], workload of higher-or-equal priority jobs distinct from [j], and workload of higher-or-equal priority jobs. *) Section HEPWorkload. (** Consider a JLFP policy that indicates a higher-or-equal priority relation and assume that the relation is reflexive. *) Context {JLFP : JLFP_policy Job}. Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP. (** We prove that the sum of the workload of a job [j] and the workload of higher-or-equal priority jobs distinct from [j] is equal to the workload of higher-or-equal priority jobs. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP

forall (j : Job) (t1 t2 : instant), workload_of_job arr_seq j t1 t2 + workload_of_other_hep_jobs arr_seq j t1 t2 = workload_of_hep_jobs arr_seq j t1 t2
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP

forall (j : Job) (t1 t2 : instant), workload_of_job arr_seq j t1 t2 + workload_of_other_hep_jobs arr_seq j t1 t2 = workload_of_hep_jobs arr_seq j t1 t2
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant

workload_of_job arr_seq j t1 t2 + workload_of_other_hep_jobs arr_seq j t1 t2 = workload_of_hep_jobs arr_seq j t1 t2
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant

workload_of_jobs (eq_op^~ j) (arrivals_between arr_seq t1 t2) + workload_of_jobs (another_hep_job^~ j) (arrivals_between arr_seq t1 t2) = workload_of_jobs (hep_job^~ j) (arrivals_between arr_seq t1 t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant

workload_of_jobs (eq_op^~ j) (arrivals_between arr_seq t1 t2) + workload_of_jobs (another_hep_job^~ j) (arrivals_between arr_seq t1 t2) = workload_of_jobs (fun j0 : Job => hep_job j0 j && (j0 != j)) (arrivals_between arr_seq t1 t2) + workload_of_jobs (fun j0 : Job => hep_job j0 j && ~~ (j0 != j)) (arrivals_between arr_seq t1 t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
EQ: forall a b c d : nat, a = b -> c = d -> a + c = b + d

workload_of_jobs (eq_op^~ j) (arrivals_between arr_seq t1 t2) + workload_of_jobs (another_hep_job^~ j) (arrivals_between arr_seq t1 t2) = workload_of_jobs (fun j0 : Job => hep_job j0 j && (j0 != j)) (arrivals_between arr_seq t1 t2) + workload_of_jobs (fun j0 : Job => hep_job j0 j && ~~ (j0 != j)) (arrivals_between arr_seq t1 t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
EQ: forall a b c d : nat, a = b -> c = d -> a + c = b + d

workload_of_jobs (eq_op^~ j) (arrivals_between arr_seq t1 t2) = workload_of_jobs (fun j0 : Job => hep_job j0 j && ~~ (j0 != j)) (arrivals_between arr_seq t1 t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2

(jo == j) = hep_job jo j && ~~ (jo != j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
EQ: j = jo

true = hep_job jo j && ~~ ~~ true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
NEQ: j != jo
false = hep_job jo j && ~~ ~~ false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
EQ: j = jo

true = hep_job jo j && ~~ ~~ true
by subst; rewrite andbT; symmetry; apply H_priority_is_reflexive.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
NEQ: j != jo

false = hep_job jo j && ~~ ~~ false
by rewrite andbF. Qed. End HEPWorkload. (** If at some point in time [t] the predicate [P] by which we select jobs from the set of arrivals in an interval <<[t1, t2)>> becomes certainly false, then we may disregard all jobs arriving at time [t] or later. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq

forall (P : Job -> bool) (t1 : instant) (t2 t : nat), t <= t2 -> (forall j : Job, j \in arrivals_between arr_seq t1 t2 -> t <= job_arrival j -> ~~ P j) -> workload_of_jobs P (arrivals_between arr_seq t1 t2) = workload_of_jobs P (arrivals_between arr_seq t1 t)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq

forall (P : Job -> bool) (t1 : instant) (t2 t : nat), t <= t2 -> (forall j : Job, j \in arrivals_between arr_seq t1 t2 -> t <= job_arrival j -> ~~ P j) -> workload_of_jobs P (arrivals_between arr_seq t1 t2) = workload_of_jobs P (arrivals_between arr_seq t1 t)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job, j \in arrivals_between arr_seq t1 t2 -> t <= job_arrival j -> ~~ P j

workload_of_jobs P (arrivals_between arr_seq t1 t2) = workload_of_jobs P (arrivals_between arr_seq t1 t)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job, j \in arrivals_between arr_seq t1 t2 -> t <= job_arrival j -> ~~ P j

workload_of_jobs P (arrivals_between arr_seq t1 t2) = workload_of_jobs P [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job, j \in arrivals_between arr_seq t1 t2 -> t <= job_arrival j -> ~~ P j
j: Job
IN: j \in arrivals_between arr_seq t1 t2
Pj: P j

job_arrival j < t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job, j \in arrivals_between arr_seq t1 t2 -> t <= job_arrival j -> ~~ P j
j: Job
IN: j \in arrivals_between arr_seq t1 t2
Pj: P j
TAIL: t <= job_arrival j

false
by move: (IMPL j IN TAIL) => /negP. Qed. (** For simplicity, let's define a local name. *) Let arrivals_between := arrivals_between arr_seq. (** We observe that the cumulative workload of all jobs arriving in a time interval <<[t1, t2)>> and respecting a predicate [P] can be split into two parts. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job

forall (t t1 t2 : nat) (P : pred Job), t1 <= t <= t2 -> workload_of_jobs P (arrivals_between t1 t2) = workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job

forall (t t1 t2 : nat) (P : pred Job), t1 <= t <= t2 -> workload_of_jobs P (arrivals_between t1 t2) = workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
t, t1, t2: nat
P: pred Job
GE: t1 <= t
LE: t <= t2

workload_of_jobs P (arrivals_between t1 t2) = workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
t, t1, t2: nat
P: pred Job
GE: t1 <= t
LE: t <= t2

\sum_(j <- arrival_sequence.arrivals_between arr_seq t1 t2 | P j) job_cost j = \sum_(j <- arrival_sequence.arrivals_between arr_seq t1 t | P j) job_cost j + \sum_(j <- arrival_sequence.arrivals_between arr_seq t t2 | P j) job_cost j
by rewrite (arrivals_between_cat _ _ t) // big_cat. Qed. (** As a corollary, we prove that the workload in any range <<[t1,t3)>> always bounds the workload in any sub-range <<[t1,t2)>>. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job

forall (t1 t2 t3 : nat) (P : pred Job), t1 <= t2 -> t2 <= t3 -> workload_of_jobs P (arrivals_between t1 t2) <= workload_of_jobs P (arrivals_between t1 t3)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job

forall (t1 t2 t3 : nat) (P : pred Job), t1 <= t2 -> t2 <= t3 -> workload_of_jobs P (arrivals_between t1 t2) <= workload_of_jobs P (arrivals_between t1 t3)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
t1, t2, t3: nat
P: pred Job
_Hyp_: t1 <= t2
_Hyp1_: t2 <= t3

workload_of_jobs P (arrivals_between t1 t2) <= workload_of_jobs P (arrivals_between t1 t3)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
t1, t2, t3: nat
P: pred Job
_Hyp_: t1 <= t2
_Hyp1_: t2 <= t3

workload_of_jobs P (arrivals_between t1 t2) <= workload_of_jobs P (arrivals_between t1 t2) + workload_of_jobs P (arrivals_between t2 t3)
by apply leq_addr. Qed. (** Consider a job [j] ... *) Variable j : Job. (** ... and a duplicate-free sequence of jobs [jobs]. *) Variable jobs : seq Job. Hypothesis H_jobs_uniq : uniq jobs. (** Further, assume that [j] is contained in [jobs]. *) Hypothesis H_j_in_jobs : j \in jobs. (** To help with rewriting, we prove that the workload of [jobs] minus the job cost of [j] is equal to the workload of all jobs except [j]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs

forall P : Job -> bool, workload_of_jobs (fun jhp : Job => P jhp && (jhp != j)) jobs = workload_of_jobs P jobs - (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs

forall P : Job -> bool, workload_of_jobs (fun jhp : Job => P jhp && (jhp != j)) jobs = workload_of_jobs P jobs - (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

workload_of_jobs (fun jhp : Job => P jhp && (jhp != j)) jobs = workload_of_jobs P jobs - (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

\sum_(j0 <- jobs | P j0 && (j0 != j)) job_cost j0 = \sum_(j <- jobs | P j) job_cost j - (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

\sum_(j0 <- jobs | P j0 && (j0 != j)) job_cost j0 = \sum_(i <- jobs | P i && (i != j)) job_cost i + \sum_(i <- jobs | P i && ~~ (i != j)) job_cost i - (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

\sum_(j0 <- jobs | P j0 && ~~ (j0 != j)) job_cost j0 = (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

(if P j && ~~ (j != j) then job_cost j else 0) + \sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j)) job_cost y = (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

(if P j then job_cost j else 0) + \sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j)) job_cost y = (if P j then job_cost j else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

\sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j)) job_cost y = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool

\sum_(i <- rem (T:=Job) j jobs | [&& i \in rem (T:=Job) j jobs, P i & ~~ (i != j)]) job_cost i = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job

[&& jo \in rem (T:=Job) j jobs, P jo & ~~ (jo != j)] = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job

(jo == j) && (jo \in rem (T:=Job) j jobs) && P jo = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job

(jo == j) && (jo \in rem (T:=Job) j jobs) = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job
JJ: (jo == j) = true

(jo \in rem (T:=Job) j jobs) = false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job

(j \in rem (T:=Job) j jobs) = false
by apply mem_rem_uniqF => //=. Qed. (** Next, we specialize the above lemma to the trivial predicate [predT]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs

workload_of_jobs (fun jhp : Job => jhp != j) jobs = workload_of_jobs predT jobs - job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs

workload_of_jobs (fun jhp : Job => jhp != j) jobs = workload_of_jobs predT jobs - job_cost j
by rewrite (workload_minus_job_cost' predT) //=. Qed. (** In this section, we prove the relation between two different ways of constraining [workload_of_jobs] to only those jobs that arrive prior to a given time. *) Section Subset. (** Assume that arrival times are consistent and that arrivals are unique. *) Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** Consider a time interval <<[t1, t2)>> and a time instant [t]. *) Variable t1 t2 t : instant. Hypothesis H_t1_le_t2 : t1 <= t2. (** Let [P] be an arbitrary predicate on jobs. *) Variable P : pred Job. (** Consider the window <<[t1,t2)>>. We prove that the total workload of the jobs arriving in this window before some [t] is the same as the workload of the jobs arriving in <<[t1,t)>>. Note that we only require [t1] to be less-or-equal than [t2]. Consequently, the interval <<[t1,t)>> may be empty. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
H_t1_le_t2: t1 <= t2
P: pred Job

workload_of_jobs (fun j : Job => (job_arrival j <= t) && P j) (arrivals_between t1 t2) <= workload_of_jobs [eta P] (arrivals_between t1 (t + 1))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
H_t1_le_t2: t1 <= t2
P: pred Job

workload_of_jobs (fun j : Job => (job_arrival j <= t) && P j) (arrivals_between t1 t2) <= workload_of_jobs [eta P] (arrivals_between t1 (t + 1))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job

workload_of_jobs (fun j : Job => (job_arrival j <= t) && P j) (arrivals_between t1 t2) <= workload_of_jobs [eta P] (arrivals_between t1 (t + 1))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job

\sum_(i <- arrivals_between t1 t2 | [&& i \in arrivals_between t1 t2, job_arrival i <= t & P i]) job_cost i <= \sum_(j <- arrivals_between t1 (t + 1) | P j) job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job

\sum_(i <- [seq i <- arrivals_between t1 t2 | i \in arrivals_between t1 t2 & (job_arrival i <= t) && P i]) job_cost i <= \sum_(i <- [seq x <- arrivals_between t1 (t + 1) | P x]) job_cost i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job

{subset [seq i <- arrivals_between t1 t2 | i \in arrivals_between t1 t2 & (job_arrival i <= t) && P i] <= [seq x <- arrivals_between t1 (t + 1) | P x]}
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'

j' \in [seq x <- arrivals_between t1 (t + 1) | P x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j' /\ t1 <= job_arrival j' < t2

j' \in [seq x <- arrivals_between t1 (t + 1) | P x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j'
A1: t1 <= job_arrival j'
A2: job_arrival j' < t2

j' \in [seq x <- arrivals_between t1 (t + 1) | P x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j'
A1: t1 <= job_arrival j'
A2: job_arrival j' < t2

j' \in arrivals_between t1 (t + 1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j'
A1: t1 <= job_arrival j'
A2: job_arrival j' < t2

job_arrival j' < t + 1
by lia. Qed. End Subset. End WorkloadFacts.