Library prosa.analysis.facts.preemption.task.limited


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

Welcome to Coq 8.13.0 (January 2021)

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


Require Export prosa.analysis.facts.preemption.job.limited.

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

Platform for Models with Limited Preemptions

In this section, we prove that instantiation of functions [job_preemptable and task_preemption_points] to the limited preemptions model indeed defines a valid preemption model with bounded non-preemptive regions.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

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

In addition, we assume the existence of functions mapping a job and task to the sequence of its preemption points.
  Context `{JobPreemptionPoints Job}.
  Context `{TaskPreemptionPoints Task}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Next, consider any ideal uni-processor preemption-aware schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Consider an arbitrary task set ts.
  Variable ts : list Task.

Next, we assume that preemption points are defined by the model with fixed preemption points.
Then we prove that functions [job_preemptable and task_preemption_points] define a model with bounded non-preemptive regions.
  Lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
    model_with_bounded_nonpreemptive_segments arr_seq .

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

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

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


  Proof.
    intros j ARR.

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

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

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


    move: H_valid_fixed_preemption_points_model ⇒ [LIM FIX].

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

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

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


    move: (LIM) ⇒ [BEG [END NDEC]]; move: (FIX) ⇒ [A1 [A2 [A3 [A4 A5]]]].

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

1 subgoal (ID 125)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

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


    case: (posnP (job_cost j)) ⇒ [ZERO|POS].

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

2 subgoals (ID 148)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ZERO : job_cost j = 0
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

subgoal 2 (ID 149) is:
 job_respects_max_nonpreemptive_segment j /\
 nonpreemptive_regions_have_bounded_length j

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


    - split.

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

3 subgoals (ID 151)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ZERO : job_cost j = 0
  ============================
  job_respects_max_nonpreemptive_segment j

subgoal 2 (ID 152) is:
 nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 149) is:
 job_respects_max_nonpreemptive_segment j /\
 nonpreemptive_regions_have_bounded_length j

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


      rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.

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

3 subgoals (ID 199)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ZERO : job_cost j = 0
  ============================
  max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <=
  task_max_nonpreemptive_segment (job_task j)

subgoal 2 (ID 152) is:
 nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 149) is:
 job_respects_max_nonpreemptive_segment j /\
 nonpreemptive_regions_have_bounded_length j

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


      rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.

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

2 subgoals (ID 152)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ZERO : job_cost j = 0
  ============================
  nonpreemptive_regions_have_bounded_length j

subgoal 2 (ID 149) is:
 job_respects_max_nonpreemptive_segment j /\
 nonpreemptive_regions_have_bounded_length j

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


      + moveprogr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].

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

2 subgoals (ID 484)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ZERO : job_cost j = 0
  progr : duration
  LE : progr = 0
  ============================
  exists pp : duration,
    progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
    job_preemptable j pp

subgoal 2 (ID 149) is:
 job_respects_max_nonpreemptive_segment j /\
 nonpreemptive_regions_have_bounded_length j

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


         0; rewrite LE; split; first by apply/andP; split.

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

2 subgoals (ID 491)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  ZERO : job_cost j = 0
  progr : duration
  LE : progr = 0
  ============================
  job_preemptable j 0

subgoal 2 (ID 149) is:
 job_respects_max_nonpreemptive_segment j /\
 nonpreemptive_regions_have_bounded_length j

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


          by eapply zero_in_preemption_points; eauto 2.

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

1 subgoal (ID 149)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

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


    - split; last (moveprogr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).

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

3 subgoals (ID 526)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  ============================
  job_respects_max_nonpreemptive_segment j

subgoal 2 (ID 584) is:
 exists pp : duration,
   progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
   job_preemptable j pp
subgoal 3 (ID 585) is:
 exists pp : duration,
   progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
   job_preemptable j pp

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


      + rewrite /job_respects_max_nonpreemptive_segment
                /job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.

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

3 subgoals (ID 617)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  ============================
  max0 (distances (job_preemption_points j)) <=
  task_max_nonpreemptive_segment (job_task j)

subgoal 2 (ID 584) is:
 exists pp : duration,
   progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
   job_preemptable j pp
subgoal 3 (ID 585) is:
 exists pp : duration,
   progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
   job_preemptable j pp

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


          by apply max_of_dominating_seq; intros; apply A5.

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

2 subgoals (ID 584)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : (progr \in job_preemption_points j) = true
  ============================
  exists pp : duration,
    progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
    job_preemptable j pp

subgoal 2 (ID 585) is:
 exists pp : duration,
   progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
   job_preemptable j pp

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


      + progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
(* ----------------------------------[ coqtop ]---------------------------------

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

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


      + move: NotIN ⇒ /eqP; rewrite eqbF_neg; moveNotIN.
(* ----------------------------------[ coqtop ]---------------------------------

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

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


        edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

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

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


move: N ⇒ /andP [N1 N2].

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

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

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


        set ptl := nth 0 (job_preemption_points j) x.

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

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

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


        set ptr := nth 0 (job_preemption_points j) x.+1.

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

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

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


         ptr; split; first last.

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

2 subgoals (ID 2690)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : x.+1 < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) x.+1
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) x.+1 : nat
  ============================
  job_preemptable j ptr

subgoal 2 (ID 2689) is:
 progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)

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


        × by unfold job_preemptable, limited_preemptions_model; apply mem_nth.

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

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

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


        × apply/andP; split; first by apply ltnW.

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

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

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


          apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.

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

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

subgoal 2 (ID 2725) is:
 ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1

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


          -- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------

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

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


          -- unfold job_max_nonpreemptive_segment.

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

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

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


             rewrite -addnA -leq_subLR -(leq_add2r 1).

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

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

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


             rewrite [in X in _ X]addnC -leq_subLR.
(* ----------------------------------[ coqtop ]---------------------------------

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

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



             rewrite !subn1 !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------

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

subgoal 2 (ID 2786) is:
 0 < max0 (lengths_of_segments j)

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


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

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

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


rewrite -[_.+1.-1]pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------

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

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


rewrite /lengths_of_segments.

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

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

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


               erewrite job_parameters_max_np_to_job_limited; eauto.

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

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

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


                 by apply distance_between_neighboring_elements_le_max_distance_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 2786) is:
 0 < max0 (lengths_of_segments j)

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


}

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

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

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


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

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

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


rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.

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

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

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


               apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.

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

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

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


                0, (job_cost j); repeat split.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 9219)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : x.+1 < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) x.+1
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) x.+1 : nat
  ============================
  0 \in job_preemption_points j

subgoal 2 (ID 9223) is:
 job_cost j \in job_preemption_points j
subgoal 3 (ID 9224) is:
 0 <> job_cost j

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


               - by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 9223)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  H4 : TaskPreemptionPoints Task
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ts : seq Task
  H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
                                            arr_seq ts
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  FIX : valid_fixed_preemption_points_task_model arr_seq ts
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  A1 : task_beginning_of_execution_in_preemption_points ts
  A2 : task_end_of_execution_in_preemption_points ts
  A3 : nondecreasing_task_preemption_points ts
  A4 : consistent_job_segment_count arr_seq
  A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : x.+1 < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) x.+1
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) x.+1 : nat
  ============================
  job_cost j \in job_preemption_points j

subgoal 2 (ID 9224) is:
 0 <> job_cost j

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


               - by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------

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

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


               - by apply/eqP; rewrite eq_sym -lt0n; apply POS.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


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

No more subgoals.

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



  Qed.

Which together with lemma [valid_fixed_preemption_points_model] gives us the fact that functions [job_preemptable and task_preemption_points] defines a valid preemption model with bounded non-preemptive regions.
  Corollary fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

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

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

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


  Proof.
    split.

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

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

subgoal 2 (ID 60) is:
 model_with_bounded_nonpreemptive_segments arr_seq

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


    - by apply valid_fixed_preemption_points_model_lemma; destruct H_valid_fixed_preemption_points_model.

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

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

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


    - by apply fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.

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

No more subgoals.

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


  Qed.

End LimitedPreemptionsModel.

We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
     valid_fixed_preemption_points_model_lemma
     fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
     fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.