Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.model.aggregate.workload. Require Export prosa.model.aggregate.service_of_jobs. Require Export prosa.analysis.facts.model.service_of_jobs. Require Export prosa.analysis.facts.behavior.completion. Require Export prosa.analysis.facts.model.scheduled. (** * Service Received by Sets of Jobs in Uniprocessor Ideal-Progress Schedules *) (** In this file, we establish a fact about the service received by _sets_ of jobs in the presence of idle times on a uniprocessor under the ideal-progress assumption (i.e., that a scheduled job necessarily receives nonzero service). *) Section IdealModelLemmas. (** Consider any type of tasks ... *) Context {Task : TaskType}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Consider any arrival sequence with consistent arrivals. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** Allow for any uniprocessor model that ensures ideal progress. *) Context {PState : ProcessorState Job}. Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState. Hypothesis H_uniproc : uniprocessor_model PState. (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *) Variable sched : schedule PState. Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq. (** ... where jobs do not execute before their arrival or after completion. *) Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched. (** Let [P] be any predicate over jobs. *) Variable P : pred Job. (** We prove that if the total service within some time interval <<[t1,t2)>> is smaller than <<t2 - t1>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job

forall t1 t2 : instant, service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 -> exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job

forall t1 t2 : instant, service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 -> exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1

exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = false

exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = true
exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = false

exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1

t2 < t1 -> exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LT: t2 - t1 == 0

exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
by move: LT => /eqP -> in SERV; rewrite ltn0 in SERV.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = true

exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = true

exists δ : nat, t2 = t1 + δ
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = true
EX: exists δ : nat, t2 = t1 + δ
exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = true

exists δ : nat, t2 = t1 + δ
by exists (t2 - t1); rewrite subnKC // ltnW.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1, t2: instant
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
LE: (t1 <= t2) = true
EX: exists δ : nat, t2 = t1 + δ

exists t : nat, t1 <= t < t2 /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ: nat
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 (t1 + δ)) t1 (t1 + δ) < t1 + δ - t1

exists t : nat, t1 <= t < t1 + δ /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ: nat
SERV: service_of_jobs sched predT (arrivals_between arr_seq 0 (t1 + δ)) t1 (t1 + δ) < δ

exists t : nat, t1 <= t < t1 + δ /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ: nat
SERV: \sum_(t1 <= j < t1 + δ) \sum_(i <- arrivals_between arr_seq 0 (t1 + δ)) service_at sched i j < δ

exists t : nat, t1 <= t < t1 + δ /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ: nat
SERV: exists x : nat, t1 <= x < t1 + δ /\ \sum_(i <- arrivals_between arr_seq 0 (t1 + δ)) service_at sched i x = 0

exists t : nat, t1 <= t < t1 + δ /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ)) service_at sched i x = 0

exists t : nat, t1 <= t < t1 + δ /\ is_idle arr_seq sched t
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ)) service_at sched i x = 0

is_idle arr_seq sched x
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
L: \sum_(i <- arrivals_between arr_seq 0 (t1 + δ)) service_at sched i x = 0
j: Job
SCHED: scheduled_at sched j x

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

service_at sched j x == 0
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}
service_at sched j x = 0 -> False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

service_at sched j x == 0
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

arrived_between j 0 (t1 + δ)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

job_arrival j < t1 + δ
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

job_arrival j <= x -> job_arrival j < t1 + δ
lia.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
PState: ProcessorState Job
H_ideal_progress_proc_model: ideal_progress_proc_model PState
H_uniproc: uniprocessor_model PState
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
P: pred Job
t1: instant
δ, x: nat
GEx: t1 <= x
LEx: x < t1 + δ
j: Job
SCHED: scheduled_at sched j x
L: {in arrivals_between arr_seq 0 (t1 + δ), forall x0 : Job, service_at sched x0 x == 0}

service_at sched j x = 0 -> False
by rewrite -no_service_not_scheduled // => /negP. Qed. End IdealModelLemmas.