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.analysis.definitions.job_properties. Require Export prosa.analysis.facts.behavior.all. Require Export prosa.analysis.facts.model.sequential. Require Export prosa.model.preemption.limited_preemptive. (** * Platform for Models with Limited Preemptions *) (** In this section, we prove that instantiation of predicate [job_preemptable] to the model with limited preemptions indeed defines a valid preemption model. *) Section ModelWithLimitedPreemptions. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** In addition, assume the existence of a function that maps a job to the sequence of its preemption points... *) Context `{JobPreemptionPoints Job}. (** ..., i.e., we assume limited-preemptive jobs. *) #[local] Existing Instance limited_preemptive_job_model. (** Consider any arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** Next, consider any limited-preemptive schedule of this arrival sequence ... *) Context {PState : ProcessorState Job}. Variable sched : schedule PState. Hypothesis H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched. (** ...where jobs do not execute after their completion. *) Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched. (** Next, we assume that preemption points are defined by the job-level model with limited preemptions. *) Hypothesis H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq. (** First, we prove a few auxiliary lemmas. *) Section AuxiliaryLemmas. (** Consider a job j. *) Variable j : Job. Hypothesis H_j_arrives : arrives_in arr_seq j. (** Recall that 0 is a preemption point. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

0 \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

0 \in job_preemptive_points j
by apply H_valid_limited_preemptions_job_model. Qed. (** Using the fact that [job_preemptive_points] is a non-decreasing sequence, we prove that the first element of [job_preemptive_points] is 0. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

first0 (job_preemptive_points j) = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

first0 (job_preemptive_points j) = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
F: 0 \in job_preemptive_points j

first0 (job_preemptive_points j) = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
F: 0 \in job_preemptive_points j
C: nondecreasing_sequence (job_preemptive_points j)

first0 (job_preemptive_points j) = 0
by apply nondec_seq_zero_first. Qed. (** We prove that the list of preemption points is not empty. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

0 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

0 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

0 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
CONTR: job_preemptive_points j == [::]

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: 0 \in job_preemptive_points j
END: end_of_execution_in_preemption_points arr_seq
CONTR: job_preemptive_points j == [::]

False
by move: CONTR BEG => /eqP; rewrite /beginning_of_execution_in_preemption_points => ->. Qed. (** Next, we prove that the cost of a job is a preemption point. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

job_cost j \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

job_cost j \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

job_cost j \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
EQ: last0 (job_preemptive_points j) = job_cost j

job_cost j \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

last0 (job_preemptive_points j) \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

nth 0 (job_preemptive_points j) (size (job_preemptive_points j)).-1 \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

exists2 i : nat, i < size (job_preemptive_points j) & nth 0 (job_preemptive_points j) i = nth 0 (job_preemptive_points j) (size (job_preemptive_points j)).-1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

(size (job_preemptive_points j)).-1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

0 < size (job_preemptive_points j)
exact: list_of_preemption_point_is_not_empty. Qed. (** As a corollary, we prove that the sequence of non-preemptive points of a job with positive cost contains at least 2 points. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

job_cost_positive j -> 1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

job_cost_positive j -> 1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j

1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
EQ: 2 = size [:: 0; job_cost j]

1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

size [:: 0; job_cost j] <= size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

uniq [:: 0; job_cost j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
forall x : Datatypes_nat__canonical__eqtype_Equality, x \in [:: 0; job_cost j] -> x \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

uniq [:: 0; job_cost j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

[&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

[&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

0 \notin [:: job_cost j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
(job_cost j \notin [::]) && uniq [::]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

0 \notin [:: job_cost j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

0 != job_cost j
rewrite neq_ltn; apply/orP; left; eauto 2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

(job_cost j \notin [::]) && uniq [::]
by apply/andP. }
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq

forall x : Datatypes_nat__canonical__eqtype_Equality, x \in [:: 0; job_cost j] -> x \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
t: Datatypes_nat__canonical__eqtype_Equality

[|| t == 0, t == job_cost j | t \in [::]] -> t \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = 0

t \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = job_cost j
t \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = 0

t \in job_preemptive_points j
by rewrite EQ; apply zero_in_preemption_points.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
POS: job_cost_positive j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = job_cost j

t \in job_preemptive_points j
by rewrite EQ; apply job_cost_in_nonpreemptive_points. Qed. (** Next we prove that "anti-density" property (from [preemption.util] file) holds for [job_preemption_point j]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

forall ρ : work, ρ <= job_cost j -> ρ \notin job_preemptive_points j -> first0 (job_preemptive_points j) <= ρ < last0 (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

forall ρ : work, ρ <= job_cost j -> ρ \notin job_preemptive_points j -> first0 (job_preemptive_points j) <= ρ < last0 (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j

first0 (job_preemptive_points j) <= ρ < last0 (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq

first0 (job_preemptive_points j) <= ρ < last0 (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq

first0 (job_preemptive_points j) <= ρ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq
ρ < last0 (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq

first0 (job_preemptive_points j) <= ρ
by rewrite zero_is_first_element.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq

ρ < last0 (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq

ρ < job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq

ρ != job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq
CONTR: ρ = job_cost j

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq
CONTR: ρ = job_cost j
NotIN: job_cost j \notin job_preemptive_points j

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
BEG: beginning_of_execution_in_preemption_points arr_seq
END: end_of_execution_in_preemption_points arr_seq
NDEC: preemption_points_is_nondecreasing_sequence arr_seq
CONTR: ρ = job_cost j

job_cost j \in job_preemptive_points j
by apply job_cost_in_nonpreemptive_points. Qed. (** We also prove that any work that doesn't belong to preemption points of job j is placed strictly between two neighboring preemption points. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

forall ρ : work, ρ <= job_cost j -> ρ \notin job_preemptive_points j -> exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

forall ρ : work, ρ <= job_cost j -> ρ \notin job_preemptive_points j -> exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j

exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
ZERO: job_cost j = 0

exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j
exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
ZERO: job_cost j = 0

exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
ZERO: job_cost j = 0

ρ \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
ZERO: job_cost j = 0

ρ <= job_cost j -> ρ \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
ZERO: job_cost j = 0

0 \in job_preemptive_points j
by apply zero_in_preemption_points.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j

exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) n <= ρ
N2: ρ < nth 0 (job_preemptive_points j) n.+1

exists n : nat, n.+1 < size (job_preemptive_points j) /\ nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) n <= ρ
N2: ρ < nth 0 (job_preemptive_points j) n.+1

nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) n <= ρ
N2: ρ < nth 0 (job_preemptive_points j) n.+1

nth 0 (job_preemptive_points j) n < ρ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N2: ρ < nth 0 (job_preemptive_points j) n.+1
EQ: nth 0 (job_preemptive_points j) n = ρ

nth 0 (job_preemptive_points j) n < ρ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
NotIN: ρ \notin job_preemptive_points j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N2: ρ < nth 0 (job_preemptive_points j) n.+1
EQ: nth 0 (job_preemptive_points j) n = ρ

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N2: ρ < nth 0 (job_preemptive_points j) n.+1
EQ: nth 0 (job_preemptive_points j) n = ρ

ρ \in job_preemptive_points j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
ρ: work
LE: ρ <= job_cost j
POS: 0 < job_cost j
n: nat
SIZE2: n.+1 < size (job_preemptive_points j)
N2: ρ < nth 0 (job_preemptive_points j) n.+1

nth 0 (job_preemptive_points j) n \in job_preemptive_points j
by rewrite mem_nth. Qed. (** Recall that the module [prosa.model.preemption.parameters] also defines a notion of preemption points, namely [job_preemption_points], which cannot have duplicated preemption points. Therefore, we need additional lemmas to relate [job_preemption_points] and [job_preemptive_points]. *) (** First we show that the length of the last non-preemptive segment in [job_preemption_points] is equal to the length of the last non-empty non-preemptive segment of [job_preemptive_points]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

last0 (distances (job_preemption_points j)) = last0 [seq x <- distances (job_preemptive_points j) | 0 < x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

last0 (distances (job_preemption_points j)) = last0 [seq x <- distances (job_preemptive_points j) | 0 < x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

last0 (distances (job_preemption_points j)) = last0 [seq x <- distances (job_preemptive_points j) | 0 < x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

last0 (distances [seq ρ <- range 0 (job_cost j) | ρ \in job_preemptive_points j]) = last0 [seq x <- distances (job_preemptive_points j) | 0 < x]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

forall x : nat, x \in job_preemptive_points j -> x <= job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

forall x : nat, x \in job_preemptive_points j -> x <= last0 (job_preemptive_points j)
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2. Qed. (** Next we show that the length of the max non-preemptive segment of [job_preemption_points] is equal to the length of the max non-preemptive segment of [job_preemptive_points]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

max0 (distances (job_preemption_points j)) = max0 (distances (job_preemptive_points j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j

max0 (distances (job_preemption_points j)) = max0 (distances (job_preemptive_points j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

max0 (distances (job_preemption_points j)) = max0 (distances (job_preemptive_points j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

max0 (distances [seq ρ <- range 0 (job_cost j) | ρ \in job_preemptive_points j]) = max0 (distances (job_preemptive_points j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

max0 [seq x <- distances (job_preemptive_points j) | 0 < x] = max0 (distances (job_preemptive_points j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq
forall x : nat, x \in job_preemptive_points j -> x <= job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

max0 [seq x <- distances (job_preemptive_points j) | 0 < x] = max0 (distances (job_preemptive_points j))
by rewrite max0_rem0 //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

forall x : nat, x \in job_preemptive_points j -> x <= job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
H_j_arrives: arrives_in arr_seq j
A1: beginning_of_execution_in_preemption_points arr_seq
A2: end_of_execution_in_preemption_points arr_seq
A3: preemption_points_is_nondecreasing_sequence arr_seq

forall x : nat, x \in job_preemptive_points j -> x <= last0 (job_preemptive_points j)
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2. Qed. End AuxiliaryLemmas. (** We prove that the [fixed_preemption_point_model] function defines a valid preemption model. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq

valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq

valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

job_cannot_become_nonpreemptive_before_execution j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
job_cannot_be_nonpreemptive_after_completion j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
not_preemptive_implies_scheduled sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
execution_starts_with_preemption_point sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

job_cannot_become_nonpreemptive_before_execution j
by apply zero_in_preemption_points.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

job_cannot_be_nonpreemptive_after_completion j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
not_preemptive_implies_scheduled sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
execution_starts_with_preemption_point sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

job_cannot_be_nonpreemptive_after_completion j
by apply job_cost_in_nonpreemptive_points.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

not_preemptive_implies_scheduled sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
execution_starts_with_preemption_point sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

not_preemptive_implies_scheduled sched j
by move => t NPP; apply H_schedule_respects_preemption_model.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

execution_starts_with_preemption_point sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j

execution_starts_with_preemption_point sched j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
t: instant
NSCHED: ~~ scheduled_at sched j t
SCHED: scheduled_at sched j t.+1

job_preemptable j (service sched j t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
t: instant
NSCHED: ~~ scheduled_at sched j t
SCHED: scheduled_at sched j t.+1

job_preemptable j (service sched j t)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
t: instant
NSCHED: ~~ scheduled_at sched j t
SCHED: scheduled_at sched j t.+1
NP: ~~ job_preemptable j (service sched j t)

false
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model: valid_limited_preemptions_job_model arr_seq
j: Job
ARR: arrives_in arr_seq j
t: instant
NSCHED: ~~ scheduled_at sched j t
SCHED: scheduled_at sched j t.+1
NP: ~~ job_preemptable j (service sched j t)

scheduled_at sched j t -> false
by move: NSCHED => /negP. } Qed. End ModelWithLimitedPreemptions. Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.