Require Export prosa.analysis.facts.preemption.task.limited.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.model.task.preemption.limited_preemptive.

(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
    to completion threshold] to the model with limited preemptions
    indeed defines a valid run-to-completion threshold function. *)
Section TaskRTCThresholdLimitedPreemptions.

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

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

  (** We assume a task model with fixed preemption points. *)
  #[local] Existing Instance limited_preemptive_job_model.
  #[local] Existing Instance limited_preemptions_rtc_threshold.

  (** Consider any arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

  (** Next, consider any preemption-aware schedule of this arrival sequence... *)
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.
  Hypothesis H_schedule_respects_preemption_model:
    schedule_respects_preemption_model arr_seq sched.

  (** ... where jobs do not execute 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 : seq Task.

  (** Assume that a job cost cannot be larger than a task cost. *)
  Hypothesis H_valid_job_cost:
    arrivals_have_valid_job_costs arr_seq.

  (** Consider the model with fixed preemption points. I.e., each task
      is divided into a number of non-preemptive segments by inserting
      statically predefined preemption points. *)
  Hypothesis H_valid_fixed_preemption_points_model:
    valid_fixed_preemption_points_model arr_seq ts.

  (** And consider any task from task set ts with positive cost. *)
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.
  Hypothesis H_positive_cost : 0 < task_cost tsk.

  (** We start by proving an auxiliary lemma. Note that since [tsk]
      has a positive cost, [task_preemption_points tsk] contains [0]
      and [task_cost tsk]. Thus, [2 <= size (task_preemption_points tsk)]. *)
  Remark number_of_preemption_points_in_task_at_least_two: 2 <= size (task_preemption_points tsk).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
1 < size (task_preemption_points tsk)
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
1 < size (task_preemption_points tsk)
    move: (H_valid_fixed_preemption_points_model) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
1 < size (task_preemption_points tsk)
    have Fact2: 0 < size (task_preemption_points tsk).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
0 < size (task_preemption_points tsk)
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
1 < size (task_preemption_points tsk)
    {
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
0 < size (task_preemption_points tsk) apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
CONTR: size (task_preemption_points tsk) = 0
False
      move: (END _ H_tsk_in_ts) => EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
CONTR: size (task_preemption_points tsk) = 0
EQ: last0 (task_preemption_points tsk) =
task_cost tsk
False
      move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
CONTR: size (task_preemption_points tsk) = 0
0 = task_cost tsk -> False
      by move=> EQ; move: (H_positive_cost); rewrite EQ ltnn.
    }
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
1 < size (task_preemption_points tsk)
    have EQ: 2 = size [::0; task_cost tsk] by [].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
EQ: 2 = size [:: 0; task_cost tsk]
1 < size (task_preemption_points tsk)
    rewrite EQ; clear EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
size [:: 0; task_cost tsk] <=
size (task_preemption_points tsk)
    apply subseq_leq_size.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
uniq [:: 0; task_cost tsk]
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: 0; task_cost tsk] ->
x \in task_preemption_points tsk
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
uniq [:: 0; task_cost tsk] rewrite !cons_uniq.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
[&& 0 \notin [:: task_cost tsk],
    task_cost tsk \notin [::]
  & uniq [::]]
      apply/andP; split=> [|//].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
0 \notin [:: task_cost tsk]
      rewrite in_cons negb_or; apply/andP; split=> [|//].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
0 != task_cost tsk
      by rewrite neq_ltn; apply/orP; left. 
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: 0; task_cost tsk] ->
x \in task_preemption_points tsk intros t EQ; move: EQ; rewrite !in_cons.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
[|| t == 0, t == task_cost tsk | t \in [::]] ->
t \in task_preemption_points tsk
      move => /orP[/eqP EQ | /orP[/eqP EQ|//]].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = 0
t \in task_preemption_points tsk
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = task_cost tsk
t \in task_preemption_points tsk
      +
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = 0
t \in task_preemption_points tsk rewrite EQ; clear EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
0 \in task_preemption_points tsk
        move: (BEG _ H_tsk_in_ts) => EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
EQ: first0 (task_preemption_points tsk) = 0
0 \in task_preemption_points tsk
        rewrite -EQ; clear EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
first0 (task_preemption_points tsk)
  \in task_preemption_points tsk
        rewrite /first0 -nth0.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
nth 0 (task_preemption_points tsk) 0
  \in task_preemption_points tsk
        apply/(nthP 0).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
exists2 i : nat,
  i < size (task_preemption_points tsk) &
  nth 0 (task_preemption_points tsk) i =
  nth 0 (task_preemption_points tsk) 0
        by exists 0.
      +
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
EQ: t = task_cost tsk
t \in task_preemption_points tsk rewrite EQ; clear EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
task_cost tsk \in task_preemption_points tsk
        move: (END _ H_tsk_in_ts) => EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
EQ: last0 (task_preemption_points tsk) =
task_cost tsk
task_cost tsk \in task_preemption_points tsk
        rewrite -EQ; clear EQ.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
last0 (task_preemption_points tsk)
  \in task_preemption_points tsk
        rewrite /last0 -nth_last.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
nth 0 (task_preemption_points tsk)
  (size (task_preemption_points tsk)).-1
  \in task_preemption_points tsk
        apply/(nthP 0).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
exists2 i : nat,
  i < size (task_preemption_points tsk) &
  nth 0 (task_preemption_points tsk) i =
  nth 0 (task_preemption_points tsk)
    (size (task_preemption_points tsk)).-1
        exists ((size (task_preemption_points tsk)).-1) => [|//].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
HYP1: consistent_job_segment_count arr_seq
HYP2: job_respects_segment_lengths arr_seq
HYP3: task_segments_are_nonempty ts
Fact2: 0 < size (task_preemption_points tsk)
t: Datatypes_nat__canonical__eqtype_Equality
(size (task_preemption_points tsk)).-1 <
size (task_preemption_points tsk)
        by rewrite -(leq_add2r 1) !addn1 prednK.
  Qed.

  (** Then, we prove that [task_rtct] function
      defines a valid task's run to completion threshold. *)
  Lemma limited_valid_task_run_to_completion_threshold:
    valid_task_run_to_completion_threshold arr_seq tsk.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
valid_task_run_to_completion_threshold arr_seq tsk
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
valid_task_run_to_completion_threshold arr_seq tsk
    split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
job_respects_task_rtc arr_seq tsk
    intros j ARR__j TSK__j.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
job_rtct j <= task_rtct tsk move: (H_valid_fixed_preemption_points_model) => [LJ LT].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
job_rtct j <= task_rtct tsk
    move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
job_rtct j <= task_rtct tsk
    rewrite /job_rtct /task_rtct /limited_preemptions_rtc_threshold
            /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    case: (posnP (job_cost j)) => [Z|POS]; first by rewrite Z; compute.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
      by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < task_last_nonpr_segment tsk
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    {
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < task_last_nonpr_segment tsk unfold job_respects_segment_lengths, task_last_nonpr_segment in *.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < last0 (distances (task_preemption_points tsk))
      rewrite last0_nth; apply T6; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
(size (distances (task_preemption_points tsk))).-1 <
size (distances (task_preemption_points tsk))
      have F: 1 <= size (distances (task_preemption_points tsk)).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < size (distances (task_preemption_points tsk))
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
F: 0 < size (distances (task_preemption_points tsk))
(size (distances (task_preemption_points tsk))).-1 <
size (distances (task_preemption_points tsk))
      {
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < size (distances (task_preemption_points tsk)) apply leq_trans with (size (task_preemption_points tsk) - 1).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < size (task_preemption_points tsk) - 1
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
size (task_preemption_points tsk) - 1 <=
size (distances (task_preemption_points tsk))
        -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
0 < size (task_preemption_points tsk) - 1 have F := number_of_preemption_points_in_task_at_least_two; lia.
        -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
size (task_preemption_points tsk) - 1 <=
size (distances (task_preemption_points tsk)) rewrite [in X in X - 1]size_of_seq_of_distances; [lia | apply number_of_preemption_points_in_task_at_least_two].
      }
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemptive_points j)) n <=
nth 0
  (distances
     (task_preemption_points (job_task j))) n
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
F: 0 < size (distances (task_preemption_points tsk))
(size (distances (task_preemption_points tsk))).-1 <
size (distances (task_preemption_points tsk)) lia.
    }
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    have J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
      by eapply job_last_nonpreemptive_segment_le_job_cost; eauto using valid_fixed_preemption_points_model_lemma.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    have T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
task_last_nonpr_segment tsk <= task_cost tsk
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    {
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
task_last_nonpr_segment tsk <= task_cost tsk unfold task_last_nonpr_segment.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
last0 (distances (task_preemption_points tsk)) <=
task_cost tsk rewrite -COST__task //.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
last0 (distances (task_preemption_points tsk)) <=
last0 (task_preemption_points tsk)
      eapply leq_trans; last by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
last0 (distances (task_preemption_points tsk)) <=
max0 (distances (task_preemption_points tsk))
        by apply last_of_seq_le_max_of_seq.
    }
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
job_cost j -
(last0 (distances (job_preemption_points j)) - 1) <=
task_cost tsk -
(last0 (distances (task_preemption_points tsk)) - 1)
    rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
job_cost j -
last0 (distances (job_preemption_points j)) <=
task_cost tsk -
last0 (distances (task_preemption_points tsk))
    erewrite job_parameters_last_np_to_job_limited; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
job_cost j -
last0
  [seq x <- distances (job_preemptive_points j)
     | 0 < x] <=
task_cost tsk -
last0 (distances (task_preemption_points tsk))
    rewrite distances_positive_undup//.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
job_cost j -
last0 (distances (undup (job_preemptive_points j))) <=
task_cost tsk -
last0 (distances (task_preemption_points tsk))
    have -> : job_cost j = last0 (undup (job_preemptive_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
last0 (undup (job_preemptive_points j)) -
last0 (distances (undup (job_preemptive_points j))) <=
task_cost tsk -
last0 (distances (task_preemption_points tsk))
    rewrite last_seq_minus_last_distance_seq; last by apply nondecreasing_sequence_undup, SORT__job.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
nth 0 (undup (job_preemptive_points j))
  (size (undup (job_preemptive_points j))).-2 <=
task_cost tsk -
last0 (distances (task_preemption_points tsk))
    apply leq_trans with( nth 0 (job_preemptive_points j) ((size (job_preemptive_points j)).-2)); first by apply undup_nth_le; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
nth 0 (job_preemptive_points j)
  (size (job_preemptive_points j)).-2 <=
task_cost tsk -
last0 (distances (task_preemption_points tsk))
    have -> : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
nth 0 (job_preemptive_points j)
  (size (job_preemptive_points j)).-2 <=
last0 (task_preemption_points tsk) -
last0 (distances (task_preemption_points tsk))
    rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
TSK__j: job_of_task tsk j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
nth 0 (job_preemptive_points j)
  (size (job_preemptive_points j)).-2 <=
nth 0 (task_preemption_points tsk)
  (size (task_preemption_points tsk)).-2
    move: TSK__j => /eqP TSK__j; rewrite -TSK__j.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
nth 0 (job_preemptive_points j)
  (size (job_preemptive_points j)).-2 <=
nth 0 (task_preemption_points (job_task j))
  (size (task_preemption_points (job_task j))).-2
    rewrite T4//.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
nth 0 (job_preemptive_points j)
  (size (task_preemption_points (job_task j))).-2 <=
nth 0 (task_preemption_points (job_task j))
  (size (task_preemption_points (job_task j))).-2
    apply domination_of_distances_implies_domination_of_seq; try eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
first0 (job_preemptive_points j) <=
first0 (task_preemption_points (job_task j))
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
1 < size (job_preemptive_points j)
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
1 < size (task_preemption_points (job_task j))
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
nondecreasing_sequence
  (task_preemption_points (job_task j))
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
first0 (job_preemptive_points j) <=
first0 (task_preemption_points (job_task j)) erewrite zero_is_first_element; eauto.
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
1 < size (job_preemptive_points j) eapply number_of_preemption_points_at_least_two; eauto 2.
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
1 < size (task_preemption_points (job_task j)) by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
j: Job
ARR__j: arrives_in arr_seq j
LJ: valid_limited_preemptions_job_model arr_seq
LT: valid_fixed_preemption_points_task_model arr_seq
  ts
ZERO__job: beginning_of_execution_in_preemption_points
  arr_seq
COST__job: end_of_execution_in_preemption_points
  arr_seq
SORT__job: preemption_points_is_nondecreasing_sequence
  arr_seq
ZERO__task: task_beginning_of_execution_in_preemption_points
  ts
COST__task: task_end_of_execution_in_preemption_points
  ts
SORT__task: nondecreasing_task_preemption_points ts
T4: consistent_job_segment_count arr_seq
T5: job_respects_segment_lengths arr_seq
T6: task_segments_are_nonempty ts
POS: 0 < job_cost j
J_RTCT__pos: 0 < job_last_nonpreemptive_segment j
T_RTCT__pos: 0 < task_last_nonpr_segment tsk
J_RTCT__le: job_last_nonpreemptive_segment j <=
job_cost j
T_RTCT__le: task_last_nonpr_segment tsk <=
task_cost tsk
TSK__j: job_task j = tsk
nondecreasing_sequence
  (task_preemption_points (job_task j)) by apply SORT__task; rewrite TSK__j.
  Qed.

  (** We show that the last non-preemptive segment of a task can be
      easily expressed in terms of the task cost and the task
      run-to-completion threshold. *)
  Lemma last_segment_eq_cost_minus_rtct :
    task_cost tsk - task_rtct tsk = task_last_nonpr_segment tsk - ε.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
task_cost tsk - task_rtct tsk =
task_last_nonpr_segment tsk - 1
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
task_cost tsk - task_rtct tsk =
task_last_nonpr_segment tsk - 1
    move: (H_valid_fixed_preemption_points_model) => [MLP [BEG [END [INCR _]]]].
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_cost tsk - task_rtct tsk =
task_last_nonpr_segment tsk - 1
    rewrite /task_last_nonpr_segment /task_rtct /limited_preemptions_rtc_threshold.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_cost tsk -
(task_cost tsk - (task_last_nonpr_segment tsk - 1)) =
last0 (distances (task_preemption_points tsk)) - 1
    rewrite subKn // -[leqRHS]subn0 leq_sub //.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_last_nonpr_segment tsk <= task_cost tsk
    apply leq_trans with (task_max_nonpreemptive_segment tsk).
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_last_nonpr_segment tsk <=
task_max_nonpreemptive_segment tsk
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_max_nonpreemptive_segment tsk <= task_cost tsk
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_last_nonpr_segment tsk <=
task_max_nonpreemptive_segment tsk by apply last_of_seq_le_max_of_seq.
    -
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_max_nonpreemptive_segment tsk <= task_cost tsk rewrite -END; last by done.
Task: TaskType
H: TaskCost Task
H0: TaskPreemptionPoints Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptionPoints Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
PState: ProcessorState Job
sched: schedule PState
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_job_cost: arrivals_have_valid_job_costs
  arr_seq
H_valid_fixed_preemption_points_model: valid_fixed_preemption_points_model
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_positive_cost: 0 < task_cost tsk
MLP: valid_limited_preemptions_job_model arr_seq
BEG: task_beginning_of_execution_in_preemption_points
  ts
END: task_end_of_execution_in_preemption_points ts
INCR: nondecreasing_task_preemption_points ts
task_max_nonpreemptive_segment tsk <=
last0 (task_preemption_points tsk)
      by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
  Qed.

End TaskRTCThresholdLimitedPreemptions.
Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.