Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file 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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.model.task.suspension.dynamic. Require Export prosa.analysis.facts.model.arrival_curves. (** In this file, we prove some facts related to the dynamic self-suspension model. *) Section TotalSuspensionBounded. (** Consider any type of tasks each characterized by a WCET [task_cost], an arrival curve [max_arrivals], and a bound on the maximum total self-suspension duration exhibited by any job of the task [task_total_suspension]. *) Context {Task : TaskType}. Context `{TaskCost Task}. Context `{MaxArrivals Task}. Context `{TaskTotalSuspension Task}. (** Consider any kind of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Here we consider that the jobs can exhibit self-suspensions. *) Context `{JobSuspension Job}. (** Assume that all jobs respect the bound on the maximum total self-suspension duration. *) Hypothesis H_valid_dynamic_suspensions : valid_dynamic_suspensions. (** Consider any valid arrival sequence of jobs ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** ... and assume the notion of readiness for self-suspending jobs. *) #[local] Existing Instance suspension_ready_instance. (** Consider any kind of processor model. *) Context `{PState : ProcessorState Job}. (** Consider any valid schedule. *) Variable sched : schedule PState. Hypothesis H_valid_schedule : valid_schedule sched arr_seq. (** Let [tsk] be any task. *) Variable tsk : Task. (** Consider any arbitrary time interval <<[t1, t1 + Δ)>>. *) Variable t1 : instant. Variable Δ : duration. (** We first prove a bound on the total self-suspension duration of a job. *) Section JobSuspensionBounded. (** Consider any job [j] of [tsk]. *) Variable j : Job. Hypothesis H_job_tsk : job_of_task tsk j. (** Now we prove an upper bound on the total duration a job remains suspended in the interval <<[t1, t1 + Δ)>>. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= task_total_suspension (job_task j)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= total_suspension j
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= \sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(t1 <= t < t1 + Δ) suspended sched j t <= \sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
t: Datatypes_nat__canonical__eqtype_Equality
INt: t \in index_iota t1 (t1 + Δ)

service sched j t \in index_iota 0 (service sched j (t1 + Δ) + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
t: Datatypes_nat__canonical__eqtype_Equality
INt: t1 <= t < t1 + Δ

service sched j t \in index_iota 0 (service sched j (t1 + Δ) + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
t: Datatypes_nat__canonical__eqtype_Equality
INt: t1 <= t < t1 + Δ

service sched j t < service sched j (t1 + Δ) + 1
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
t: Datatypes_nat__canonical__eqtype_Equality
INt: t1 <= t < t1 + Δ

service sched j t < service sched j t + service_during sched j t (t1 + Δ) + 1
by lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)
\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(0 <= i < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t + \sum_(job_cost j <= i < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(job_cost j <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t = 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
\sum_(0 <= i < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t + 0 <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(job_cost j <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t = 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

all (fun x : Datatypes_nat__canonical__eqtype_Equality => \sum_(t1 <= t < t1 + Δ | service sched j t == x) suspended sched j t == 0) [seq _ <- index_iota (job_cost j) (service sched j (t1 + Δ) + 1) | true]
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: r \in [seq _ <- index_iota (job_cost j) (service sched j (t1 + Δ) + 1) | true]

\sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t == 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: job_cost j <= r < service sched j (t1 + Δ) + 1

\sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t == 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: job_cost j <= r < service sched j (t1 + Δ) + 1
to: Datatypes_nat__canonical__eqtype_Equality
INto: to \in [seq x <- index_iota t1 (t1 + Δ) | service sched j x == r]

suspended sched j to == 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: job_cost j <= r < service sched j (t1 + Δ) + 1
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to = r
INto: to \in index_iota t1 (t1 + Δ)

suspended sched j to == 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: job_cost j <= r < service sched j (t1 + Δ) + 1
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to = r
INto: to \in index_iota t1 (t1 + Δ)

~~ suspension_has_passed sched j to && pending sched j to == 0
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: job_cost j <= r < service sched j (t1 + Δ) + 1
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to = r
INto: to \in index_iota t1 (t1 + Δ)

~~ pending sched j to
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: Datatypes_nat__canonical__eqtype_Equality
INr: job_cost j <= r < service sched j (t1 + Δ) + 1
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to = r
INto: to \in index_iota t1 (t1 + Δ)

completed_by sched j to
rewrite /completed_by; by lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(0 <= i < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t + 0 <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1

\sum_(0 <= i < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
GEQ: job_cost j <= service sched j (t1 + Δ) + 1
r: nat

\sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= job_suspension j r
by apply : suspension_bounded_in_interval.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= r < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)
\sum_(0 <= r < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= r < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: service sched j (t1 + Δ) + 1 < job_cost j

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= r < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: service sched j (t1 + Δ) + 1 < job_cost j

\sum_(0 <= r < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= i < service sched j (t1 + Δ) + 1) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t + \sum_(service sched j (t1 + Δ) + 1 <= i < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == i) suspended sched j t
by lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)

\sum_(0 <= r < job_cost j) \sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= \sum_(0 <= ρ < job_cost j) job_suspension j ρ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
j: Job
H_job_tsk: job_of_task tsk j
LT: ~~ (job_cost j <= service sched j (t1 + Δ) + 1)
r: nat

\sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t <= job_suspension j r
by apply: suspension_bounded_in_interval. } Qed. End JobSuspensionBounded. (* Next, assume that [tsk] respects the arrival curve defined by [max_arrivals]. *) Hypothesis H_tsk_respects_max_arrivals : respects_max_arrivals arr_seq tsk (max_arrivals tsk). (** Now we establish a bound on the total duration the jobs of task [tsk] remain suspended in the interval <<[t1, t2)>>. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

\sum_(t1 <= t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t <= max_arrivals tsk Δ * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

\sum_(t1 <= t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t <= max_arrivals tsk Δ * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) * task_total_suspension tsk <= max_arrivals tsk Δ * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
\sum_(t1 <= t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t <= number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) * task_total_suspension tsk <= max_arrivals tsk Δ * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <= max_arrivals tsk (t1 + Δ - t1)
apply: H_tsk_respects_max_arrivals; by lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

\sum_(t1 <= t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t <= number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

\sum_(t1 <= t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t <= \sum_(i <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) 1 * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

\sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) \sum_(t1 <= i < t1 + Δ) suspended sched j i <= \sum_(i <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) 1 * task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
jo: Job
INjo: jo \in task_arrivals_between arr_seq tsk t1 (t1 + Δ)

\sum_(t1 <= i < t1 + Δ) suspended sched jo i <= task_total_suspension tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
H1: TaskTotalSuspension Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobSuspension Job
H_valid_dynamic_suspensions: valid_dynamic_suspensions
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
tsk: Task
t1: instant
Δ: duration
H_tsk_respects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
jo: Job
INjo: jo \in task_arrivals_between arr_seq tsk t1 (t1 + Δ)

job_of_task tsk jo
by move: INjo; rewrite mem_filter => /andP[? ?]. Qed. End TotalSuspensionBounded.