Library prosa.analysis.facts.preemption.rtc_threshold.limited


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.analysis.facts.preemption.task.limited.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.

Furthermore, we assume the task model with fixed preemption points.

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.
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}.

Consider any arrival sequence with consistent arrivals.
Next, consider any ideal uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Consider an arbitrary task set ts.
  Variable ts : seq Task.

Assume that a job cost cannot be larger than a task cost.
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.
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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 968)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.
    move: (H_valid_fixed_preemption_points_model) ⇒ [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1030)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1034)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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)

subgoal 2 (ID 1036) is:
 1 < size (task_preemption_points tsk)

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1034)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1175)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1179)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1194)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 intros; move: (H_positive_cost); rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1036)

subgoal 1 (ID 1036) is:
 1 < size (task_preemption_points tsk)

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1036)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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]; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1244)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1247)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1249)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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]

subgoal 2 (ID 1250) is:
 forall x : nat_eqType,
 x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


    rewrite !cons_uniq.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1260)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 [::]]

subgoal 2 (ID 1250) is:
 forall x : nat_eqType,
 x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1260)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1289)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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]

subgoal 2 (ID 1290) is:
 (task_cost tsk \notin [::]) && uniq [::]

----------------------------------------------------------------------------- *)


      rewrite in_cons negb_or; apply/andP; split; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1326)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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

subgoal 2 (ID 1290) is:
 (task_cost tsk \notin [::]) && uniq [::]

----------------------------------------------------------------------------- *)


      rewrite neq_ltn; apply/orP; left; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1290)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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)
  ============================
  (task_cost tsk \notin [::]) && uniq [::]

----------------------------------------------------------------------------- *)


      apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1250)

subgoal 1 (ID 1250) is:
 forall x : nat_eqType,
 x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


}
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1250)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType,
  x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk

----------------------------------------------------------------------------- *)



    intros t EQ; move: EQ; rewrite !in_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1405)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  [|| t == 0, t == task_cost tsk | t \in [::]] ->
  t \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


    move ⇒ /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1557)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  EQ : t = 0
  ============================
  t \in task_preemption_points tsk

subgoal 2 (ID 1558) is:
 t \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1557)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  EQ : t = 0
  ============================
  t \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


rewrite EQ; clear EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1584)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  0 \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      move: (BEG _ H_tsk_in_ts) ⇒ EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1588)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  EQ : first0 (task_preemption_points tsk) = 0
  ============================
  0 \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      rewrite -EQ; clear EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1591)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  first0 (task_preemption_points tsk) \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      rewrite /first0 -nth0.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1597)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  nth 0 (task_preemption_points tsk) 0 \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      apply/(nthP 0).

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1625)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  exists2 i : nat,
    i < size (task_preemption_points tsk) &
    nth 0 (task_preemption_points tsk) i =
    nth 0 (task_preemption_points tsk) 0

----------------------------------------------------------------------------- *)


       0; by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1558)

subgoal 1 (ID 1558) is:
 t \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1558)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  EQ : t = task_cost tsk
  ============================
  t \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1558)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  EQ : t = task_cost tsk
  ============================
  t \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


rewrite EQ; clear EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1631)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  task_cost tsk \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      move: (END _ H_tsk_in_ts) ⇒ EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1635)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  EQ : last0 (task_preemption_points tsk) = task_cost tsk
  ============================
  task_cost tsk \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      rewrite -EQ; clear EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1638)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  last0 (task_preemption_points tsk) \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      rewrite /last0 -nth_last.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1644)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  nth 0 (task_preemption_points tsk)
    (predn (size (task_preemption_points tsk)))
    \in task_preemption_points tsk

----------------------------------------------------------------------------- *)


      apply/(nthP 0).

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1672)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  exists2 i : nat,
    i < size (task_preemption_points tsk) &
    nth 0 (task_preemption_points tsk) i =
    nth 0 (task_preemption_points tsk)
      (predn (size (task_preemption_points tsk)))

----------------------------------------------------------------------------- *)


       ((size (task_preemption_points tsk)).-1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1677)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 : nat_eqType
  ============================
  predn (size (task_preemption_points tsk)) <
  size (task_preemption_points tsk)

----------------------------------------------------------------------------- *)


        by rewrite -(leq_add2r 1) !addn1 prednK //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Then, we prove that [task_run_to_completion_threshold] 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 979)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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.
    split; first by rewrite /task_rtc_bounded_by_cost leq_subr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 982)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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 ? ARR__j TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 997)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  ============================
  job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk

----------------------------------------------------------------------------- *)


move: (H_valid_fixed_preemption_points_model) ⇒ [LJ LT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1009)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  LJ : valid_limited_preemptions_job_model arr_seq
  LT : valid_fixed_preemption_points_task_model arr_seq ts
  ============================
  job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk

----------------------------------------------------------------------------- *)


    move: (LJ) (LT) ⇒ [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1083)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_run_to_completion_threshold j <= task_run_to_completion_threshold tsk

----------------------------------------------------------------------------- *)


    rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions
            /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1121)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) - ε) <=
  task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    case: (posnP (job_cost j)) ⇒ [Z|POS]; first by rewrite Z; compute.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1145)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) - ε) <=
  task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1179)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) - ε) <=
  task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1182)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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

subgoal 2 (ID 1184) is:
 job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
 task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1182)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 ×.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1186)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1191)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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
  ============================
  predn (size (distances (task_preemption_points tsk))) <
  size (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


      have F: 1 size (distances (task_preemption_points tsk)).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1208)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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))

subgoal 2 (ID 1210) is:
 predn (size (distances (task_preemption_points tsk))) <
 size (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1208)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1214)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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

subgoal 2 (ID 1215) is:
 size (task_preemption_points tsk) - 1 <=
 size (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


        - have F := number_of_preemption_points_in_task_at_least_two; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1215)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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; [ssrlia | apply number_of_preemption_points_in_task_at_least_two].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1210)

subgoal 1 (ID 1210) is:
 predn (size (distances (task_preemption_points tsk))) <
 size (distances (task_preemption_points tsk))
subgoal 2 (ID 1184) is:
 job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
 task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


      }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1210)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_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))
  ============================
  predn (size (distances (task_preemption_points tsk))) <
  size (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1184)

subgoal 1 (ID 1184) is:
 job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
 task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1184)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) - ε) <=
  task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


   
    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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2020)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) - ε) <=
  task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    have T_RTCT__le : task_last_nonpr_segment tsk task_cost tsk.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 2025)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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

subgoal 2 (ID 2027) is:
 job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
 task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2025)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2029)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2035)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2060)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2027)

subgoal 1 (ID 2027) is:
 job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
 task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2027)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) - ε) <=
  task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)

----------------------------------------------------------------------------- *)



    rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2192)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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 (parameter.job_preemption_points j)) <=
  task_cost tsk - last0 (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


    erewrite job_parameters_last_np_to_job_limited; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2197)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j) | 0 < x] <=
  task_cost tsk - last0 (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


    rewrite distances_positive_undup //; last by apply SORT__job.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2223)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j))) <=
  task_cost tsk - last0 (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


    have → : job_cost j = last0 (undup (job_preemption_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2298)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j)) -
  last0 (distances (undup (job_preemption_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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2302)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j))
    (predn (predn (size (undup (job_preemption_points j))))) <=
  task_cost tsk - last0 (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


    apply leq_trans with( nth 0 (job_preemption_points j) ((size (job_preemption_points j)).-2)); first by apply undup_nth_le; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2313)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j)
    (predn (predn (size (job_preemption_points j)))) <=
  task_cost tsk - last0 (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


    have → : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2334)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j)
    (predn (predn (size (job_preemption_points j)))) <=
  last0 (task_preemption_points tsk) -
  last0 (distances (task_preemption_points tsk))

----------------------------------------------------------------------------- *)


    rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2338)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j)
    (predn (predn (size (job_preemption_points j)))) <=
  nth 0 (task_preemption_points tsk)
    (predn (predn (size (task_preemption_points tsk))))

----------------------------------------------------------------------------- *)


    rewrite -TSK__j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2342)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j)
    (predn (predn (size (job_preemption_points j)))) <=
  nth 0 (task_preemption_points (job_task j))
    (predn (predn (size (task_preemption_points (job_task j)))))

----------------------------------------------------------------------------- *)


    rewrite T4; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2348)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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_preemption_points j)
    (predn (predn (size (task_preemption_points (job_task j))))) <=
  nth 0 (task_preemption_points (job_task j))
    (predn (predn (size (task_preemption_points (job_task j)))))

----------------------------------------------------------------------------- *)


    apply domination_of_distances_implies_domination_of_seq; try eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 2350)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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
  ============================
  first0 (job_preemption_points j) <=
  first0 (task_preemption_points (job_task j))

subgoal 2 (ID 2351) is:
 1 < size (job_preemption_points j)
subgoal 3 (ID 2352) is:
 1 < size (task_preemption_points (job_task j))
subgoal 4 (ID 2355) is:
 nondecreasing_sequence (task_preemption_points (job_task j))

----------------------------------------------------------------------------- *)


    - erewrite zero_is_first_element; eauto.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 2351)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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
  ============================
  1 < size (job_preemption_points j)

subgoal 2 (ID 2352) is:
 1 < size (task_preemption_points (job_task j))
subgoal 3 (ID 2355) is:
 nondecreasing_sequence (task_preemption_points (job_task j))

----------------------------------------------------------------------------- *)


    - eapply number_of_preemption_points_at_least_two; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 2352)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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
  ============================
  1 < size (task_preemption_points (job_task j))

subgoal 2 (ID 2355) is:
 nondecreasing_sequence (task_preemption_points (job_task j))

----------------------------------------------------------------------------- *)


    - by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2355)
  
  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
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_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_task j = tsk
  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
  ============================
  nondecreasing_sequence (task_preemption_points (job_task j))

----------------------------------------------------------------------------- *)



    - by apply SORT__task; rewrite TSK__j.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End TaskRTCThresholdLimitedPreemptions.
Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.