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]
(** In this file, we establish some basic facts related to self-suspensions. *) Section Suspensions. (** Consider any kind of jobs. *) Context {Job : JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Suppose that the jobs can exhibit self-suspensions. *) Context `{JobSuspension Job}. (** 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. (** First, we establish some basic lemmas regarding self-suspending jobs. *) Section BasicLemmas. (** We show that a self-suspended job cannot be ready, ... *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> ~~ job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> ~~ job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
SUS: ~~ suspension_has_passed sched j t
PEND: pending sched j t

~~ job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
SUS: ~~ suspension_has_passed sched j t
PEND: pending sched j t

~~ (suspension_has_passed sched j t && ~~ completed_by sched j t)
by rewrite negb_and; apply /orP; left. Qed. (** ... which trivially implies that the job cannot be scheduled. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> ~~ scheduled_at sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> ~~ scheduled_at sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
SUS: ~~ job_ready sched j t

~~ scheduled_at sched j t
by move: SUS; apply contra. Qed. (** Next, we observe that a self-suspended job has already arrived. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> has_arrived j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> has_arrived j t
by move=> j t /andP [? /andP [? ?]]. Qed. (** By definition, only pending jobs can be self-suspended. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> pending sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> pending sched j t
by move=> j t /andP [? ?]. Qed. (** Next, we note that self-suspended jobs are not backlogged. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> ~~ backlogged sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), suspended sched j t -> ~~ backlogged sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
SUS: ~~ job_ready sched j t

~~ backlogged sched j t
by rewrite /backlogged negb_and; apply /orP; left. Qed. (** Further, we prove that if a job is pending and not self-suspended then it is ready. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), pending sched j t -> ~~ suspended sched j t -> job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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

forall (j : Job) (t : instant), pending sched j t -> ~~ suspended sched j t -> job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
PEND: pending sched j t
NOTSUS: ~~ (~~ suspension_has_passed sched j t && pending sched j t)

job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
PEND: pending sched j t
NOTSUS: suspension_has_passed sched j t

job_ready sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t: instant
NOTSUS: suspension_has_passed sched j t
ARR: has_arrived j t
NOTCOMP: ~~ completed_by sched j t

job_ready sched j t
by rewrite /job_ready /suspension_ready_instance; apply /andP; split. Qed. End BasicLemmas. (** Next, we focus on bounding the self-suspension period of a job after receiving some amount of service. *) Section SuspensionBoundedinInterval. (** Consider any job [j] ... *) Variable j : Job. (** ... and any time interval <<[t1, t2)>>. *) Variable t1 t2 : instant. (** Now consider any amount of work [ρ]. *) Variable ρ : work. (** Our aim is to prove a bound on the self-suspension period of [j] after receiving an amount of service [ρ]. Note that it is possible that the job may not self-suspend after receiving [ρ] amount of service in which case [job_suspension j ρ = 0]. Additionally, it is also important to note that the job may self-suspend multiple times within an interval, and these self-suspension intervals are separated by an interval where the job gets serviced. We can refer each such self-suspension interval as a segment, and each such segment is characterized by the amount of service received by the job. Essentially here we are establishing a bound on the length of the self-suspension segment of [j] characterized by [ρ]. *) (** Note that we can have two cases here, either the job [j] starts a suspension segment within the interval <<[t1, t2)>>, or the job is already suspended at [t1]. *) Section Step1. (** Consider a point [tf] inside <<[t1, t2)>>. *) Variable tf : instant. Hypothesis INtf : t1 <= tf < t2. (** Let [tf] be the first point in the interval <<[t1, t2)>> that is also inside the self-suspension segment. *) Hypothesis H_suspended_tf : suspended sched j tf. Hypothesis H_service_at_tf : service sched j tf = ρ. Hypothesis H_before_tf : forall to, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ)). (** First, we prove a trivial result that the total suspension before [tf] is zero. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))

\sum_(t1 <= t < tf | service sched j t == ρ) suspended sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))

\sum_(t1 <= t < tf | service sched j t == ρ) suspended sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))

all (fun x : Datatypes_nat__canonical__eqtype_Equality => suspended sched j x == 0) [seq x <- index_iota t1 tf | service sched j x == ρ]
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to == ρ
INto: t1 <= to < tf

suspended sched j to == 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to == ρ
INto: t1 <= to < tf

~~ suspended sched j to -> suspended sched j to == 0
by move => /negPf ->. Qed. (** Next we consider the trivial case when the suspension period exceeds the interval <<[tf, t2)>>. *) Section TrivialCase. Hypothesis H_LEQ : t2 - tf <= job_suspension j ρ.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_LEQ: t2 - tf <= job_suspension j ρ

\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_LEQ: t2 - tf <= job_suspension j ρ

\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_LEQ: t2 - tf <= job_suspension j ρ

1 * size [seq j0 <- index_iota tf t2 | (fun j1 : Datatypes_nat__canonical__eqtype_Equality => service sched j j1 == ρ) j0] <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_LEQ: t2 - tf <= job_suspension j ρ

\sum_(i <- index_iota tf t2 | service sched j i == ρ) 1 <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_LEQ: t2 - tf <= job_suspension j ρ

\sum_(tf <= t0 < t2) 1 <= job_suspension j ρ
by rewrite sum1_size size_iota. Qed. End TrivialCase. (** Next, we consider the case when the suspension period is within the interval <<[tf, t2)>>. *) Section IntervalLengthLonger. Hypothesis H_GT : t2 - tf > job_suspension j ρ.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf

\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf

\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf

\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf <= i < tf + job_suspension j ρ | service sched j i == ρ) suspended sched j i + \sum_(tf + job_suspension j ρ <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf + job_suspension j ρ <= t < t2 | service sched j t == ρ) suspended sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
\sum_(tf <= i < tf + job_suspension j ρ | service sched j i == ρ) suspended sched j i + 0 <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf + job_suspension j ρ <= t < t2 | service sched j t == ρ) suspended sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

all (fun x : nat => suspended sched j x == 0) [seq x <- index_iota (tf + job_suspension j ρ) t2 | service sched j x == ρ]
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
INto: to \in [seq x <- index_iota (tf + job_suspension j ρ) t2 | service sched j x == ρ]
NOTSUSto: suspended sched j to != 0

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
INto: to \in [seq x <- index_iota (tf + job_suspension j ρ) t2 | service sched j x == ρ]
NOTSUSto: suspended sched j to != 0
A: forall b : bool, 0 < b -> b

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
INto: to \in [seq x <- index_iota (tf + job_suspension j ρ) t2 | service sched j x == ρ]
A: forall b : bool, 0 < b -> b
NOTSUSto: suspended sched j to

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
NOTSUSto: suspended sched j to
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

~~ suspension_has_passed sched j to && pending sched j to -> False
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

suspension_has_passed sched j to
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

suspension_has_passed sched j to
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

job_arrival j + job_suspension j ρ <= to
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2
no_progress_for sched j to (job_suspension j ρ)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

job_arrival j + job_suspension j ρ <= to
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2
LT: job_suspension j ρ <= to - tf

job_arrival j + job_suspension j ρ <= to
by move: (leq_add ARRj LT); rewrite subnKC //=; lia.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

no_progress_for sched j to (job_suspension j ρ)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

no_progress_for sched j to (job_suspension j ρ)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2

service sched j (to - job_suspension j ρ) == service sched j to
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2
SERVGT: ρ <= service sched j (to - job_suspension j ρ)

service sched j (to - job_suspension j ρ) == service sched j to
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
to: Datatypes_nat__canonical__eqtype_Equality
A: forall b : bool, 0 < b -> b
SERVto: service sched j to = ρ
INgt: tf + job_suspension j ρ <= to
INlt: to < t2
SERVGT: ρ <= service sched j (to - job_suspension j ρ)
SERVLT: service sched j (to - job_suspension j ρ) <= ρ

service sched j (to - job_suspension j ρ) == service sched j to
by apply /eqP; lia. } }
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf <= i < tf + job_suspension j ρ | service sched j i == ρ) suspended sched j i + 0 <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf <= i < tf + job_suspension j ρ | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

1 * size [seq j0 <- index_iota tf (tf + job_suspension j ρ) | (fun j1 : Datatypes_nat__canonical__eqtype_Equality => service sched j j1 == ρ) j0] <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(i <- index_iota tf (tf + job_suspension j ρ) | service sched j i == ρ) 1 <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
H_GT: job_suspension j ρ < t2 - tf
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf <= t0 < tf + job_suspension j ρ) 1 <= job_suspension j ρ
by rewrite sum1_size size_iota; lia. Qed. End IntervalLengthLonger. (** Now we prove the required bound in case a point like [tf] exists. This helps to simplify our final proof. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(t1 <= i < tf | service sched j i == ρ) suspended sched j i + \sum_(tf <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf

\sum_(tf <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
LEQ: t2 - tf <= job_suspension j ρ

\sum_(tf <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
GT: ~~ (t2 - tf <= job_suspension j ρ)
\sum_(tf <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
LEQ: t2 - tf <= job_suspension j ρ

\sum_(tf <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
by apply suspension_bounded_trivial.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
tf: instant
INtf: t1 <= tf < t2
H_suspended_tf: suspended sched j tf
H_service_at_tf: service sched j tf = ρ
H_before_tf: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))
ARRj: job_arrival j <= tf
PENDj: pending sched j tf
GT: ~~ (t2 - tf <= job_suspension j ρ)

\sum_(tf <= i < t2 | service sched j i == ρ) suspended sched j i <= job_suspension j ρ
by apply suspension_bounded_longer_interval; lia. Qed. End Step1. Section Step2. (** Now we prove that the point [tf], as used in the above lemmas, always exists if [suspended] is true at some point inside <<[t1, t2)>>. *) Hypothesis H_exists : (exists2 t, t \in index_iota t1 t2 & (suspended sched j t && (service sched j t == ρ))).
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ

exists t' : nat, t1 <= t' < t2 /\ suspended sched j t' /\ service sched j t' = ρ /\ (forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ

forall to : nat, t1 <= to < t' -> ~~ (suspended sched j to && (service sched j to == ρ))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'

~~ (suspended sched j to && (service sched j to == ρ))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))

~~ (suspended sched j to && (service sched j to == ρ))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))

index to (index_iota t1 t2) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: index to (index_iota t1 t2) < ind
~~ (suspended sched j to && (service sched j to == ρ))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))

index to (index_iota t1 t2) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))

index to (iota t1 (t2 - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')

index to (iota t1 (t2 - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')

(if to \in iota t1 (t' - t1) then index to (iota t1 (t' - t1)) else size (iota t1 (t' - t1)) + index to (iota (t1 + (t' - t1)) (t2 - t'))) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')

index to (iota t1 (t' - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)

index to (iota t1 (t' - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)

size (iota t1 (t' - t1)) <= index t' (index_iota t1 t2)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
GT: size (iota t1 (t' - t1)) <= index t' (index_iota t1 t2)
index to (iota t1 (t' - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)

size (iota t1 (t' - t1)) <= index t' (index_iota t1 t2)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)

size (iota t1 (t' - t1)) <= (if t' \in iota t1 (t' - t1) then index t' (iota t1 (t' - t1)) else size (iota t1 (t' - t1)) + index t' (iota (t1 + (t' - t1)) (t2 - t')))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)

size (iota t1 (t' - t1)) <= size (iota t1 (t' - t1)) + index t' (iota (t1 + (t' - t1)) (t2 - t'))
rewrite size_iota; by lia.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
GT: size (iota t1 (t' - t1)) <= index t' (index_iota t1 t2)

index to (iota t1 (t' - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
GT: size (iota t1 (t' - t1)) <= index t' (index_iota t1 t2)
LT: index to (iota t1 (t' - t1)) < t' - t1

index to (iota t1 (t' - t1)) < ind
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
LT: index to (iota t1 (t' - t1)) < t' - t1

ind < size (index_iota t1 t2)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
LT: index to (iota t1 (t' - t1)) < t' - t1
uniq (index_iota t1 t2)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
LT: index to (iota t1 (t' - t1)) < t' - t1

ind < size (index_iota t1 t2)
by rewrite /ind /P.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
LT: index to (iota t1 (t' - t1)) < t' - t1

uniq (index_iota t1 t2)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
SPLIT: t2 - t1 = t' - t1 + (t2 - t')
NOTINt': t' \notin iota t1 (t' - t1)
LT: index to (iota t1 (t' - t1)) < t' - t1

uniq (index_iota t1 t2)
by apply iota_uniq. }
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: index to (index_iota t1 t2) < ind

~~ (suspended sched j to && (service sched j to == ρ))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: index to (index_iota t1 t2) < ind

P to = false
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: index to (index_iota t1 t2) < ind
P to = false -> ~~ (suspended sched j to && (service sched j to == ρ))
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: index to (index_iota t1 t2) < ind

P to = false
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: P (nth 0 (index_iota t1 t2) (index to (index_iota t1 t2))) = false

P to = false
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))

to \in index_iota t1 t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
INto: t1 <= to < t'

to \in index_iota t1 t2
rewrite mem_index_iota; lia.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
H_exists: exists2 t : Datatypes_nat__canonical__eqtype_Equality, t \in index_iota t1 t2 & suspended sched j t && (service sched j t == ρ)
P:= fun t : instant => suspended sched j t && (service sched j t == ρ): instant -> bool
ind:= find P (index_iota t1 t2): nat
t':= nth 0 (index_iota t1 t2) ind: nat
indLT: find (fun t : nat => suspended sched j t && (service sched j t == ρ)) (index_iota t1 t2) < size (index_iota t1 t2)
INt': t1 <= t' < t2
SUSt': suspended sched j t'
SERVt': service sched j t' = ρ
to: nat
INto: to \in index_iota t1 t'
LT: index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1))
indexLT: index to (index_iota t1 t2) < ind

P to = false -> ~~ (suspended sched j to && (service sched j to == ρ))
by rewrite /P => ->. Qed. End Step2. (** Finally we prove the required result. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
HAS: exists2 x : Datatypes_nat__canonical__eqtype_Equality, x \in index_iota t1 t2 & suspended sched j x && (service sched j x == ρ)

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}
\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
HAS: exists2 x : Datatypes_nat__canonical__eqtype_Equality, x \in index_iota t1 t2 & suspended sched j x && (service sched j x == ρ)

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
HAS: exists2 x : Datatypes_nat__canonical__eqtype_Equality, x \in index_iota t1 t2 & suspended sched j x && (service sched j x == ρ)
tf: nat
INtf: t1 <= tf < t2
SUStf: suspended sched j tf
SERVtf: service sched j tf = ρ
tfFirst: forall to : nat, t1 <= to < tf -> ~~ (suspended sched j to && (service sched j to == ρ))

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
by apply: suspension_bounded_in_interval_aux.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}

\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}

all (fun x : Datatypes_nat__canonical__eqtype_Equality => suspended sched j x == 0) [seq x <- index_iota t1 t2 | service sched j x == ρ]
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}
to: Datatypes_nat__canonical__eqtype_Equality
INto: to \in [seq x <- index_iota t1 t2 | service sched j x == ρ]

suspended sched j to == 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to == ρ
INto: to \in index_iota t1 t2

suspended sched j to == 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
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
j: Job
t1, t2: instant
ρ: work
NOTHAS: {in index_iota t1 t2, forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ (suspended sched j x && (service sched j x == ρ))}
to: Datatypes_nat__canonical__eqtype_Equality
SERVto: service sched j to == ρ
INto: to \in index_iota t1 t2

~~ suspended sched j to -> suspended sched j to == 0
by move => /negPf ->. Qed. End SuspensionBoundedinInterval. End Suspensions.