Library prosa.analysis.facts.preemption.task.floating


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

Welcome to Coq 8.11.2 (June 2020)

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


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

Furthermore, we assume the task model with floating non-preemptive regions.

Platform for Floating Non-Preemptive Regions Model

In this section, we prove that instantiation of functions [job_preemptable and task_max_nonpreemptive_segment] to the model with floating non-preemptive regions 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 a function mapping a task to its maximal non-preemptive segment ...
.. and the existence of functions mapping a job to the sequence of its preemption points.
  Context `{JobPreemptionPoints Job}.

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.
Next, we assume that preemption points are defined by the model with floating non-preemptive regions.
Then, we prove that the [job_preemptable and task_max_nonpreemptive_segment] functions define a model with bounded non-preemptive regions.
  Lemma floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
    model_with_bounded_nonpreemptive_segments arr_seq.

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

1 subgoal (ID 658)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  ============================
  model_with_bounded_nonpreemptive_segments arr_seq

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


  Proof.
    intros j ARR.

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

1 subgoal (ID 661)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

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


    move: (H_valid_model_with_floating_nonpreemptive_regions) ⇒ LIM; move: LIM (LIM) ⇒ [LIM L] [[BEG [END NDEC]] MAX].

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

1 subgoal (ID 708)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

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


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

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

2 subgoals (ID 731)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ZERO : job_cost j = 0
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

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

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


    - split.

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

3 subgoals (ID 734)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ZERO : job_cost j = 0
  ============================
  job_respects_max_nonpreemptive_segment j

subgoal 2 (ID 735) is:
 nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 732) 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 783)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ZERO : job_cost j = 0
  ============================
  max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <=
  task_max_nonpreemptive_segment (job_task j)

subgoal 2 (ID 735) is:
 nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 732) 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 735)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ZERO : job_cost j = 0
  ============================
  nonpreemptive_regions_have_bounded_length j

subgoal 2 (ID 732) 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 1062)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ZERO : job_cost j = 0
  progr : duration
  LE : progr = 0
  ============================
  exists pp : duration,
    progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
    job_preemptable j pp

subgoal 2 (ID 732) 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 1069)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  ZERO : job_cost j = 0
  progr : duration
  LE : progr = 0
  ============================
  job_preemptable j 0

subgoal 2 (ID 732) 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 732)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  ============================
  job_respects_max_nonpreemptive_segment j /\
  nonpreemptive_regions_have_bounded_length j

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


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

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

3 subgoals (ID 1104)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  ============================
  job_respects_max_nonpreemptive_segment j

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

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


      + by apply MAX.

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

2 subgoals (ID 1163)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : (progr \in job_preemption_points j) = true
  ============================
  exists pp : duration,
    progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
    job_preemptable j pp

subgoal 2 (ID 1164) 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 1164)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : (progr \in job_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 1271)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_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 1296)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N : nth 0 (job_preemption_points j) x < progr <
      nth 0 (job_preemption_points j) (succn x)
  ============================
  exists pp : duration,
    progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
    job_preemptable j pp

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


move: N ⇒ /andP [N1 N2].

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

1 subgoal (ID 1358)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ============================
  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 1363)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  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 1368)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  exists pp : duration,
    progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
    job_preemptable j pp

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


         ptr; split; first last.

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

2 subgoals (ID 1373)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  job_preemptable j ptr

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

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


        × by unfold job_preemptable, limited_preemptions_model; apply mem_nth.

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

1 subgoal (ID 1372)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)

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


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

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

1 subgoal (ID 1403)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : 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 1410)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptl + (job_max_nonpreemptive_segment j - ε) + 1 <=
  progr + (job_max_nonpreemptive_segment j - ε)

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

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


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

1 subgoal (ID 1409)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1

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


          -- unfold job_max_nonpreemptive_segment.

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

1 subgoal (ID 1420)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr <= ptl + (max0 (lengths_of_segments j) - ε) + 1

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


             rewrite -addnA -leq_subLR -(leq_add2r 1).

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

1 subgoal (ID 1436)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr - ptl + 1 <= max0 (lengths_of_segments j) - ε + 1 + 1

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


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

1 subgoal (ID 1452)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr - ptl + 1 - 1 <= max0 (lengths_of_segments j) - ε + 1

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



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

2 subgoals (ID 1470)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  predn (succn (ptr - ptl)) <= max0 (lengths_of_segments j)

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

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


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

1 subgoal (ID 1470)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  predn (succn (ptr - ptl)) <= max0 (lengths_of_segments j)

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


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

1 subgoal (ID 1475)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr - ptl <= max0 (lengths_of_segments j)

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


rewrite /lengths_of_segments.

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

1 subgoal (ID 1482)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr - ptl <= max0 (distances (parameter.job_preemption_points j))

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


               erewrite job_parameters_max_np_to_job_limited; eauto.

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

1 subgoal (ID 1487)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  ptr - ptl <= max0 (distances (job_preemption_points j))

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


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

1 subgoal (ID 1471)

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

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


}

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

1 subgoal (ID 1471)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  0 < max0 (lengths_of_segments j)

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


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

1 subgoal (ID 1471)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  0 < max0 (lengths_of_segments j)

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


rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.

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

1 subgoal (ID 3570)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  0 < max0 (distances (job_preemption_points j))

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


               apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.

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

1 subgoal (ID 7919)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : 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 7928)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  0 \in job_preemption_points j

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

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


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

2 subgoals (ID 7932)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : nat
  ============================
  job_cost j \in job_preemption_points j

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

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


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

1 subgoal (ID 7933)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  LIM : valid_limited_preemptions_job_model arr_seq
  L : job_respects_task_max_np_segment arr_seq
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  MAX : job_respects_task_max_np_segment arr_seq
  POS : 0 < job_cost j
  progr : duration
  LE : progr <= job_cost j
  NotIN : progr \notin job_preemption_points j
  x : nat
  SIZE2 : succn x < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) x < progr
  N2 : progr < nth 0 (job_preemption_points j) (succn x)
  ptl := nth 0 (job_preemption_points j) x : nat
  ptr := nth 0 (job_preemption_points j) (succn x) : 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_max_nonpreemptive_segment] define a valid preemption model with bounded non-preemptive regions.
  Corollary floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

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

1 subgoal (ID 668)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  ============================
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched

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


  Proof.
    split.

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

2 subgoals (ID 670)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  ============================
  valid_preemption_model arr_seq sched

subgoal 2 (ID 671) is:
 model_with_bounded_nonpreemptive_segments arr_seq

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


    - apply valid_fixed_preemption_points_model_lemma; auto.

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

2 subgoals (ID 676)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  ============================
  valid_limited_preemptions_job_model arr_seq

subgoal 2 (ID 671) is:
 model_with_bounded_nonpreemptive_segments arr_seq

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


        by apply H_valid_model_with_floating_nonpreemptive_regions.

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

1 subgoal (ID 671)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : TaskMaxNonpreemptiveSegment Task
  H4 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
                                  sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_model_with_floating_nonpreemptive_regions : 
  valid_model_with_floating_nonpreemptive_regions arr_seq
  ============================
  model_with_bounded_nonpreemptive_segments arr_seq

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


    - apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.

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

No more subgoals.

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


  Qed.

End FloatingNonPreemptiveRegionsModel.

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