Library prosa.results.edf.rta.bounded_nps


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Import prosa.model.priority.edf.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.results.edf.rta.bounded_pi.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.

Throughout this file, we assume ideal uni-processor schedules.
Require Import prosa.model.processor.ideal.

Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model.
Require Import prosa.model.readiness.basic.

RTA for EDF with Bounded Non-Preemptive Segments

In this section we instantiate the Abstract RTA for EDF-schedulers with Bounded Priority Inversion to EDF-schedulers for ideal uni-processor model of real-time tasks with arbitrary arrival models _and_ bounded non-preemptive segments.
Recall that Abstract RTA for EDF-schedulers with Bounded Priority Inversion does not specify the cause of priority inversion. In this section, we prove that the priority inversion caused by execution of non-preemptive segments is bounded. Thus the Abstract RTA for EDF-schedulers is applicable to this instantiation.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.
  Context `{TaskRunToCompletionThreshold Task}.
  Context `{TaskMaxNonpreemptiveSegment Task}.

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

For clarity, let's denote the relative deadline of a task as D.
  Let D tsk := task_deadline tsk.

Consider the EDF policy that indicates a higher-or-equal priority relation. Note that we do not relate the EDF policy with the scheduler. However, we define functions for Interference and Interfering Workload that actively use the concept of priorities.
  Let EDF := EDF Job.

Consider any arrival sequence with consistent, non-duplicate arrivals.
Next, consider any ideal uni-processor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
In addition, we assume the existence of a function mapping jobs to theirs preemption points ...
  Context `{JobPreemptable Job}.

... and assume that it defines a valid preemption model with bounded non-preemptive segments.
Assume we have sequential tasks, i.e, jobs from the same task execute in the order of their arrival.
Next, we assume that the schedule is a work-conserving schedule...
... and the schedule respects the policy defined by the [job_preemptable] function (i.e., jobs have bounded non-preemptive segments).
Consider an arbitrary task set ts, ...
  Variable ts : list Task.

... assume that all jobs come from the task set, ...
... and the cost of a job cannot be larger than the task cost.
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.
Let [tsk] be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Consider a valid preemption model...
...and a valid task run-to-completion threshold function. That is, [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s cost, (2) for any job of task [tsk] job_run_to_completion_threshold is bounded by task_run_to_completion_threshold.
We introduce as an abbreviation [rbf] for the task request bound function, which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T.
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).
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 + ε) + D tsk - D tsk_o) Δ).

Let's define some local names for clarity.
We also define a bound for the priority inversion caused by jobs with lower priority.

Priority inversion is bounded

In this section, we prove that a priority inversion for task [tsk] is bounded by the maximum length of non-preemptive segments among the tasks with lower priority.
First, we prove that the maximum length of a priority inversion of job j is bounded by the maximum length of a non-preemptive section of a task with lower-priority task (i.e., the blocking term).
    Lemma priority_inversion_is_bounded_by_blocking:
       j t,
        arrives_in arr_seq j
        job_task j = tsk
        t job_arrival j
        max_length_of_priority_inversion j t blocking_bound.

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

1 subgoal (ID 1964)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  ============================
  forall (j : Job) (t : nat),
  arrives_in arr_seq j ->
  job_task j = tsk ->
  t <= job_arrival j ->
  max_length_of_priority_inversion j t <= blocking_bound

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


    Proof.
      intros j t ARR TSK LE; unfold max_length_of_priority_inversion, blocking_bound.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1971)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  priority_inversion.max_length_of_priority_inversion arr_seq j t <=
  \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
     (task_max_nonpreemptive_segment tsk_o - ε)

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


      apply leq_trans with
          (\max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
            (task_max_nonpreemptive_segment (job_task j_lp) - ε)).

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

2 subgoals (ID 1983)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  priority_inversion.max_length_of_priority_inversion arr_seq j t <=
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε)

subgoal 2 (ID 1984) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
    (task_max_nonpreemptive_segment tsk_o - ε)

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


      - apply leq_big_max.

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

2 subgoals (ID 1985)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  forall i : Job,
  i \in arrivals_between arr_seq 0 t ->
  ~~ EDF i j ->
  job_max_nonpreemptive_segment i - ε <=
  task_max_nonpreemptive_segment (job_task i) - ε

subgoal 2 (ID 1984) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
    (task_max_nonpreemptive_segment tsk_o - ε)

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


        intros j' JINB NOTHEP.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1988)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  job_max_nonpreemptive_segment j' - ε <=
  task_max_nonpreemptive_segment (job_task j') - ε

subgoal 2 (ID 1984) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
    (task_max_nonpreemptive_segment tsk_o - ε)

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



        rewrite leq_sub2r //.

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

2 subgoals (ID 1995)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  job_max_nonpreemptive_segment j' <=
  task_max_nonpreemptive_segment (job_task j')

subgoal 2 (ID 1984) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
    (task_max_nonpreemptive_segment tsk_o - ε)

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


        apply in_arrivals_implies_arrived in JINB.

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

2 subgoals (ID 2019)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : arrives_in arr_seq j'
  NOTHEP : ~~ EDF j' j
  ============================
  job_max_nonpreemptive_segment j' <=
  task_max_nonpreemptive_segment (job_task j')

subgoal 2 (ID 1984) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
    (task_max_nonpreemptive_segment tsk_o - ε)

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


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

1 subgoal (ID 1984)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
  \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
     (task_max_nonpreemptive_segment tsk_o - ε)

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


      - apply /bigmax_leq_seqP.
(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 2062)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  forall i : Job,
  i \in arrivals_between arr_seq 0 t ->
  ~~ EDF i j ->
  task_max_nonpreemptive_segment (job_task i) - ε <=
  \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
     (task_max_nonpreemptive_segment tsk_o - ε)

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


        intros j' JINB NOTHEP.

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

1 subgoal (ID 2065)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  task_max_nonpreemptive_segment (job_task j') - ε <=
  \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
     (task_max_nonpreemptive_segment tsk_o - ε)

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


        apply leq_bigmax_cond_seq with (i0 := (job_task j')) (F := fun tsktask_max_nonpreemptive_segment tsk - 1).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 2074)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  job_task j' \in ts

subgoal 2 (ID 2075) is:
 (job_task j' != tsk) && (D tsk < D (job_task j'))

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


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

1 subgoal (ID 2074)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  job_task j' \in ts

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


apply H_all_jobs_from_taskset.

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

1 subgoal (ID 2076)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  arrives_in arr_seq j'

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


          apply mem_bigcat_nat_exists in JINB.

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

1 subgoal (ID 2077)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : exists i : nat, j' \in arrivals_at arr_seq i /\ 0 <= i < t
  NOTHEP : ~~ EDF j' j
  ============================
  arrives_in arr_seq j'

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


            by inversion JINB as [ta' [JIN' _]]; ta'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2075)

subgoal 1 (ID 2075) is:
 (job_task j' != tsk) && (D tsk < D (job_task j'))

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


}

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

1 subgoal (ID 2075)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  (job_task j' != tsk) && (D tsk < D (job_task j'))

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


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

1 subgoal (ID 2075)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  (job_task j' != tsk) && (D tsk < D (job_task j'))

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


have NINTSK: job_task j' != tsk.

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

2 subgoals (ID 2098)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  job_task j' != tsk

subgoal 2 (ID 2100) is:
 (job_task j' != tsk) && (D tsk < D (job_task j'))

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


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

1 subgoal (ID 2098)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  ============================
  job_task j' != tsk

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


apply/eqP; intros TSKj'.

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

1 subgoal (ID 2140)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  TSKj' : job_task j' = tsk
  ============================
  False

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


            rewrite /EDF -ltnNge in NOTHEP.

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

1 subgoal (ID 2203)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  TSKj' : job_task j' = tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  False

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


            rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.

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

1 subgoal (ID 2267)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  TSKj' : job_task j' = tsk
  NOTHEP : job_arrival j + task_deadline (job_task j) <
           job_arrival j' + task_deadline (job_task j')
  ============================
  False

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


            rewrite TSKj' TSK ltn_add2r in NOTHEP.

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

1 subgoal (ID 2334)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  TSKj' : job_task j' = tsk
  NOTHEP : job_arrival j < job_arrival j'
  ============================
  False

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


            move: NOTHEP; rewrite ltnNge; move ⇒ /negP T; apply: T.

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

1 subgoal (ID 2372)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  TSKj' : job_task j' = tsk
  ============================
  job_arrival j' <= job_arrival j

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


            apply leq_trans with t; last by done.

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

1 subgoal (ID 2373)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  TSKj' : job_task j' = tsk
  ============================
  job_arrival j' <= t

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


            eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.

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

1 subgoal (ID 2377)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : arrived_between j' 0 t
  TSKj' : job_task j' = tsk
  ============================
  job_arrival j' <= t

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


            move: JINB; move ⇒ /andP [_ T].

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

1 subgoal (ID 2421)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  TSKj' : job_task j' = tsk
  T : job_arrival j' < t
  ============================
  job_arrival j' <= t

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


              by apply ltnW.

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

1 subgoal (ID 2100)

subgoal 1 (ID 2100) is:
 (job_task j' != tsk) && (D tsk < D (job_task j'))

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


          }

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

1 subgoal (ID 2100)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  NINTSK : job_task j' != tsk
  ============================
  (job_task j' != tsk) && (D tsk < D (job_task j'))

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


          apply/andP; split; first by done.

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

1 subgoal (ID 2449)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ EDF j' j
  NINTSK : job_task j' != tsk
  ============================
  D tsk < D (job_task j')

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


          rewrite /EDF -ltnNge in NOTHEP.

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

1 subgoal (ID 2512)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  D tsk < D (job_task j')

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


          rewrite -TSK.

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

1 subgoal (ID 2514)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  D (job_task j) < D (job_task j')

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


          have ARRLE: job_arrival j' < job_arrival j.

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

2 subgoals (ID 2519)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  job_arrival j' < job_arrival j

subgoal 2 (ID 2521) is:
 D (job_task j) < D (job_task j')

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


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

1 subgoal (ID 2519)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  job_arrival j' < job_arrival j

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


apply leq_trans with t; last by done.

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

1 subgoal (ID 2522)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  job_arrival j' < t

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


            eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.

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

1 subgoal (ID 2526)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : arrived_between j' 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ============================
  job_arrival j' < t

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


              by move: JINB; move ⇒ /andP [_ T].

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

1 subgoal (ID 2521)

subgoal 1 (ID 2521) is:
 D (job_task j) < D (job_task j')

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


          }

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

1 subgoal (ID 2521)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  NOTHEP : job_deadline j < job_deadline j'
  ARRLE : job_arrival j' < job_arrival j
  ============================
  D (job_task j) < D (job_task j')

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


          rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.

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

1 subgoal (ID 2635)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NINTSK : job_task j' != tsk
  ARRLE : job_arrival j' < job_arrival j
  NOTHEP : job_arrival j + task_deadline (job_task j) <
           job_arrival j' + task_deadline (job_task j')
  ============================
  D (job_task j) < D (job_task j')

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


          rewrite /D; ssrlia.

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

No more subgoals.

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


        }

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

No more subgoals.

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


    Qed.

Using the lemma above, we prove that the priority inversion of the task is bounded by the maximum length of a nonpreemptive section of lower-priority tasks.
    Lemma priority_inversion_is_bounded:
      priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound.

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

1 subgoal (ID 1976)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  ============================
  priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound

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


    Proof.
      movej ARR TSK POS t1 t2 PREF; move: (PREF) ⇒ [_ [_ [_ /andP [T _]]]].

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

1 subgoal (ID 2056)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      destruct (leqP (t2 - t1) blocking_bound) as [NEQ|NEQ].

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

2 subgoals (ID 2079)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

subgoal 2 (ID 2080) is:
 cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


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

1 subgoal (ID 2079)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


apply leq_trans with (t2 - t1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2081)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  cumulative_priority_inversion sched j t1 t2 <= t2 - t1

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


        rewrite /cumulative_priority_inversion /is_priority_inversion.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2088)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= t2 - t1

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


        rewrite -[X in _ X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2116)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= \sum_(t1 <= i < t2) 1

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


        rewrite leq_sum //.

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

1 subgoal (ID 2125)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  forall i : nat,
  true ->
  match sched i with
  | Some jlp => ~~ hep_job jlp j
  | None => false
  end <= 1

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


        intros t _; case: (sched t); last by done.

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

1 subgoal (ID 2161)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  t : nat
  ============================
  forall a : Job, ~~ hep_job a j <= 1

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


          by intros s; destruct (hep_job s j).

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

1 subgoal (ID 2080)

subgoal 1 (ID 2080) is:
 cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      }

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

1 subgoal (ID 2080)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      edestruct @preemption_time_exists as [ppt [PPT NEQ2]]; eauto 2 with basic_facts.

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

1 subgoal (ID 2233)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  NEQ2 : t1 <= ppt <=
         t1 +
         priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      move: NEQ2 ⇒ /andP [GE LE].

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

1 subgoal (ID 2296)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
        last apply leq_trans with (ppt - t1).

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

3 subgoals (ID 2304)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <=
  cumulative_priority_inversion sched j t1 ppt

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


      - rewrite /cumulative_priority_inversion /is_priority_inversion.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 2313)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <=
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        rewrite (@big_cat_nat _ _ _ ppt) //=; last first.

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

4 subgoals (ID 2360)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt <= t2

subgoal 2 (ID 2336) is:
 \sum_(t1 <= i < ppt)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end +
 \sum_(ppt <= i < t2)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end <=
 \sum_(t1 <= t < ppt)
    match sched t with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end
subgoal 3 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 4 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


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

1 subgoal (ID 2360)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt <= t2

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


rewrite ltn_subRL in NEQ.

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

1 subgoal (ID 2449)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  NEQ : t1 + blocking_bound < t2
  ============================
  ppt <= t2

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


          apply leq_trans with (t1 + blocking_bound); last by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2450)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  NEQ : t1 + blocking_bound < t2
  ============================
  ppt <= t1 + blocking_bound

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


          apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.

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

1 subgoal (ID 2454)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  NEQ : t1 + blocking_bound < t2
  ============================
  t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound

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


            by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 2336)

subgoal 1 (ID 2336) is:
 \sum_(t1 <= i < ppt)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end +
 \sum_(ppt <= i < t2)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end <=
 \sum_(t1 <= t < ppt)
    match sched t with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end
subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


}

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

3 subgoals (ID 2336)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= i < ppt)
     match sched i with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end +
  \sum_(ppt <= i < t2)
     match sched i with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <=
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        rewrite -[X in _ X]addn0 leq_add2l leqn0.

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

3 subgoals (ID 2486)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(ppt <= i < t2)
     match sched i with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end == 0

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        rewrite big_nat_cond big1 //; movet /andP [/andP [GEt LTt] _ ].

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

3 subgoals (ID 2611)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  ============================
  match sched t with
  | Some jlp => ~~ hep_job jlp j
  | None => false
  end = 0

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        case SCHED: (sched t) ⇒ [s | ]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 2682)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  ~~ hep_job s j = 0

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        edestruct @not_quiet_implies_exists_scheduled_hp_job
          with (K := ppt - t1) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.

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

5 subgoals (ID 2795)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  exists pr_t : instant,
    preemption_time sched pr_t /\ t1 <= pr_t <= t1 + (ppt - t1)

subgoal 2 (ID 2796) is:
 t1 + (ppt - t1) <= t < t2
subgoal 3 (ID 2810) is:
 ~~ hep_job s j = 0
subgoal 4 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 5 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


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

1 subgoal (ID 2795)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  exists pr_t : instant,
    preemption_time sched pr_t /\ t1 <= pr_t <= t1 + (ppt - t1)

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


ppt; split.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 2837)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  preemption_time sched ppt

subgoal 2 (ID 2838) is:
 t1 <= ppt <= t1 + (ppt - t1)

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


 by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2838)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  t1 <= ppt <= t1 + (ppt - t1)

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


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

4 subgoals (ID 2796)

subgoal 1 (ID 2796) is:
 t1 + (ppt - t1) <= t < t2
subgoal 2 (ID 2810) is:
 ~~ hep_job s j = 0
subgoal 3 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 4 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


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

4 subgoals (ID 2796)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  t1 + (ppt - t1) <= t < t2

subgoal 2 (ID 2810) is:
 ~~ hep_job s j = 0
subgoal 3 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 4 (ID 2307) is:
 ppt - t1 <= blocking_bound

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



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

1 subgoal (ID 2796)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  t1 + (ppt - t1) <= t < t2

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


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

3 subgoals (ID 2810)

subgoal 1 (ID 2810) is:
 ~~ hep_job s j = 0
subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


}

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

3 subgoals (ID 2810)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  ~~ hep_job s j = 0

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        apply/eqP; rewrite eqb0 Bool.negb_involutive.

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

3 subgoals (ID 3009)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  hep_job s j

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        enough (EQ : s = j_hp); first by subst.

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

3 subgoals (ID 3013)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  s = j_hp

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        move: SCHED ⇒ /eqP SCHED; rewrite -scheduled_at_def in SCHED.

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

3 subgoals (ID 3179)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s, j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  SCHED : scheduled_at sched s t
  ============================
  s = j_hp

subgoal 2 (ID 2306) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


          by eapply ideal_proc_model_is_a_uniprocessor_model; [exact SCHED | exact SCHEDHP].

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

2 subgoals (ID 2306)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 ppt <= ppt - t1

subgoal 2 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


      - rewrite /cumulative_priority_inversion /is_priority_inversion.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3190)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= ppt - t1

subgoal 2 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        rewrite -[X in _ X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3218)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= \sum_(t1 <= i < ppt) 1

subgoal 2 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        rewrite leq_sum //.

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

2 subgoals (ID 3227)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  forall i : nat,
  true ->
  match sched i with
  | Some jlp => ~~ hep_job jlp j
  | None => false
  end <= 1

subgoal 2 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


        intros t _; case: (sched t); last by done.

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

2 subgoals (ID 3263)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  ============================
  forall a : Job, ~~ hep_job a j <= 1

subgoal 2 (ID 2307) is:
 ppt - t1 <= blocking_bound

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


          by intros s; destruct (hep_job s j).

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

1 subgoal (ID 2307)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt - t1 <= blocking_bound

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


      - rewrite leq_subLR.

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

1 subgoal (ID 3280)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt <= t1 + blocking_bound

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


         apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.

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

1 subgoal (ID 3282)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  t1, t2 : instant
  PREF : busy_interval_prefix arr_seq sched j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound

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


           by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.

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

No more subgoals.

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


    Qed.

  End PriorityInversionIsBounded.

Response-Time Bound

In this section, we prove that the maximum among the solutions of the response-time bound recurrence is a response-time bound for [tsk].
  Section ResponseTimeBound.

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.

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 L A
         (F : duration),
          A + F = blocking_bound
                  + (task_rbf (A + ε) - (task_cost tsk - task_run_to_completion_threshold tsk))
                  + bound_on_total_hep_workload A (A + F)
          F + (task_cost tsk - task_run_to_completion_threshold tsk) R.

Then, using the results for the general RTA for EDF-schedulers, we establish a response-time bound for the more concrete model of bounded nonpreemptive segments. Note that in case of the general RTA for EDF-schedulers, we just _assume_ that the priority inversion is bounded. In this module we provide the preemption model with bounded nonpreemptive segments and _prove_ that the priority inversion is bounded.
    Theorem uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments:
      response_time_bounded_by tsk R.

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

1 subgoal (ID 1967)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space L A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) -
                      (task_cost tsk - task_run_to_completion_threshold tsk)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F +
                     (task_cost tsk - task_run_to_completion_threshold tsk) <=
                     R
  ============================
  response_time_bounded_by tsk R

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


    Proof.
      eapply uniprocessor_response_time_bound_edf; eauto 2.

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

1 subgoal (ID 1995)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskDeadline Task
  H1 : TaskRunToCompletionThreshold Task
  H2 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H3 : JobTask Job Task
  H4 : JobArrival Job
  H5 : JobCost Job
  D := [eta task_deadline] : Task -> duration
  EDF := edf.EDF Job : JLFP_policy 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
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H6 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq 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
  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
  H7 : 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
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  rbf := task_request_bound_function : Task -> duration -> nat
  task_rbf := rbf tsk : duration -> nat
  total_rbf := total_request_bound_function ts : duration -> nat
  bound_on_total_hep_workload := fun A Δ : nat =>
                                 \sum_(tsk_o <- ts | 
                                 tsk_o != tsk)
                                    rbf tsk_o
                                      (minn (A + ε + D tsk - D tsk_o) Δ)
   : nat -> nat -> nat
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta bounded_pi.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := bounded_pi.bound_on_total_hep_workload_changes_at
                                              ts tsk : 
  nat -> bool
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  is_in_search_space := bounded_pi.is_in_search_space ts tsk
   : duration -> duration -> bool
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space L A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) -
                      (task_cost tsk - task_run_to_completion_threshold tsk)) +
                     bound_on_total_hep_workload A (A + F) /\
                     F +
                     (task_cost tsk - task_run_to_completion_threshold tsk) <=
                     R
  ============================
  priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound

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


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

No more subgoals.

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


    Qed.

  End ResponseTimeBound.

End RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.