Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * Platform for Models with Limited Preemptions *) (** In this section, we prove that instantiation of functions [job_preemptable and task_preemption_points] to the limited preemptions model indeed defines a valid preemption model with bounded non-preemptive regions. *) Section LimitedPreemptionsModel. (** 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}. (** We assume that jobs are preemptable only at specific points during their execution, ... *) Context `{JobPreemptionPoints Job}. Context `{TaskPreemptionPoints Task}. (** ... 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 ideal uni-processor preemption-aware schedule of this arrival sequence ... *) Variable sched : schedule (ideal.processor_state Job). Hypothesis H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched. (** ... 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. (** Consider an arbitrary task set ts. *) Variable ts : list Task. (** Next, we assume that preemption points are defined by the model with fixed preemption points. *) Hypothesis H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts. (** Then we prove that functions [job_preemptable and task_preemption_points] define a model with bounded non-preemptive regions. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0

job_respects_max_nonpreemptive_segment j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0
nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0

max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <= task_max_nonpreemptive_segment (job_task j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0
nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0

nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0

nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0
progr: duration
LE: progr = 0

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO: job_cost j = 0
progr: duration
LE: progr = 0

job_preemptable j 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j

job_respects_max_nonpreemptive_segment j /\ nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j

job_respects_max_nonpreemptive_segment j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = true
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j

job_respects_max_nonpreemptive_segment j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = true
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j

max0 (distances (job_preemptive_points j)) <= task_max_nonpreemptive_segment (job_task j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = true
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = true

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = true

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: (progr \in job_preemptive_points j) = false

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N: nth 0 (job_preemptive_points j) x < progr < nth 0 (job_preemptive_points j) x.+1

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

job_preemptable j ptr
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

job_preemptable j ptr
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptl + (job_max_nonpreemptive_segment j - ε) + 1 <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptl + (job_max_nonpreemptive_segment j - ε) + 1 <= progr + (job_max_nonpreemptive_segment j - ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr <= ptl + (max0 (lengths_of_segments j) - ε) + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr - ptl + 1 <= max0 (lengths_of_segments j) - ε + 1 + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr - ptl + 1 - 1 <= max0 (lengths_of_segments j) - ε + 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

(ptr - ptl).+1.-1 <= max0 (lengths_of_segments j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
0 < max0 (lengths_of_segments j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

(ptr - ptl).+1.-1 <= max0 (lengths_of_segments j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr - ptl <= max0 (lengths_of_segments j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr - ptl <= max0 (distances (job_preemption_points j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

ptr - ptl <= max0 (distances (job_preemptive_points j))
by apply distance_between_neighboring_elements_le_max_distance_in_seq.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

0 < max0 (lengths_of_segments j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

0 < max0 (lengths_of_segments j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

0 < 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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

exists x y : nat_eqType, x \in job_preemptive_points j /\ y \in job_preemptive_points j /\ x <> y
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
0 <> job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
0 <> job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
0 <> job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat
0 <> job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

0 <> job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
FIX: valid_fixed_preemption_points_task_model arr_seq ts
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
A1: task_beginning_of_execution_in_preemption_points ts
A2: task_end_of_execution_in_preemption_points ts
A3: nondecreasing_task_preemption_points ts
A4: consistent_job_segment_count arr_seq
A5: job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS: 0 < job_cost j
progr: duration
LE: progr <= job_cost j
NotIN: progr \notin job_preemptive_points j
x: nat
SIZE2: x.+1 < size (job_preemptive_points j)
N1: nth 0 (job_preemptive_points j) x < progr
N2: progr < nth 0 (job_preemptive_points j) x.+1
ptl:= nth 0 (job_preemptive_points j) x: nat
ptr:= nth 0 (job_preemptive_points j) x.+1: nat

0 <> job_cost j
by apply/eqP; rewrite eq_sym -lt0n; apply POS. } Qed. (** Which together with lemma [valid_fixed_preemption_points_model] gives us the fact that functions [job_preemptable and task_preemption_points] defines a valid preemption model with bounded non-preemptive regions. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

valid_model_with_bounded_nonpreemptive_segments arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

valid_model_with_bounded_nonpreemptive_segments arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

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
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts
model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JobPreemptionPoints Job
H4: TaskPreemptionPoints Task
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model: schedule_respects_preemption_model arr_seq sched
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
ts: seq Task
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model arr_seq ts

model_with_bounded_nonpreemptive_segments arr_seq
by apply fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions. Qed. End LimitedPreemptionsModel. (** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve valid_fixed_preemption_points_model_lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.