Require Export prosa.model.preemption.limited_preemptive.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.task.preemption.floating_nonpreemptive.
Require Export prosa.analysis.facts.preemption.job.limited.

(** * Platform for Floating Non-Preemptive Regions Model *)

(** In this section, we prove that instantiation of functions
    [job_preemptable] and [task_max_nonpreemptive_segment] for the model
    with floating non-preemptive regions indeed defines a valid
    preemption model with bounded non-preemptive regions. *)
Section FloatingNonPreemptiveRegionsModel.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** In addition, we assume the existence of a function mapping a
      task to its maximal non-preemptive segment ... *)
  Context `{TaskMaxNonpreemptiveSegment Task}.

  (** .. and the existence of functions mapping a
      job to the sequence of its preemption points, ... *)
  Context `{JobPreemptionPoints Job}.
  (** ... i.e., we assume limited-preemptive jobs. *)
  #[local] Existing Instance limited_preemptive_job_model.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** Next, consider any preemption-aware schedule of this arrival sequence... *)
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.
  Hypothesis H_preemption_aware_schedule:
    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.

  (** Next, we assume that preemption points are defined by the model
      with floating non-preemptive regions. *)
  Hypothesis H_valid_model_with_floating_nonpreemptive_regions:
    valid_model_with_floating_nonpreemptive_regions arr_seq.

  (** Then, we prove that the [job_preemptable and
      task_max_nonpreemptive_segment] functions define
      a model with bounded non-preemptive regions. *)
  Lemma floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
    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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
model_with_bounded_nonpreemptive_segments arr_seq
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
model_with_bounded_nonpreemptive_segments arr_seq
    intros j ARR.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
    move: (H_valid_model_with_floating_nonpreemptive_regions) => LIM; move: LIM (LIM) => [LIM L] [[BEG [END NDEC]] MAX].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
    case: (posnP (job_cost j)) => [ZERO|POS].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
ZERO: job_cost j = 0
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j split.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
ZERO: job_cost j = 0
job_respects_max_nonpreemptive_segment j rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
              /lengths_of_segments /job_preemption_points; rewrite ZERO; simpl.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
ZERO: job_cost j = 0
max0
  (distances
     (if job_preemptable j 0 then [:: 0] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
        by rewrite /job_preemptable /limited_preemptive_job_model; erewrite zero_in_preemption_points; eauto 2.
      +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
ZERO: job_cost j = 0
nonpreemptive_regions_have_bounded_length j move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
ZERO: job_cost j = 0
progr: duration
LE: progr = 0
exists pp : duration,
  progr <= pp <=
  progr + (job_max_nonpreemptive_segment j - 1) /\
  job_preemptable j pp
        exists 0; rewrite LE; split; first by apply/andP; split.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
ZERO: job_cost j = 0
progr: duration
LE: progr = 0
job_preemptable j 0
          by eapply zero_in_preemption_points; eauto 2.
    -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemptive_points j) eqn:NotIN).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp
      +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
POS: 0 < job_cost j
job_respects_max_nonpreemptive_segment j by apply MAX.
      +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp by exists progr; split; first apply/andP; first split; rewrite ?leq_addr // conversion_preserves_equivalence.
      +
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp move: NotIN => /eqP; rewrite eqbF_neg; move => NotIN.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp
        edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp move: N => /andP [N1 N2].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp
        set ptl := nth 0 (job_preemptive_points j) x.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp
        set ptr := nth 0 (job_preemptive_points j) x.+1.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) /\
  job_preemptable j pp
        exists ptr; split; first last.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1)
        *
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 by unfold job_preemptable, limited_preemptive_job_model; apply mem_nth.
        *
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1) apply/andP; split; first by apply ltnW.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 - 1)
          apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) + 1 <=
progr + (job_max_nonpreemptive_segment j - 1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) + 1
          --
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) + 1 <=
progr + (job_max_nonpreemptive_segment j - 1) rewrite addn1 ltn_add2r; apply N1.
          --
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) + 1 unfold job_max_nonpreemptive_segment.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) + 1
             rewrite -addnA -leq_subLR -(leq_add2r 1).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 + 1
             rewrite [in X in _ <= X]addnC -leq_subLR.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 + 1
             rewrite !subn1 !addn1 prednK.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) rewrite -[_.+1.-1]pred_Sn.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) rewrite /lengths_of_segments.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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))
               erewrite job_parameters_max_np_to_job_limited; eauto.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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) rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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))
               apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 : Datatypes_nat__canonical__eqtype_Equality,
  x \in job_preemptive_points j /\
  y \in job_preemptive_points j /\ x <> y
               exists 0, (job_cost j); repeat split.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 by eapply zero_in_preemption_points; eauto.
               -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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 by eapply job_cost_in_nonpreemptive_points; eauto.
               -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
j: Job
ARR: arrives_in arr_seq j
LIM: valid_limited_preemptions_job_model arr_seq
L: job_respects_task_max_np_segment arr_seq
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
MAX: job_respects_task_max_np_segment arr_seq
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_max_nonpreemptive_segment] define a valid preemption model
      with bounded non-preemptive regions. *)
  Corollary floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
    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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
    split.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
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: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
valid_preemption_model arr_seq sched apply valid_fixed_preemption_points_model_lemma; auto.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
valid_limited_preemptions_job_model arr_seq
        by apply H_valid_model_with_floating_nonpreemptive_regions.
    -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: TaskMaxNonpreemptiveSegment Task
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
sched: schedule PState
H_preemption_aware_schedule: 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
H_valid_model_with_floating_nonpreemptive_regions: valid_model_with_floating_nonpreemptive_regions
  arr_seq
model_with_bounded_nonpreemptive_segments arr_seq by apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
  Qed.

End FloatingNonPreemptiveRegionsModel.

(** 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
     floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
     floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.