Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** Note: we do not re-export the basic definitions to avoid littering the global namespace with type class instances. *) (** In this section we establish the classes to which an ideal schedule belongs. *) Section ScheduleClass. (** We assume ideal uni-processor schedules. *) #[local] Existing Instance ideal.processor_state. Local Transparent scheduled_in scheduled_on. (** Consider any job type and the ideal processor model. *) Context {Job: JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. (** We note that the ideal processor model is indeed a uni-processor model. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job

uniprocessor_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job

uniprocessor_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j1, j2: Job
sched: schedule (processor_state Job)
t: instant
E1: sched t = Some j1
E2: sched t = Some j2

j1 = j2
by move: E1 E2 =>->[]. Qed. (** By definition, [service_in] is the sum of the service received in total across all cores. In the ideal uniprocessor model, however, there is only one "core," which is expressed by using [unit] as the type of cores. The type [unit] only has a single member [tt], which serves as a placeholder. Consequently, the definition of [service_in] simplifies to a single term of the sum, the service on the one core, which we note with the following lemma that relates [service_in] to [service_on]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s = service_on j s tt
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s = service_on j s tt
by rewrite /service_in /index_enum Finite.EnumDef.enumDef /= big_seq1. Qed. (** Furthermore, since the ideal uniprocessor state is represented by the [option Job] type, [service_in] further simplifies to a simple equality comparison, which we note next. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s = (s == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s = (s == Some j)
by rewrite service_in_service_on. Qed. (** We observe that the ideal processor model falls into the category of ideal-progress models, i.e., a scheduled job always receives service. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job

ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job

ideal_progress_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

0 < service_in j (Some j)
by rewrite service_in_def /= eqxx /nat_of_bool. Qed. (** The ideal processor model is a unit-service model. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job

unit_service_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job

unit_service_proc_model (processor_state Job)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s <= 1
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

(if s == Some j then 1 else 0) <= 1
by case:ifP. Qed.
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

scheduled_in j s = (s == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

scheduled_in j s = (s == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

[exists c, s == Some j] = (s == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

~ (exists _ : unit_finType, s == Some j) -> false = (s == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

exists _ : unit, true
by exists. Qed.
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

scheduled_at sched j t = (sched t == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

scheduled_at sched j t = (sched t == Some j)
by rewrite /scheduled_at scheduled_in_def. Qed.
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s = scheduled_in j s
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job

service_in j s = scheduled_in j s
by rewrite service_in_def scheduled_in_def. Qed.
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

service_at sched j t = scheduled_at sched j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

service_at sched j t = scheduled_at sched j t
by rewrite /service_at service_in_is_scheduled_in. Qed.
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
c: Core

service_on j s c = (s == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
c: Core

service_on j s c = (s == Some j)
done. Qed.
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

service_at sched j t = (sched t == Some j)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

service_at sched j t = (sched t == Some j)
by rewrite /service_at service_in_def. Qed. (** Next we prove a lemma which helps us to do a case analysis on the state of an ideal schedule. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job

forall (sched : schedule (processor_state Job)) (t : instant), is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job

forall (sched : schedule (processor_state Job)) (t : instant), is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant

is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
s: Job
EQ: sched t = Some s

Some s == None \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None
None == None \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
s: Job
EQ: sched t = Some s

Some s == None \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None
None == None \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None

None == None \/ (exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None

None == None \/ (exists j : Job, scheduled_at sched j t)
by left; auto. Qed. (** We prove that if a job [j] is scheduled at a time instant [t], then the scheduler is not idle at [t]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

scheduled_at sched j t -> ~ is_idle sched t
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

scheduled_at sched j t -> ~ is_idle sched t
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
SCHED: sched t = Some j
IDLE: sched t = None

False
by rewrite IDLE in SCHED; inversion SCHED. Qed. (** On a similar note, if a scheduler is idle at a time instant [t], then no job can receive service at [t]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

is_idle sched t -> service_at sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant

is_idle sched t -> service_at sched j t = 0
by rewrite service_at_is_scheduled_at scheduled_at_def => /eqP ->. Qed. End ScheduleClass. (** * Incremental Service in Ideal Schedule *) (** In the following section we prove a few facts about service in ideal schedule. *) (* Note that these lemmas can be generalized to an arbitrary scheduler. *) Section IncrementalService. (** Consider any job type, ... *) Context {Job : JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. (** ... any arrival sequence, ... *) Variable arr_seq : arrival_sequence Job. (** ... and any ideal uni-processor schedule of this arrival sequence. *) Variable sched : schedule (ideal.processor_state Job). (** As a base case, we prove that if a job [j] receives service in some time interval <<[t1,t2)>>, then there exists a time instant <<t ∈ [t1,t2)>> such that [j] is scheduled at time [t] and [t] is the first instant where [j] receives service. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)

forall (j : Job) (t1 t2 : instant), 0 < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)

forall (j : Job) (t1 t2 : instant), 0 < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2

t1 <= t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2

t1 <= t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
CONTR: t2 < t1

False
by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

t1 <= t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

t1 <= t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
CONTR: t2 <= t1

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

service_during sched j t1 t1 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true

service_during sched j t1 t1 = 0
by rewrite /service_during big_geq.
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = false

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = false

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1

0 < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
IN: t \in index_iota t1 t2
SCHEDt: 0 < service_at sched j t

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
IN: t \in index_iota t1 t2
SCHEDt: sched t == Some j

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN: t1 <= t < t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
A: scheduled_at sched j t -> exists t0 : nat, t1 < t0 <= t /\ (forall x : nat, t1 <= x < t0 -> ~~ scheduled_at sched j x) /\ scheduled_at sched j t0

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
A: exists t0 : nat, t1 < t0 <= t /\ (forall x : nat, t1 <= x < t0 -> ~~ scheduled_at sched j x) /\ scheduled_at sched j t0

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

t1 <= x < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

t1 <= x < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

x < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x

forall i : nat, (t1 <= i < x) && true -> service_at sched j i = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
y: nat
T5: t1 <= y < x

service_at sched j y = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
y: nat
T5: t1 <= y < x

service_at sched j y == 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
y: nat
T5: t1 <= y < x

sched y != Some j
by specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2. } Qed. (** Furthermore, we observe that, if a job receives some positive amount of service during an interval <<[t1, t2)>>, then the interval can't be empty and hence [t1 < t2]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)

forall (j : Job) (t1 t2 : instant) (k : nat), k < service_during sched j t1 t2 -> t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)

forall (j : Job) (t1 t2 : instant) (k : nat), k < service_during sched j t1 t2 -> t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2

t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2

~~ (t2 < t1.+1)
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
CONTR: t2 < t1.+1

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
CONTR: t2 < t1.+1

k < service_during sched j t1 t2 -> False
by rewrite /service_during big_geq. Qed. (** Next, we prove that if in some time interval <<[t1,t2)>> a job [j] receives [k] units of service, then there exists a time instant <<t ∈ [t1,t2)>> such that [j] is scheduled at time [t] and service of job [j] within interval <<[t1,t)>> is equal to [k]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)

forall (j : Job) (t1 t2 : instant) (k : nat), k < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)

forall (j : Job) (t1 t2 : instant) (k : nat), k < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
LE: t1 < t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
IHk: k < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
IHk: exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k

service_during sched j t1 t.+1 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k

service_during sched j t1 t.+1 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k

service_during sched j t1 t + service_during sched j t t.+1 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k

service_during sched j t t.+1 == 1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k

(sched t == Some j) == 1
by rewrite eqb1 -scheduled_at_def /=.
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1

t1 <= t.+1 <= t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
k.+1 < service_during sched j t1 t.+1 + service_during sched j t.+1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1

t1 <= t.+1 <= t2
by apply/andP; split; first apply leq_trans with t.
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1

k.+1 < service_during sched j t1 t.+1 + service_during sched j t.+1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

t1 <= t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

t1 <= t.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

t1 <= t.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true

t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
CONTR: t2 <= t.+1

False
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: ~~ scheduled_at sched j t.+1

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
INx: x \in index_iota t.+1 t2
SCHEDx: 0 < service_at sched j x

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
INx: x \in index_iota t.+1 t2
SCHEDx: sched x == Some j

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx: t < x < t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
A: scheduled_at sched j x -> exists t0 : nat, t.+1 < t0 <= x /\ (forall x : nat, t < x < t0 -> ~~ scheduled_at sched j x) /\ scheduled_at sched j t0

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
A: exists t0 : nat, t.+1 < t0 <= x /\ (forall x : nat, t < x < t0 -> ~~ scheduled_at sched j x) /\ scheduled_at sched j t0

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

t1 <= y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

t1 <= y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

t1 <= y
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

t <= y
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

\sum_(t1 <= i < t.+1) service_at sched j i + \sum_(t.+1 <= i < y) service_at sched j i = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

k.+1 + \sum_(t.+1 <= i < y) service_at sched j i == k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y

\sum_(t.+1 <= i < y) service_at sched j i == 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
z: nat
H5: t < z < y

service_at sched j z = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
z: nat
H5: t < z < y

service_at sched j z == 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat, t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
z: nat
H5: t < z < y

sched z != Some j
by specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2. Qed. End IncrementalService. (** * Automation *) (** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve ideal_proc_model_is_a_uniprocessor_model ideal_proc_model_ensures_ideal_progress ideal_proc_model_provides_unit_service : basic_rt_facts. (** We also provide tactics for case analysis on ideal processor state. *) (** The first tactic generates two sub-goals: one with idle processor and the other with processor executing a job named [JobName]. *) Ltac ideal_proc_model_sched_case_analysis sched t JobName := let Idle := fresh "Idle" in let Sched := fresh "Sched_" JobName in destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]]. (** The second tactic is similar to the first, but it additionally generates two equalities: [sched t = None] and [sched t = Some j]. *) Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName := let Idle := fresh "Idle" in let IdleEq := fresh "Eq" Idle in let Sched := fresh "Sched_" JobName in let SchedEq := fresh "Eq" Sched in destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]]; [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq | move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].