Library prosa.results.fixed_priority.rta.bounded_nps


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.
Require Export prosa.results.fixed_priority.rta.bounded_pi.

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

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

RTA for FP-schedulers with Bounded Non-Preemptive Segments

In this section we instantiate the Abstract RTA for FP-schedulers with Bounded Priority Inversion to FP-schedulers for ideal uni-processor model of real-time tasks with arbitrary arrival models _and_ bounded non-preemptive segments.
Recall that Abstract RTA for FP-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 FP-schedulers is applicable to this instantiation.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost 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}.

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

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

... assume that all jobs come from the task set, ...
... and the cost of a job cannot be larger than the task cost.
Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
Let [tsk] be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Consider a valid preemption model...
...and a valid task run-to-completion threshold function. That is, [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s cost, (2) for any job of task [tsk] job_run_to_completion_threshold is bounded by task_run_to_completion_threshold.
Let's define some local names for clarity.
We also define a bound for the priority inversion caused by jobs with lower priority.

Priority inversion is bounded

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

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

1 subgoal (ID 1947)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  ============================
  forall (j : Job) (t : instant),
  arrives_in arr_seq j ->
  job_task j = tsk -> max_length_of_priority_inversion j t <= blocking_bound

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


    Proof.
      intros j t ARR TSK.

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

1 subgoal (ID 1951)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  max_length_of_priority_inversion j t <= blocking_bound

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


      rewrite /max_length_of_priority_inversion /blocking_bound /FP_to_JLFP
              /priority_inversion.max_length_of_priority_inversion.

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

1 subgoal (ID 1959)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  \max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j)
     (job_max_nonpreemptive_segment j_lp - ε) <=
  \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
     (task_max_nonpreemptive_segment tsk_other - ε)

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


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

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

2 subgoals (ID 1976)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  \max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j)
     (job_max_nonpreemptive_segment j_lp - ε) <=
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                               hep_task (job_task j_lp) tsk)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε)

subgoal 2 (ID 1977) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
    (task_max_nonpreemptive_segment tsk_other - ε)

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


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

1 subgoal (ID 1976)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  \max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j)
     (job_max_nonpreemptive_segment j_lp - ε) <=
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                               hep_task (job_task j_lp) tsk)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε)

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


rewrite /hep_job TSK.

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

1 subgoal (ID 1984)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  \max_(j_lp <- arrivals_before arr_seq t | ~~ hep_task (job_task j_lp) tsk)
     (job_max_nonpreemptive_segment j_lp - ε) <=
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                               hep_task (job_task j_lp) tsk)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε)

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


        apply leq_big_max.

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

1 subgoal (ID 1985)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  forall i : Job,
  i \in arrivals_between arr_seq 0 t ->
  ~~ hep_task (job_task i) tsk ->
  job_max_nonpreemptive_segment i - ε <=
  task_max_nonpreemptive_segment (job_task i) - ε

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


        intros j' JINB NOTHEP.

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

1 subgoal (ID 1988)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  job_max_nonpreemptive_segment j' - ε <=
  task_max_nonpreemptive_segment (job_task j') - ε

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


        rewrite leq_sub2r //.

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

1 subgoal (ID 1995)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  job_max_nonpreemptive_segment j' <=
  task_max_nonpreemptive_segment (job_task j')

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


        apply H_valid_model_with_bounded_nonpreemptive_segments.

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

1 subgoal (ID 2028)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  arrives_in arr_seq j'

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


          by eapply in_arrivals_implies_arrived; eauto 2.

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

1 subgoal (ID 1977)

subgoal 1 (ID 1977) is:
 \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk)
    (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
 \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
    (task_max_nonpreemptive_segment tsk_other - ε)

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


      }

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

1 subgoal (ID 1977)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                               hep_task (job_task j_lp) tsk)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
  \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
     (task_max_nonpreemptive_segment tsk_other - ε)

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


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

1 subgoal (ID 1977)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  \max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                               hep_task (job_task j_lp) tsk)
     (task_max_nonpreemptive_segment (job_task j_lp) - ε) <=
  \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
     (task_max_nonpreemptive_segment tsk_other - ε)

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


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

1 focused subgoal
(shelved: 1) (ID 2065)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  forall i : Job,
  i \in arrivals_between arr_seq 0 t ->
  ~~ hep_task (job_task i) tsk ->
  task_max_nonpreemptive_segment (job_task i) - ε <=
  \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
     (task_max_nonpreemptive_segment tsk_other - ε)

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


        intros j' JINB NOTHEP.

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

1 subgoal (ID 2068)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  task_max_nonpreemptive_segment (job_task j') - ε <=
  \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
     (task_max_nonpreemptive_segment tsk_other - ε)

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


        apply leq_bigmax_cond_seq with
            (i0 := (job_task j')) (F := fun tsktask_max_nonpreemptive_segment tsk - 1); last by done.

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

1 subgoal (ID 2077)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  job_task j' \in ts

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


        apply H_all_jobs_from_taskset.

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

1 subgoal (ID 2079)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : j' \in arrivals_between arr_seq 0 t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  arrives_in arr_seq j'

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


        apply mem_bigcat_nat_exists in JINB.

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

1 subgoal (ID 2080)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  j' : Job
  JINB : exists i : nat, j' \in arrivals_at arr_seq i /\ 0 <= i < t
  NOTHEP : ~~ hep_task (job_task j') tsk
  ============================
  arrives_in arr_seq j'

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


          by inversion JINB as [ta' [JIN' _]]; ta'.

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

No more subgoals.

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


      }

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

No more subgoals.

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


    Qed.

Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound.
    Lemma priority_inversion_is_bounded:
      priority_inversion_is_bounded_by
        arr_seq sched tsk blocking_bound.

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

1 subgoal (ID 1957)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  response_time_bounded_by := task_response_time_bound arr_seq sched
   : Task -> duration -> Prop
  ============================
  priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound

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


    Proof.
      intros j ARR TSK POS t1 t2 PREF.

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

1 subgoal (ID 1966)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      case NEQ: (t2 - t1 blocking_bound).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 2021)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = true
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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

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


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

1 subgoal (ID 2021)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = true
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


apply leq_trans with (t2 - t1); last by done.

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

1 subgoal (ID 2069)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = true
  ============================
  cumulative_priority_inversion sched j t1 t2 <= t2 - t1

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


        rewrite /cumulative_priority_inversion /is_priority_inversion.

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

1 subgoal (ID 2076)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = true
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= t2 - t1

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


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

1 subgoal (ID 2113)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = true
  ============================
  forall i : nat,
  true ->
  match sched i with
  | Some jlp => ~~ hep_job jlp j
  | None => false
  end <= 1

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


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

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

1 subgoal (ID 2149)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = true
  t : nat
  ============================
  forall a : Job, ~~ hep_job a j <= 1

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


          by intros s; case: (hep_job s j).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2068)

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

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


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

1 subgoal (ID 2068)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  NEQ : (t2 - t1 <= blocking_bound) = false
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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



      move: NEQ ⇒ /negP /negP; rewrite -ltnNge; moveBOUND.

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

1 subgoal (ID 2243)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


      edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2; move: NEQ ⇒ /andP [GE LE].

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

1 subgoal (ID 2360)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <= blocking_bound

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


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

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

3 subgoals (ID 2369)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt - t1 <= blocking_bound

subgoal 2 (ID 2368) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


      - rewrite leq_subLR.

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

3 subgoals (ID 2374)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt <= t1 + blocking_bound

subgoal 2 (ID 2368) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


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

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

3 subgoals (ID 2376)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound

subgoal 2 (ID 2368) is:
 cumulative_priority_inversion sched j t1 ppt <= ppt - t1
subgoal 3 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


          by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.

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

2 subgoals (ID 2368)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 ppt <= ppt - t1

subgoal 2 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


      - rewrite /cumulative_priority_inversion /is_priority_inversion.

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

2 subgoals (ID 2392)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= ppt - t1

subgoal 2 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


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

2 subgoals (ID 2420)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <= \sum_(t1 <= i < ppt) 1

subgoal 2 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


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

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

2 subgoals (ID 2465)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  ============================
  forall a : Job, ~~ hep_job a j <= 1

subgoal 2 (ID 2366) is:
 cumulative_priority_inversion sched j t1 t2 <=
 cumulative_priority_inversion sched j t1 ppt

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


          by intros s; case: (hep_job s j).

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

1 subgoal (ID 2366)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  cumulative_priority_inversion sched j t1 t2 <=
  cumulative_priority_inversion sched j t1 ppt

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


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

1 subgoal (ID 2482)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= t < t2)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <=
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end

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


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

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

2 subgoals (ID 2529)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt <= t2

subgoal 2 (ID 2505) is:
 \sum_(t1 <= i < ppt)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end +
 \sum_(ppt <= i < t2)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end <=
 \sum_(t1 <= t < ppt)
    match sched t with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end

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


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

1 subgoal (ID 2529)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  ppt <= t2

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


rewrite ltn_subRL in BOUND.

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

1 subgoal (ID 2613)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  BOUND : t1 + blocking_bound < t2
  ============================
  ppt <= t2

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


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

1 subgoal (ID 2614)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  BOUND : 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 2618)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  BOUND : t1 + blocking_bound < t2
  ============================
  t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound

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


          rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.

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

1 subgoal (ID 2505)

subgoal 1 (ID 2505) is:
 \sum_(t1 <= i < ppt)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end +
 \sum_(ppt <= i < t2)
    match sched i with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end <=
 \sum_(t1 <= t < ppt)
    match sched t with
    | Some jlp => ~~ hep_job jlp j
    | None => false
    end

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


        }

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

1 subgoal (ID 2505)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(t1 <= i < ppt)
     match sched i with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end +
  \sum_(ppt <= i < t2)
     match sched i with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end <=
  \sum_(t1 <= t < ppt)
     match sched t with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end

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


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

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

1 subgoal (ID 2646)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  ============================
  \sum_(ppt <= i < t2)
     match sched i with
     | Some jlp => ~~ hep_job jlp j
     | None => false
     end == 0

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


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

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

1 subgoal (ID 2771)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  ============================
  match sched t with
  | Some jlp => ~~ hep_job jlp j
  | None => false
  end = 0

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


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

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

1 subgoal (ID 2837)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  ~~ hep_job s j = 0

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


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

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

3 subgoals (ID 2941)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  exists pr_t : instant,
    preemption_time sched pr_t /\ t1 <= pr_t <= t1 + (ppt - t1)

subgoal 2 (ID 2942) is:
 t1 + (ppt - t1) <= t < t2
subgoal 3 (ID 2956) is:
 ~~ hep_job s j = 0

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


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

1 subgoal (ID 2941)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  exists pr_t : instant,
    preemption_time sched pr_t /\ t1 <= pr_t <= t1 + (ppt - t1)

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


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

2 subgoals (ID 2942)

subgoal 1 (ID 2942) is:
 t1 + (ppt - t1) <= t < t2
subgoal 2 (ID 2956) is:
 ~~ hep_job s j = 0

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


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

2 subgoals (ID 2942)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  t1 + (ppt - t1) <= t < t2

subgoal 2 (ID 2956) is:
 ~~ hep_job s j = 0

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



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

1 subgoal (ID 2942)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  ============================
  t1 + (ppt - t1) <= t < t2

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


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

1 subgoal (ID 2956)

subgoal 1 (ID 2956) is:
 ~~ hep_job s j = 0

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


}

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

1 subgoal (ID 2956)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  ~~ hep_job s j = 0

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


        apply/eqP; rewrite eqb0 Bool.negb_involutive.

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

1 subgoal (ID 3174)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  hep_job s j

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


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

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

1 subgoal (ID 3178)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  s = j_hp

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


        eapply ideal_proc_model_is_a_uniprocessor_model; eauto 2.

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

1 subgoal (ID 3204)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 j t1 t2
  BOUND : blocking_bound < t2 - t1
  ppt : instant
  PPT : preemption_time sched ppt
  GE : t1 <= ppt
  LE : ppt <=
       t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
  t : nat
  GEt : ppt <= t
  LTt : t < t2
  s : Job
  SCHED : sched t = Some s
  j_hp : Job
  ARRB : arrived_between j_hp t1 (succn t)
  HP : hep_job j_hp j
  SCHEDHP : scheduled_at sched j_hp t
  ============================
  scheduled_at sched s t

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


          by rewrite scheduled_at_def SCHED.

(* ----------------------------------[ 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 = blocking_bound + total_hep_rbf L.

To reduce the time complexity of the analysis, recall the notion of search space.
Next, consider any value R, and assume that for any given arrival offset A from the search space there is a solution of the response-time bound recurrence that 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))
                  + total_ohep_rbf (A + F)
          F + (task_cost tsk - task_run_to_completion_threshold tsk) R.

Then, using the results for the general RTA for FP-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 FP-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_fp_with_bounded_nonpreemptive_segments:
      response_time_bounded_by tsk R.

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

1 subgoal (ID 1955)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskRunToCompletionThreshold Task
  H1 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
  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
  H5 : JobPreemptable Job
  H_valid_model_with_bounded_nonpreemptive_segments : 
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched
  H6 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  H_priority_is_transitive : transitive_priorities
  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_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H7 : MaxArrivals Task
  H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
  H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
                                          arr_seq tsk
  max_length_of_priority_inversion := priority_inversion.max_length_of_priority_inversion
                                        arr_seq : 
  Job -> instant -> nat
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_hep_rbf := total_hep_request_bound_function_FP ts tsk
   : duration -> nat
  total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk
   : duration -> nat
  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 = blocking_bound + total_hep_rbf L
  is_in_search_space := bounded_pi.is_in_search_space tsk L : 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)) +
                     total_ohep_rbf (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_fp;
        eauto using priority_inversion_is_bounded.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


    Qed.

  End ResponseTimeBound.

End RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.