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.implementation.definitions.maximal_arrival_sequence. (** Recall that, given an arrival curve [max_arrivals] and a job-generating function [generate_jobs_at], the function [concrete_arrival_sequence] generates an arrival sequence. In this section, we prove a few properties of this function. *) Section MaximalArrivalSequence. (** 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}. (** Consider a task set [ts] with non-duplicate tasks. *) Variable ts : seq Task. Hypothesis H_ts_uniq : uniq ts. (** Let [max_arrivals] be a family of valid arrival curves, i.e., for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function that equals [0] for the empty interval [delta = 0]. *) Context `{MaxArrivals Task}. Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals. (** Further assume we are given a function that generates the required number of jobs of a given task at a given instant of time. *) Variable generate_jobs_at : Task -> nat -> instant -> seq Job. (** First, we assume that [generate_jobs_at tsk n t] generates [n] jobs. *) Hypothesis H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n. (** Second, we assume that [generate_jobs_at tsk n t] generates jobs of task [tsk] that arrive at time [t]. *) Hypothesis H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), (j \in generate_jobs_at tsk n t) -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk. (** Finally, we assume that all jobs generated by [generate_jobs_at] are unique. *) Hypothesis H_jobs_unique: forall (t1 t2 : instant), uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2). (** Assuming such a well-behaved "constructor" [generate_jobs_at], we prove a few validity claims about an arrival sequence generated by [concrete_arrival_sequence]. *) Section ValidityClaims. (** We start by showing that the obtained arrival sequence is a set. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
t: instant

uniq (arrivals_at (concrete_arrival_sequence generate_jobs_at ts) t)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
t: instant

uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t t.+1) -> uniq (arrivals_at (concrete_arrival_sequence generate_jobs_at ts) t)
by rewrite /arrivals_between big_nat1. Qed. (** Next, we show that all jobs in the arrival sequence come from [ts]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
j: Job
t: instant
tsk: Task
TSK_IN: tsk \in ts
IN: j \in generate_jobs_at tsk (max_arrivals_at tsk t) t

job_task j \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
j: Job
t: instant
tsk: Task
TSK_IN: tsk \in ts
IN: j \in generate_jobs_at tsk (max_arrivals_at tsk t) t
JOB_TASK: job_task j = tsk

job_task j \in ts
by rewrite JOB_TASK. Qed. (** Further, we note that the jobs in the arrival sequence have consistent arrival times. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
j: Job
t: instant
tsk: Task
TSK_IN: tsk \in ts
IN: j \in generate_jobs_at tsk (max_arrivals_at tsk t) t

job_arrival j = t
by move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [_ [JOB_ARR _]]. Qed. (** Lastly, we observe that the jobs in the arrival sequence have valid job costs. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
j: Job
t: instant
tsk: Task
TSK_IN: tsk \in ts
IN: j \in generate_jobs_at tsk (max_arrivals_at tsk t) t

valid_job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
j: Job
t: instant
tsk: Task
TSK_IN: tsk \in ts
IN: j \in generate_jobs_at tsk (max_arrivals_at tsk t) t
JOB_TASK: job_task j = tsk
JOB_COST: job_cost j <= task_cost tsk

valid_job_cost j
by rewrite /valid_job_cost JOB_TASK. Qed. End ValidityClaims. (** In this section, we prove a series of facts regarding the maximal arrival sequence, leading up to the main theorem that all arrival-curve constraints are respected. *) Section Facts. (** Let [tsk] be any task in [ts] that is to be analyzed. *) Variable tsk : Task. Hypothesis H_tsk_in_ts : tsk \in ts. (** First, we show that the arrivals at time [t] are indeed generated by [generate_jobs_at] applied at time [t]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : instant, task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t = generate_jobs_at tsk (max_arrivals_at tsk t) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : instant, task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t = generate_jobs_at tsk (max_arrivals_at tsk t) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t: instant

task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t = generate_jobs_at tsk (max_arrivals_at tsk t) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t: instant
tsk0: Task
j: Job
INj: j \in generate_jobs_at tsk0 (max_arrivals_at tsk0 t) t

job_task j = tsk0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t: instant
tsk0: Task
j: Job
INj: job_task j = tsk0 /\ job_arrival j = t /\ job_cost j <= task_cost tsk0

job_task j = tsk0
by destruct INj. Qed. (** Next, we show that the number of arrivals at time [t] always matches [max_arrivals_at] applied at time [t]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : instant, size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t) = max_arrivals_at tsk t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : instant, size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t) = max_arrivals_at tsk t
by move=> t; rewrite task_arrivals_at_eq_generate_jobs_at. Qed. (** We then generalize the previous result to an arbitrary interval <<[t1,t2)>>. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t1 t2 : instant, number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2 = \sum_(t1 <= t < t2) max_arrivals_at tsk t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t1 t2 : instant, number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2 = \sum_(t1 <= t < t2) max_arrivals_at tsk t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t1, t2: instant

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2 = \sum_(t1 <= t < t2) max_arrivals_at tsk t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t1, t2: instant

\sum_(t1 <= t < t2) size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t) = \sum_(t1 <= t < t2) max_arrivals_at tsk t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t1, t2: instant
t: nat
RANGE: t1 <= t < t2

size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t) = max_arrivals_at tsk t
by apply task_arrivals_at_eq. Qed. (** We further show that, starting from an empty prefix and applying [extend_arrival_prefix] [t] times, we end up with a prefix of size [t]... *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : nat, size (iter t (extend_arrival_prefix tsk) [::]) = t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : nat, size (iter t (extend_arrival_prefix tsk) [::]) = t
by elim=> // t IHt; rewrite size_cat IHt //=; lia. Qed. (** ...and that the arrival sequence prefix up to an arbitrary horizon [t] is a sequence of [t+1] elements. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : nat, size (maximal_arrival_prefix tsk t) = t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : nat, size (maximal_arrival_prefix tsk t) = t.+1
by elim=> // t IHt; rewrite /maximal_arrival_prefix /extend_arrival_prefix size_cat IHt //=; lia. Qed. (** Next, we prove prefix inclusion for [maximal_arrival_prefix] when the horizon is expanded by one... *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t h : nat, t <= h -> nth 0 (maximal_arrival_prefix tsk h) t = nth 0 (maximal_arrival_prefix tsk h.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t h : nat, t <= h -> nth 0 (maximal_arrival_prefix tsk h) t = nth 0 (maximal_arrival_prefix tsk h.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h: nat
LEQ: t <= h

nth 0 (maximal_arrival_prefix tsk h) t = nth 0 (maximal_arrival_prefix tsk h.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h: nat
LEQ: t <= h

nth 0 (extend_arrival_prefix tsk (iter h (extend_arrival_prefix tsk) [::])) t = (if t < h.+1 then nth 0 (extend_arrival_prefix tsk (iter h (extend_arrival_prefix tsk) [::])) t else nth 0 [:: next_max_arrival tsk (extend_arrival_prefix tsk (iter h (extend_arrival_prefix tsk) [::]))] (t - h.+1))
by case: (ltnP t h.+1); lia. Qed. (** ...and we generalize the previous result to two arbitrary horizons [h1 <= h2]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t h1 h2 : nat, t <= h1 <= h2 -> nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t h1 h2 : nat, t <= h1 <= h2 -> nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h1, h2: nat
LEQh1: t <= h1
LEQh2: h1 <= h2

nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h1: nat
LEQh1: t <= h1
h2: nat
IHh2: h1 <= h2 -> nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
LEQh2: h1 <= h2.+1

nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h1: nat
LEQh1: t <= h1
h2: nat
IHh2: h1 <= h2 -> nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
LEQh2: (h1 == h2.+1) || (h1 < h2.+1)

nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h1: nat
LEQh1: t <= h1
h2: nat
IHh2: h1 <= h2 -> nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
LT: h1 < h2.+1

nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h1: nat
LEQh1: t <= h1
h2: nat
IHh2: nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
LT: h1 < h2.+1

nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2.+1) t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, h1: nat
LEQh1: t <= h1
h2: nat
IHh2: nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t
LT: h1 < h2.+1

t <= h2
by lia. Qed. (** Next, we prove that, for any positive time instant [t], [max_arrivals_at] indeed matches the arrivals of [next_max_arrival] applied at [t-1]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : nat, 0 < t -> max_arrivals_at tsk t = next_max_arrival tsk (maximal_arrival_prefix tsk t.-1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t : nat, 0 < t -> max_arrivals_at tsk t = next_max_arrival tsk (maximal_arrival_prefix tsk t.-1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t: nat
GT0: 0 < t

max_arrivals_at tsk t = next_max_arrival tsk (maximal_arrival_prefix tsk t.-1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t: nat
GT0: 0 < t
PUS: forall t : nat, size (iter t.+1 (extend_arrival_prefix tsk) [::]) = t.+1

max_arrivals_at tsk t = next_max_arrival tsk (iter t.-1.+1 (extend_arrival_prefix tsk) [::])
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t: nat
GT0: 0 < t
PUS: forall t : nat, size (iter t.+1 (extend_arrival_prefix tsk) [::]) = t.+1

next_max_arrival tsk ((fix loop (m : nat) : seq nat := match m with | 0 => [::] | i.+1 => loop i ++ [:: next_max_arrival tsk (loop i)] end) t) = next_max_arrival tsk (extend_arrival_prefix tsk (iter t.-1 (extend_arrival_prefix tsk) [::]))
by destruct t. Qed. (** Given a time instant [t] and and interval [Δ], we show that [max_arrivals_at] applied at time [t] is always less-or-equal to [max_arrivals] applied to [Δ+1], even when each value of [max_arrivals_at] in the interval <<[t-Δ, t)>> is subtracted from it. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t Δ : nat, Δ <= t -> max_arrivals_at tsk t <= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts

forall t Δ : nat, Δ <= t -> max_arrivals_at tsk t <= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t

max_arrivals_at tsk t <= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals_at tsk t <= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
Δ: nat
LEQ: Δ <= 0
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals_at tsk 0 <= max_arrivals tsk Δ.+1 - \sum_(0 - Δ <= i < 0) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
max_arrivals_at tsk t.+1 <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
Δ: nat
LEQ: Δ <= 0
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals_at tsk 0 <= max_arrivals tsk Δ.+1 - \sum_(0 - Δ <= i < 0) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
Δ: nat
LEQ: Δ <= 0
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals_at tsk 0 <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
Δ: nat
LEQ: Δ <= 0
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals tsk 1 <= max_arrivals tsk Δ.+1
by apply MONO.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals_at tsk t.+1 <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals_at tsk t.+1 <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

next_max_arrival tsk (maximal_arrival_prefix tsk t.+1.-1) <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

match supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t.+1.-1) Δ | Δ <- iota 0 t.+1.-1.+2] with | Some n => n | None => max_arrivals tsk 1 end <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

match supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] with | Some n => n | None => max_arrivals tsk 1 end <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s

s <= max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s

max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) max_arrivals_at tsk i \in [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s

max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i \in [seq max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= t0 < t.+1) nth 0 (maximal_arrival_prefix tsk t) t0 | Δ <- iota 0 t.+2]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s

\sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i = \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s
max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i \in [seq max_arrivals tsk Δ.+1 - \sum_( t.+1 - Δ <= t0 < t.+1) nth 0 (maximal_arrival_prefix tsk t) t0 | Δ <- iota 0 t.+2]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s

\sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i = \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s
i: nat
RANGE: t.+1 - Δ <= i < t.+1

nth 0 (maximal_arrival_prefix tsk i) i = nth 0 (maximal_arrival_prefix tsk t) i
by apply n_arrivals_at_prefix_inclusion; lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s

max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i \in [seq max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= t0 < t.+1) nth 0 (maximal_arrival_prefix tsk t) t0 | Δ <- iota 0 t.+2]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s
f:= fun x : nat => max_arrivals tsk x.+1 - \sum_(t.+1 - x <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i: nat -> nat

max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i \in [seq f i | i <- iota 0 t.+2]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s
f:= fun x : nat => max_arrivals tsk x.+1 - \sum_(t.+1 - x <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i: nat -> nat

f Δ \in [seq f i | i <- iota 0 t.+2]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
H_tsk_in_ts: tsk \in ts
t, Δ: nat
LEQ: Δ <= t.+1
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)
s: Datatypes_nat__canonical__eqtype_Equality
SUP: supremum leq [seq max_arrivals tsk Δ.+1 - suffix_sum (maximal_arrival_prefix tsk t) Δ | Δ <- iota 0 t.+2] = Some s
f:= fun x : nat => max_arrivals tsk x.+1 - \sum_(t.+1 - x <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i: nat -> nat

Δ \in iota 0 t.+2
by rewrite mem_iota; lia. } Qed. End Facts. (** Finally, we prove our main result, that is, the proposed maximal arrival sequence instantiation indeed respects all arrival-curve constraints. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)

taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1, t: instant
LEQ: t1 <= t

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t <= max_arrivals tsk (t - t1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1, t: instant
LEQ: t1 <= t
Δ:= t - t1: nat

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1, t: instant
LEQ: t1 <= t
Δ:= t - t1: nat

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1, t: instant
LEQ: t1 <= t
Δ:= t - t1: nat
LEQd: Δ <= t

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1, t: instant

forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
Δ: nat
LEQ: Δ <= 0

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (0 - Δ) 0 <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t: nat
IHt: forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Δ: nat
LEQ: Δ <= t.+1
number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t.+1 - Δ) t.+1 <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
Δ: nat
LEQ: Δ <= 0

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (0 - Δ) 0 <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
Δ: nat
LEQ: Δ <= 0

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk 0 0 <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
Δ: nat
LEQ: Δ <= 0

\sum_(0 <= t < 0) max_arrivals_at tsk t <= max_arrivals tsk Δ
by vm_compute; rewrite unlock.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t: nat
IHt: forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Δ: nat
LEQ: Δ <= t.+1

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t.+1 - Δ) t.+1 <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t: nat
IHt: forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Δ: nat
LEQ: Δ <= t.+1

number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t.+1 - Δ) t.+1 <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t: nat
IHt: forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Δ: nat
LEQ: Δ <= t.+1

\sum_(t.+1 - Δ <= t < t.+1) max_arrivals_at tsk t <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t: nat
IHt: forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Δ: nat
LEQ: Δ < t.+1

\sum_(t.+1 - Δ.+1 <= t < t.+1) max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t: nat
IHt: forall Δ : nat, Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
Δ: nat
LEQ: Δ < t.+1

\sum_(t - Δ <= t < t.+1) max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
IHt: Δ <= t -> number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
LEQ: Δ < t.+1

\sum_(t - Δ <= t < t.+1) max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
IHt: number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk (t - Δ) t <= max_arrivals tsk Δ
LEQ: Δ < t.+1

\sum_(t - Δ <= t < t.+1) max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
LEQ: Δ < t.+1
IHt: \sum_(t - Δ <= t < t) max_arrivals_at tsk t <= max_arrivals tsk Δ

\sum_(t - Δ <= t < t.+1) max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
LEQ: Δ < t.+1
IHt: \sum_(t - Δ <= t < t) max_arrivals_at tsk t <= max_arrivals tsk Δ

\sum_(t - Δ <= i < t) max_arrivals_at tsk i + max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
LEQ: Δ < t.+1
IHt: \sum_(t - Δ <= t < t) max_arrivals_at tsk t <= max_arrivals tsk Δ

\sum_(t - Δ <= i < t) max_arrivals_at tsk i <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
LEQ: Δ < t.+1
IHt: \sum_(t - Δ <= t < t) max_arrivals_at tsk t <= max_arrivals tsk Δ
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

\sum_(t - Δ <= i < t) max_arrivals_at tsk i <= max_arrivals tsk Δ.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
ts: seq Task
H_ts_uniq: uniq ts
H3: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
generate_jobs_at: Task -> nat -> instant -> seq Job
H_job_generation_valid_number: forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
H_job_generation_valid_jobs: forall (tsk : Task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
H_jobs_unique: forall t1 t2 : instant, uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2)
tsk: Task
IN: tsk \in ts
t1: instant
t, Δ: nat
LEQ: Δ < t.+1
IHt: \sum_(t - Δ <= t < t) max_arrivals_at tsk t <= max_arrivals tsk Δ
ZERO: max_arrivals tsk 0 = 0
MONO: monotone leq (max_arrivals tsk)

max_arrivals tsk Δ <= max_arrivals tsk Δ.+1
by apply MONO. } Qed. End MaximalArrivalSequence.