Library rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound


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

Welcome to Coq 8.10.1 (October 2019)

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


From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model.preemption Require Import valid_model
     job.parameters task.parameters rtc_threshold.valid_rtct.
From rt.restructuring.analysis.basic_facts.preemption Require Import
     rtc_threshold.job_preemptable.
From rt.restructuring.analysis.facts Require Import priority_inversion_is_bounded.
From rt.restructuring.model.schedule Require Import
     work_conserving priority_based.priorities priority_based.edf priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis.edf Require Export rta.response_time_bound.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

RTA for EDF-schedulers with Bounded Non-Preemprive 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-preemprive 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 Task Job.

Consider any arrival sequence with consistent, non-duplicate arrivals.
Next, consider any ideal uniprocessor 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 maping jobs to theirs preemption points ...
  Context `{JobPreemptable Job}.

... and assume that it defines a valid preemption model with bounded nonpreemptive 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 thejob_preemptable function (i.e., jobs have bounded nonpreemptive 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 nonpreemtive 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 nonpreemptive 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 306)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  ============================
  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 313)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq EDF
    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 325)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  j : Job
  t : nat
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  LE : t <= job_arrival j
  ============================
  priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq EDF
    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 326) 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 327)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 326) 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 330)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 326) 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 337)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 326) 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 361)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 326) 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 326)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 404)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 407)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 416)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 417) is:
 (job_task j' != tsk) && (D tsk < D (job_task j'))

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


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

1 subgoal (ID 416)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 418)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 419)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 417)

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

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


}

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

1 subgoal (ID 417)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 417)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 440)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 442) is:
 (job_task j' != tsk) && (D tsk < D (job_task j'))

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


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

1 subgoal (ID 440)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 482)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 544)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 /job_deadline.job_deadline_from_task_deadline in NOTHEP.

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

1 subgoal (ID 607)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 673)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 711)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 712)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 716)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 760)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 442)

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

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


          }

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

1 subgoal (ID 442)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 788)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 850)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 852)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 857)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 859) is:
 D (job_task j) < D (job_task j')

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


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

1 subgoal (ID 857)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 860)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 864)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 859)

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

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


          }

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

1 subgoal (ID 859)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 /job_deadline.job_deadline_from_task_deadline in NOTHEP.

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

1 subgoal (ID 972)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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; ssromega.

(* ----------------------------------[ 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 321)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  ============================
  priority_inversion_is_bounded_by arr_seq sched (edf.EDF Task Job) tsk
    blocking_bound

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


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

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

1 subgoal (ID 401)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
  blocking_bound

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


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

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

2 subgoals (ID 424)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
  blocking_bound

subgoal 2 (ID 425) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
 blocking_bound

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


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

1 subgoal (ID 424)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
  blocking_bound

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


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

1 subgoal (ID 426)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <= t2 - t1

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


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

1 subgoal (ID 433)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ edf.EDF Task 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 461)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end <= \sum_(t1 <= i < t2) 1

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


        rewrite leq_sum //.

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

1 subgoal (ID 470)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  ============================
  forall i : nat,
  true ->
  match sched i with
  | Some jlp => ~~ edf.EDF Task Job jlp j
  | None => false
  end <= 1

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


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

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

1 subgoal (ID 506)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : t2 - t1 <= blocking_bound
  t : nat
  ============================
  forall a : Job, ~~ edf.EDF Task Job a j <= 1

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


          by intros s; case: edf.EDF.

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

1 subgoal (ID 425)

subgoal 1 (ID 425) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
 blocking_bound

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


      }

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

1 subgoal (ID 425)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
  blocking_bound

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


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

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

1 subgoal (ID 589)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  NEQ2 : t1 <= ppt <=
         t1 +
         priority_inversion_is_bounded.max_length_of_priority_inversion
           arr_seq (edf.EDF Task Job) j t1
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
  blocking_bound

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


      move: NEQ2 ⇒ /andP [GE LE].

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

1 subgoal (ID 651)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) 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 662)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 t2 <=
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

3 subgoals (ID 671)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end <=
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

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

4 subgoals (ID 718)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  ppt <= t2

subgoal 2 (ID 694) is:
 \sum_(t1 <= i < ppt)
    match sched i with
    | Some jlp => ~~ edf.EDF Task Job jlp j
    | None => false
    end +
 \sum_(ppt <= i < t2)
    match sched i with
    | Some jlp => ~~ edf.EDF Task Job jlp j
    | None => false
    end <=
 \sum_(t1 <= t < ppt)
    match sched t with
    | Some jlp => ~~ edf.EDF Task Job jlp j
    | None => false
    end
subgoal 3 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 4 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

1 subgoal (ID 718)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  ppt <= t2

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


rewrite ltn_subRL in NEQ.

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

1 subgoal (ID 806)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  NEQ : t1 + blocking_bound < t2
  ============================
  ppt <= t2

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


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

1 subgoal (ID 807)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 811)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 694)

subgoal 1 (ID 694) is:
 \sum_(t1 <= i < ppt)
    match sched i with
    | Some jlp => ~~ edf.EDF Task Job jlp j
    | None => false
    end +
 \sum_(ppt <= i < t2)
    match sched i with
    | Some jlp => ~~ edf.EDF Task Job jlp j
    | None => false
    end <=
 \sum_(t1 <= t < ppt)
    match sched t with
    | Some jlp => ~~ edf.EDF Task Job jlp j
    | None => false
    end
subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


}

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

3 subgoals (ID 694)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  \sum_(t1 <= i < ppt)
     match sched i with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end +
  \sum_(ppt <= i < t2)
     match sched i with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end <=
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

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

3 subgoals (ID 843)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  \sum_(ppt <= i < t2)
     match sched i with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end == 0

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

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

3 subgoals (ID 968)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  ============================
  match sched t with
  | Some jlp => ~~ edf.EDF Task Job jlp j
  | None => false
  end = 0

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

3 subgoals (ID 1038)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  ~~ edf.EDF Task Job s j = 0

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) 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 1150)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  exists pr_t : instant,
    preemption_time.preemption_time sched pr_t /\
    t1 <= pr_t <= t1 + (ppt - t1)

subgoal 2 (ID 1151) is:
 t1 + (ppt - t1) <= t < t2
subgoal 3 (ID 1165) is:
 ~~ edf.EDF Task Job s j = 0
subgoal 4 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 5 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

1 subgoal (ID 1150)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  exists pr_t : instant,
    preemption_time.preemption_time sched pr_t /\
    t1 <= pr_t <= t1 + (ppt - t1)

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


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

2 subgoals (ID 1191)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  preemption_time.preemption_time sched ppt

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

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


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

1 subgoal (ID 1192)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 1151)

subgoal 1 (ID 1151) is:
 t1 + (ppt - t1) <= t < t2
subgoal 2 (ID 1165) is:
 ~~ edf.EDF Task Job s j = 0
subgoal 3 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 4 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

4 subgoals (ID 1151)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 1165) is:
 ~~ edf.EDF Task Job s j = 0
subgoal 3 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 4 (ID 665) is:
 ppt - t1 <= blocking_bound

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



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

1 subgoal (ID 1151)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 1165)

subgoal 1 (ID 1165) is:
 ~~ edf.EDF Task Job s j = 0
subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


}

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

3 subgoals (ID 1165)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 : edf.EDF Task Job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  ~~ edf.EDF Task Job s j = 0

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


        apply/eqP; rewrite eqb0 Bool.negb_involutive.

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

3 subgoals (ID 1363)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 : edf.EDF Task Job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  edf.EDF Task Job s j

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

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

3 subgoals (ID 1367)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 : edf.EDF Task Job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  s = j_hp

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

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

3 subgoals (ID 1530)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s, j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : edf.EDF Task Job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  SCHED : scheduled_at sched s t
  ============================
  s = j_hp

subgoal 2 (ID 664) is:
 cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1
subgoal 3 (ID 665) is:
 ppt - t1 <= blocking_bound

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


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

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

2 subgoals (ID 664)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  cumulative_priority_inversion sched (edf.EDF Task Job) j t1 ppt <= ppt - t1

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

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


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

2 subgoals (ID 1541)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end <= ppt - t1

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

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


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

2 subgoals (ID 1569)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ edf.EDF Task Job jlp j
     | None => false
     end <= \sum_(t1 <= i < ppt) 1

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

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


        rewrite leq_sum //.

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

2 subgoals (ID 1578)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  forall i : nat,
  true ->
  match sched i with
  | Some jlp => ~~ edf.EDF Task Job jlp j
  | None => false
  end <= 1

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

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


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

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

2 subgoals (ID 1614)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  t : nat
  ============================
  forall a : Job, ~~ edf.EDF Task Job a j <= 1

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

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


          by intros s; case: edf.EDF.

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

1 subgoal (ID 665)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  ppt - t1 <= blocking_bound

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


      - rewrite leq_subLR.

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

1 subgoal (ID 1642)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) 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 1644)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  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 (edf.EDF Task Job) j t1 t2
  T : t1 <= job_arrival j
  NEQ : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time.preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 +
       priority_inversion_is_bounded.max_length_of_priority_inversion arr_seq
         (edf.EDF Task Job) j t1
  ============================
  t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound

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


         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.

To reduce the time complexity of the analysis, recall the notion of search space.
Consider any value R, and assume that for any given arrival offset A in the search space, there is a solution of the response-time bound recurrence which is bounded by R.
    Variable R : duration.
    Hypothesis H_R_is_maximum:
       (A : duration),
        is_in_search_space A
         (F : duration),
          A + F = blocking_bound
                  + (task_rbf (A + ε) - (task_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 310)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := fun A : nat =>
                        (A < L) &&
                        (task_rbf_changes_at A
                         || bound_on_total_hep_workload_changes_at A)
   : nat -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) -
                      (task_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 338)
  
  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 Task 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 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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              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_is_bounded.max_length_of_priority_inversion
                                        arr_seq EDF : 
  Job -> instant -> nat
  task_rbf_changes_at := [eta response_time_bound.task_rbf_changes_at tsk]
   : duration -> bool
  bound_on_total_hep_workload_changes_at := response_time_bound.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
  L : duration
  H_L_positive : 0 < L
  H_fixed_point : L = total_rbf L
  is_in_search_space := fun A : nat =>
                        (A < L) &&
                        (task_rbf_changes_at A
                         || bound_on_total_hep_workload_changes_at A)
   : nat -> bool
  R : duration
  H_R_is_maximum : forall A : duration,
                   is_in_search_space A ->
                   exists F : duration,
                     A + F =
                     blocking_bound +
                     (task_rbf (A + ε) -
                      (task_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 (edf.EDF Task Job) tsk
    blocking_bound

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


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

No more subgoals.

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


    Qed.

  End ResponseTimeBound.

End RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.