Library prosa.results.edf.rta.limited_preemptive


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

RTA for EDF with Fixed Preemption Points

In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points.
Throughout this file, we assume the EDF priority policy, ideal uni-processor schedules, and the basic (i.e., Liu & Layland) readiness model.
Require Import prosa.model.priority.edf.
Require Import prosa.model.processor.ideal.
Require Import prosa.model.readiness.basic.

Furthermore, we assume the task model with fixed preemption points.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.limited_preemptive.

Setup and Assumptions


Section RTAforFixedPreemptionPointsModelwithArrivalCurves.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.

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

Consider any arrival sequence with consistent, non-duplicate arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.

Consider an arbitrary task set ts, ...
  Variable ts : list Task.

... assume that all jobs come from this task set, ...
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

... and the cost of a job cannot be larger than the task cost.
  Hypothesis H_valid_job_cost:
    arrivals_have_valid_job_costs arr_seq.

Next, we assume we have the model with fixed preemption points. I.e., each task is divided into a number of non-preemptive segments by inserting statically predefined preemption points.
  Context `{JobPreemptionPoints Job}.
  Context `{TaskPreemptionPoints Task}.
  Hypothesis H_valid_model_with_fixed_preemption_points:
    valid_fixed_preemption_points_model arr_seq ts.

Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
  Context `{MaxArrivals Task}.
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

Let [tsk] be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Next, consider any ideal uni-processor schedule with limited preemptions of this arrival sequence ...
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.
  Hypothesis H_schedule_with_limited_preemptions:
    schedule_respects_preemption_model arr_seq sched.

... where jobs do not execute before their arrival or after completion.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Assume we have sequential tasks, i.e, jobs from the same task execute in the order of their arrival.
  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.

Next, we assume that the schedule is a work-conserving schedule...
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

... and the schedule respects the policy defined by the [job_preemptable] function (i.e., jobs have bounded non-preemptive segments).
  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.

Total Workload and Length of Busy Interval

We introduce the abbreviation [rbf] for the task request bound function, which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T.
  Let rbf := task_request_bound_function.

Next, we introduce [task_rbf] as an abbreviation for the task request bound function of task [tsk].
  Let task_rbf := rbf tsk.

Using the sum of individual request bound functions, we define the request bound function of all tasks (total request bound function).
  Let total_rbf := total_request_bound_function ts.

We define a bound for the priority inversion caused by jobs with lower priority.
  Let blocking_bound :=
    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
     (task_max_nonpreemptive_segment tsk_other - ε).

Next, we define an upper bound on interfering workload received from jobs of other tasks with higher-than-or-equal priority.
  Let bound_on_total_hep_workload A Δ :=
    \sum_(tsk_o <- ts | tsk_o != tsk)
     rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).

Let L be any positive fixed point of the busy interval recurrence.
  Variable L : duration.
  Hypothesis H_L_positive : L > 0.
  Hypothesis H_fixed_point : L = total_rbf L.

Response-Time Bound

To reduce the time complexity of the analysis, recall the notion of search space.
  Let is_in_search_space := is_in_search_space ts tsk L.

Consider any value R, and assume that for any given arrival offset A in the search space, there is a solution of the response-time bound recurrence which is bounded by R.
  Variable R : duration.
  Hypothesis H_R_is_maximum:
    ∀ (A : duration),
      is_in_search_space A →
      ∃ (F : duration),
        A + F = blocking_bound
                + (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε))
                + bound_on_total_hep_workload A (A + F) ∧
        F + (task_last_nonpr_segment tsk - ε) ≤ R.

Now, we can leverage the results for the abstract model with bounded non-preemptive segments to establish a response-time bound for the more concrete model of fixed preemption points.

  Let response_time_bounded_by := task_response_time_bound arr_seq sched.

  Theorem uniprocessor_response_time_bound_edf_with_fixed_preemption_points:
    response_time_bounded_by tsk R.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2205)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  ============================
  response_time_bounded_by tsk R

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


  Proof.
    move: (H_valid_model_with_fixed_preemption_points) ⇒ [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].

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

1 subgoal (ID 2267)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  ============================
  response_time_bounded_by tsk R

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

    move: (MLP) ⇒ [BEGj [ENDj _]].

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

1 subgoal (ID 2290)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  ============================
  response_time_bounded_by tsk R

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

    case: (posnP (task_cost tsk)) ⇒ [ZERO|POSt].

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

2 subgoals (ID 2313)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  ZERO : task_cost tsk = 0
  ============================
  response_time_bounded_by tsk R

subgoal 2 (ID 2314) is:
 response_time_bounded_by tsk R

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

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

1 subgoal (ID 2313)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  ZERO : task_cost tsk = 0
  ============================
  response_time_bounded_by tsk R

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

intros j ARR TSK.

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

1 subgoal (ID 2318)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  ZERO : task_cost tsk = 0
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_response_time_bound sched j R

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

      move: (H_valid_job_cost _ ARR) ⇒ POSt.

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

1 subgoal (ID 2322)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  ZERO : task_cost tsk = 0
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POSt : valid_job_cost j
  ============================
  job_response_time_bound sched j R

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

      move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move ⇒ /eqP Z.

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

1 subgoal (ID 2376)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  ZERO : task_cost tsk = 0
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  Z : job_cost j = 0
  ============================
  job_response_time_bound sched j R

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

        by rewrite /job_response_time_bound /completed_by Z.

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

1 subgoal (ID 2314)

subgoal 1 (ID 2314) is:
 response_time_bounded_by tsk R

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

    }

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

1 subgoal (ID 2314)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  response_time_bounded_by tsk R

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

    eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).

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

19 focused subgoals
(shelved: 1) (ID 2409)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  consistent_arrival_times arr_seq

subgoal 2 (ID 2410) is:
 arrival_sequence_uniq arr_seq
subgoal 3 (ID 2411) is:
 jobs_come_from_arrival_sequence sched arr_seq
subgoal 4 (ID 2412) is:
 jobs_must_arrive_to_execute sched
subgoal 5 (ID 2413) is:
 completed_jobs_dont_execute sched
subgoal 6 (ID 2414) is:
 valid_model_with_bounded_nonpreemptive_segments arr_seq sched
subgoal 7 (ID 2415) is:
 sequential_tasks arr_seq sched
subgoal 8 (ID 2416) is:
 work_conserving arr_seq sched
subgoal 9 (ID 2417) is:
 respects_policy_at_preemption_point arr_seq sched
subgoal 10 (ID 2418) is:
 all_jobs_from_taskset arr_seq ?ts0
subgoal 11 (ID 2419) is:
 arrivals_have_valid_job_costs arr_seq
subgoal 12 (ID 2420) is:
 valid_taskset_arrival_curve ?ts0 max_arrivals
subgoal 13 (ID 2421) is:
 taskset_respects_max_arrivals arr_seq ?ts0
subgoal 14 (ID 2422) is:
 tsk \in ?ts0
subgoal 15 (ID 2423) is:
 valid_preemption_model arr_seq sched
subgoal 16 (ID 2424) is:
 valid_task_run_to_completion_threshold arr_seq tsk
subgoal 17 (ID 2425) is:
 0 < L
subgoal 18 (ID 2426) is:
 L = total_request_bound_function ?ts0 L
subgoal 19 (ID 2427) is:
 forall A : duration,
 bounded_pi.is_in_search_space ?ts0 tsk L A ->
 exists F : duration,
   A + F =
   bounded_nps.blocking_bound ?ts0 tsk +
   (task_request_bound_function tsk (A + ε) - (task_cost tsk - task_rtct tsk)) +
   \sum_(tsk_o <- ?ts0 | tsk_o != tsk)
      task_request_bound_function tsk_o
        (minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
   F + (task_cost tsk - task_rtct tsk) <= R

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

    all: eauto 2 with basic_facts.

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

1 subgoal (ID 2427)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  forall A : duration,
  bounded_pi.is_in_search_space ts tsk L A ->
  exists F : duration,
    A + F =
    bounded_nps.blocking_bound ts tsk +
    (task_request_bound_function tsk (A + ε) -
     (task_cost tsk - task_rtct tsk)) +
    \sum_(tsk_o <- ts | tsk_o != tsk)
       task_request_bound_function tsk_o
         (minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
    F + (task_cost tsk - task_rtct tsk) <= R

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

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

1 subgoal (ID 2427)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  forall A : duration,
  bounded_pi.is_in_search_space ts tsk L A ->
  exists F : duration,
    A + F =
    bounded_nps.blocking_bound ts tsk +
    (task_request_bound_function tsk (A + ε) -
     (task_cost tsk - task_rtct tsk)) +
    \sum_(tsk_o <- ts | tsk_o != tsk)
       task_request_bound_function tsk_o
         (minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
    F + (task_cost tsk - task_rtct tsk) <= R

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

rewrite subKn; first by done.

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

1 subgoal (ID 2469)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  task_last_nonpr_segment tsk - ε <= task_cost tsk

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

      rewrite /task_last_nonpr_segment -(leq_add2r 1) subn1 !addn1 prednK; last first.

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

2 subgoals (ID 2493)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  0 < last0 (distances (task_preemption_points tsk))

subgoal 2 (ID 2492) is:
 last0 (distances (task_preemption_points tsk)) <= succn (task_cost tsk)

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

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

1 subgoal (ID 2493)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  0 < last0 (distances (task_preemption_points tsk))

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

 rewrite /last0 -nth_last.

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

1 subgoal (ID 2499)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  0 <
  nth 0 (distances (task_preemption_points tsk))
    (predn (size (distances (task_preemption_points tsk))))

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

        apply HYP3; try by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2501)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  predn (size (distances (task_preemption_points tsk))) <
  size (distances (task_preemption_points tsk))

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

        rewrite -(ltn_add2r 1) !addn1 prednK //.

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

1 subgoal (ID 2539)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  0 < size (distances (task_preemption_points tsk))

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

        move: (number_of_preemption_points_in_task_at_least_two
                 _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) ⇒ Fact2.

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

1 subgoal (ID 2576)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  Fact2 : 1 < size (task_preemption_points tsk)
  ============================
  0 < size (distances (task_preemption_points tsk))

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

        move: (Fact2) ⇒ Fact3.

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

1 subgoal (ID 2578)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  Fact2, Fact3 : 1 < size (task_preemption_points tsk)
  ============================
  0 < size (distances (task_preemption_points tsk))

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

          by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.

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

1 subgoal (ID 2492)

subgoal 1 (ID 2492) is:
 last0 (distances (task_preemption_points tsk)) <= succn (task_cost tsk)

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

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

1 subgoal (ID 2492)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  last0 (distances (task_preemption_points tsk)) <= succn (task_cost tsk)

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

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

1 subgoal (ID 2492)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  last0 (distances (task_preemption_points tsk)) <= succn (task_cost tsk)

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

apply leq_trans with (task_max_nonpreemptive_segment tsk).

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

2 subgoals (ID 2623)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  last0 (distances (task_preemption_points tsk)) <=
  task_max_nonpreemptive_segment tsk

subgoal 2 (ID 2624) is:
 task_max_nonpreemptive_segment tsk <= succn (task_cost tsk)

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

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

1 subgoal (ID 2624)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  task_max_nonpreemptive_segment tsk <= succn (task_cost tsk)

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

        - rewrite -END; last by done.

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

1 subgoal (ID 2630)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  task_max_nonpreemptive_segment tsk <=
  succn (last0 (task_preemption_points tsk))

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

          apply ltnW; rewrite ltnS; try done.

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

1 subgoal (ID 2636)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  ts : seq Task
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H4 : JobPreemptionPoints Job
  H5 : TaskPreemptionPoints Task
  H_valid_model_with_fixed_preemption_points : valid_fixed_preemption_points_model
                                                 arr_seq ts
  H6 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_schedule_with_limited_preemptions : schedule_respects_preemption_model
                                          arr_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_sequential_tasks : sequential_tasks arr_seq sched
  H_work_conserving : work_conserving arr_seq sched
  H_respects_policy : respects_policy_at_preemption_point arr_seq sched
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  blocking_bound := \max_(tsk_other <- ts | (tsk_other != tsk) &&
                                            (task_deadline tsk <
                                             task_deadline tsk_other))
                       (task_max_nonpreemptive_segment tsk_other - ε) : nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn
                                         (A + ε + task_deadline tsk -
                                          task_deadline tsk_o) Δ)
   : nat -> nat -> nat
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := bounded_pi.is_in_search_space ts tsk L
   : duration -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F + (task_last_nonpr_segment tsk - ε) <= R
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  MLP : valid_limited_preemptions_job_model arr_seq
  BEG : task_beginning_of_execution_in_preemption_points ts
  END : task_end_of_execution_in_preemption_points ts
  INCR : nondecreasing_task_preemption_points ts
  HYP1 : consistent_job_segment_count arr_seq
  HYP2 : job_respects_segment_lengths arr_seq
  HYP3 : task_segments_are_nonempty ts
  BEGj : beginning_of_execution_in_preemption_points arr_seq
  ENDj : end_of_execution_in_preemption_points arr_seq
  POSt : 0 < task_cost tsk
  ============================
  task_max_nonpreemptive_segment tsk <= last0 (task_preemption_points tsk)

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

            by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

      }

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

No more subgoals.

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

    }

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

No more subgoals.

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

  Qed.

End RTAforFixedPreemptionPointsModelwithArrivalCurves.