Library rt.restructuring.analysis.arrival.workload_bound


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

Welcome to Coq 8.10.1 (October 2019)

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

From rt.util Require Import sum.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task schedule.priority_based.priorities.
From rt.restructuring.model.aggregate Require Import task_arrivals.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.analysis Require Import
     workload ideal_schedule basic_facts.arrivals.

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

Task Workload Bounded by Arrival Curves

Section TaskWorkloadBoundedByArrivalCurves.

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

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

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

... and any ideal uniprocessor schedule of this arrival sequence.
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

Consider an FP policy that indicates a higher-or-equal priority relation.
  Variable higher_eq_priority : FP_policy Task.
  Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.

For simplicity, let's define some local names.
  Let arrivals_between := arrivals_between arr_seq.

We define the notion of request bound function.
  Section RequestBoundFunction.

Let MaxArrivals denote any function that takes a task and an interval length and returns the associated number of job arrivals of the task.
    Context `{MaxArrivals Task}.

In this section, we define a bound for the workload of a single task under uniprocessor FP scheduling.
    Section SingleTask.

Consider any task tsk that is to be scheduled in an interval of length delta.
      Variable tsk : Task.
      Variable delta : duration.

We define the following workload bound for the task.
      Definition task_request_bound_function := task_cost tsk × max_arrivals tsk delta.

    End SingleTask.

In this section, we define a bound for the workload of multiple tasks.
    Section AllTasks.

Consider a task set ts...
      Variable ts : list Task.

...and let tsk be any task in task set.
      Variable tsk : Task.

Let delta be the length of the interval of interest.
      Variable delta : duration.

Recall the definition of higher-or-equal-priority task and the per-task workload bound for FP scheduling.
      Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
      Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).

Using the sum of individual workload bounds, we define the following bound for the total workload of tasks in any interval of length delta.
      Definition total_request_bound_function :=
        \sum_(tsk <- ts) task_request_bound_function tsk delta.

Similarly, we define the following bound for the total workload of tasks of higher-or-equal priority (with respect to tsk) in any interval of length delta.
      Definition total_hep_request_bound_function_FP :=
        \sum_(tsk_other <- ts | is_hep_task tsk_other)
         task_request_bound_function tsk_other delta.

We also define a bound for the total workload of higher-or-equal priority tasks other than tsk in any interval of length delta.
      Definition total_ohep_request_bound_function_FP :=
        \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
         task_request_bound_function tsk_other delta.

    End AllTasks.

  End RequestBoundFunction.

In this section we prove some lemmas about request bound functions.
  Section ProofWorkloadBound.

Consider a task set ts...
    Variable ts : list Task.

...and let tsk be any task in ts.
    Variable tsk : Task.
    Hypothesis H_tsk_in_ts : tsk \in ts.

Assume that the job costs are no larger than the task costs.
    Hypothesis H_job_cost_le_task_cost :
      cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.

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

Let max_arrivals be any arrival bound for taskset ts.
    Context `{MaxArrivals Task}.
    Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.

Let's define some local names for clarity.
    Let task_rbf := task_request_bound_function tsk.
    Let total_rbf := total_request_bound_function ts.
    Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
    Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.

Next, we consider any job j of tsk.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_task j = tsk.

Next, we say that two jobs j1 and j2 are in relation other_higher_eq_priority, iff j1 has higher or equal priority than j2 and is produced by a different task.
    Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).

Next, we recall the notions of total workload of jobs...
    Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between t1 t2).

...notions of workload of higher or equal priority jobs...
    Let total_hep_workload t1 t2 :=
      workload_of_jobs (fun j_other ⇒ jlfp_higher_eq_priority j_other j) (arrivals_between t1 t2).

... workload of other higher or equal priority jobs...
    Let total_ohep_workload t1 t2 :=
      workload_of_jobs (fun j_other ⇒ other_higher_eq_priority j_other j) (arrivals_between t1 t2).

... and the workload of jobs of the same task as job j.
    Let task_workload t1 t2 :=
      workload_of_jobs (job_of_task tsk) (arrivals_between t1 t2).

In this section we prove that the workload of any jobs is no larger than the request bound function.
    Section WorkloadIsBoundedByRBF.

Consider any time t and any interval of length delta.
      Variable t : instant.
      Variable delta : instant.

First, we show that workload of task tsk is bounded by the number of arrivals of the task times the cost of the task.
      Lemma task_workload_le_num_of_arrivals_times_cost:
        task_workload t (t + delta)
        ≤ task_cost tsk × number_of_task_arrivals arr_seq tsk t (t + delta).

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

1 subgoal (ID 235)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  task_workload t (t + delta) <=
  task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta)

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

      Proof.
        rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.

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

1 subgoal (ID 289)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  task_workload t (t + delta) <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk) task_cost tsk * 1

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

        rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.

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

1 subgoal (ID 313)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  \sum_(j0 <- arrivals_between t (t + delta) | job_of_task tsk j0)
     job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk) task_cost tsk * 1

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

        rewrite /same_task -H_job_of_tsk muln1.

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

1 subgoal (ID 327)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  \sum_(j0 <- arrivals_between t (t + delta) | job_of_task (job_task j) j0)
     job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == job_task j) task_cost (job_task j)

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

        apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.

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

1 subgoal (ID 364)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = job_task j
  ============================
  job_cost j0 <= task_cost (job_task j)

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

        rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.

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

1 subgoal (ID 368)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  j0 : Job
  IN0 : arrives_in arr_seq j0
  EQ : job_task j0 = job_task j
  ============================
  job_cost j0 <= task_cost (job_task j0)

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

          by apply H_job_cost_le_task_cost.

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

No more subgoals.

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

      Qed.

As a corollary, we prove that workload of task is no larger the than task request bound function.
      Corollary task_workload_le_task_rbf:
        task_workload t (t + delta) ≤ task_rbf delta.

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

1 subgoal (ID 236)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  task_workload t (t + delta) <= task_rbf delta

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

      Proof.
        apply leq_trans with
            (task_cost tsk × number_of_task_arrivals arr_seq tsk t (t + delta));
          first by apply task_workload_le_num_of_arrivals_times_cost.

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

1 subgoal (ID 243)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta) <=
  task_rbf delta

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

        rewrite leq_mul2l; apply/orP; right.

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

1 subgoal (ID 274)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  number_of_task_arrivals arr_seq tsk t (t + delta) <= max_arrivals tsk delta

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

        rewrite -{2}[delta](addKn t).

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

1 subgoal (ID 280)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  number_of_task_arrivals arr_seq tsk t (t + delta) <=
  max_arrivals tsk (t + delta - t)

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

          by apply H_is_arrival_bound; last rewrite leq_addr.

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

No more subgoals.

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

      Qed.

Next, we prove that total workload of other tasks with higher-or-equal priority is no larger than the total request bound function.
      Lemma total_workload_le_total_rbf:
        total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.

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

1 subgoal (ID 237)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  total_ohep_workload t (t + delta) <= total_ohep_rbf delta

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

      Proof.
        set l := arrivals_between t (t + delta).

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

1 subgoal (ID 239)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  total_ohep_workload t (t + delta) <= total_ohep_rbf delta

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

        set hep := higher_eq_priority.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 241)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  total_ohep_workload t (t + delta) <= total_ohep_rbf delta

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


        apply leq_trans with
            (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
              (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).

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

2 subgoals (ID 259)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  total_ohep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

subgoal 2 (ID 260) is:
 \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
    \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= 
 total_ohep_rbf delta

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

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

1 subgoal (ID 259)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  total_ohep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

intros.
          rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.

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

1 subgoal (ID 267)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  \sum_(j0 <- arrivals_between t (t + delta) | jlfp_higher_eq_priority j0 j &&
                                               ~~ same_task j0 j) 
  job_cost j0 <=
  \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 278)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  \sum_(j0 <- arrivals_between t (t + delta) | hep_task (job_task j0) tsk &&
                                               (job_task j0 != tsk))
     job_cost j0 <=
  \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          have EXCHANGE := exchange_big_dep (fun x ⇒ hep (job_task x) tsk && (job_task x != tsk)).

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

1 subgoal (ID 302)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 : Type) (j : JobType) (l : seq T0) 
               (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j)
               (j0 j1 : JobTask j Task) (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i -> p0 i j2 -> hep (job_task j2) tsk && (job_task j2 != tsk)) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j2 <- l0 | p0 i j2) F i j2 =
             \big[c/y]_(j2 <- l0 | hep (job_task j2) tsk &&
                                   (job_task j2 != tsk))
                \big[c/y]_(i <- l | p i && p0 i j2) F i j2
  ============================
  \sum_(j0 <- arrivals_between t (t + delta) | hep_task (job_task j0) tsk &&
                                               (job_task j0 != tsk))
     job_cost j0 <=
  \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.

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

1 subgoal (ID 319)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 : Type) (j : JobType) (l : seq T0) 
               (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j)
               (j0 j1 : JobTask j Task) (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i -> p0 i j2 -> hep (job_task j2) tsk && (job_task j2 != tsk)) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j2 <- l0 | p0 i j2) F i j2 =
             \big[c/y]_(j2 <- l0 | hep (job_task j2) tsk &&
                                   (job_task j2 != tsk))
                \big[c/y]_(i <- l | p i && p0 i j2) F i j2
  ============================
  \sum_(j0 <- arrivals_between t (t + delta) | hep_task (job_task j0) tsk &&
                                               (job_task j0 != tsk))
     job_cost j0 <=
  \sum_(j0 <- l | hep (job_task j0) tsk && (job_task j0 != tsk))
     \sum_(i <- ts | hep i tsk && (i != tsk) && (job_task j0 == i))
        job_cost j0

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

          rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.

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

1 subgoal (ID 388)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 : Type) (j : JobType) (l : seq T0) 
               (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j)
               (j0 j1 : JobTask j Task) (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i -> p0 i j2 -> hep (job_task j2) tsk && (job_task j2 != tsk)) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j2 <- l0 | p0 i j2) F i j2 =
             \big[c/y]_(j2 <- l0 | hep (job_task j2) tsk &&
                                   (job_task j2 != tsk))
                \big[c/y]_(i <- l | p i && p0 i j2) F i j2
  ============================
  \sum_(i <- l | [&& i \in l, hep_task (job_task i) tsk & job_task i != tsk])
     job_cost i <=
  \sum_(i <- l | [&& i \in l, hep (job_task i) tsk & job_task i != tsk])
     \sum_(i0 <- ts | hep i0 tsk && (i0 != tsk) && (job_task i == i0))
        job_cost i

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

          apply leq_sum; move ⇒ j0 /andP [IN0 HP0].

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

1 subgoal (ID 430)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 : Type) (j : JobType) (l : seq T0) 
               (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j)
               (j0 j1 : JobTask j Task) (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i -> p0 i j2 -> hep (job_task j2) tsk && (job_task j2 != tsk)) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j2 <- l0 | p0 i j2) F i j2 =
             \big[c/y]_(j2 <- l0 | hep (job_task j2) tsk &&
                                   (job_task j2 != tsk))
                \big[c/y]_(i <- l | p i && p0 i j2) F i j2
  j0 : Job
  IN0 : j0 \in l
  HP0 : hep (job_task j0) tsk && (job_task j0 != tsk)
  ============================
  job_cost j0 <=
  \sum_(i <- ts | hep i tsk && (i != tsk) && (job_task j0 == i)) job_cost j0

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

          rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.

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

1 subgoal (ID 463)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 : Type) (j : JobType) (l : seq T0) 
               (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j)
               (j0 j1 : JobTask j Task) (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i -> p0 i j2 -> hep (job_task j2) tsk && (job_task j2 != tsk)) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j2 <- l0 | p0 i j2) F i j2 =
             \big[c/y]_(j2 <- l0 | hep (job_task j2) tsk &&
                                   (job_task j2 != tsk))
                \big[c/y]_(i <- l | p i && p0 i j2) F i j2
  j0 : Job
  IN0 : j0 \in l
  HP0 : hep (job_task j0) tsk && (job_task j0 != tsk)
  ============================
  job_task j0 \in ts

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

            by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.

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

1 subgoal (ID 260)

subgoal 1 (ID 260) is:
 \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
    \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= 
 total_ohep_rbf delta

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

        }

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

1 subgoal (ID 260)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  \sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= 
  total_ohep_rbf delta

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

        apply leq_sum_seq; intros tsk0 INtsk0 HP0.

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

1 subgoal (ID 482)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_request_bound_function tsk0 delta

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

        apply leq_trans with
            (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + delta))).

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

2 subgoals (ID 489)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))

subgoal 2 (ID 490) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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

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

1 subgoal (ID 489)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))

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

rewrite -sum1_size big_distrr /= big_filter.

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

1 subgoal (ID 515)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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

          rewrite /workload_of_jobs.

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

1 subgoal (ID 520)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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

          rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 530)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- \big[cat/[::]]_(t <= t0 < t + delta) arrivals_at arr_seq t0 | 
  job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- \big[cat/[::]]_(t <= t0 < t + delta) arrivals_at arr_seq t0 | 
  job_task i == tsk0) task_cost tsk0

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

          apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.

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

1 subgoal (ID 567)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  j0 : Job
  IN0 : j0 \in \big[cat/[::]]_(t <= t < t + delta) arrivals_at arr_seq t
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost tsk0

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

            by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0.

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

1 subgoal (ID 490)

subgoal 1 (ID 490) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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

        }

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

1 subgoal (ID 490)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  task_request_bound_function tsk0 delta

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

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

1 subgoal (ID 490)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  task_request_bound_function tsk0 delta

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

rewrite leq_mul2l; apply/orP; right.

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

1 subgoal (ID 604)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  max_arrivals tsk0 delta

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

          rewrite -{2}[delta](addKn t).

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

1 subgoal (ID 610)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk && (tsk0 != tsk)
  ============================
  size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  max_arrivals tsk0 (t + delta - t)

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

            by apply H_is_arrival_bound; last rewrite leq_addr.

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

No more subgoals.

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

        }

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

No more subgoals.

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

      Qed.

Next, we prove that total workload of tasks with higher-or-equal priority is no larger than the total request bound function.
      Lemma total_workload_le_total_rbf':
        total_hep_workload t (t + delta) ≤ total_hep_rbf delta.

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

1 subgoal (ID 238)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  total_hep_workload t (t + delta) <= total_hep_rbf delta

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

      Proof.
        set l := arrivals_between t (t + delta).

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

1 subgoal (ID 240)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  total_hep_workload t (t + delta) <= total_hep_rbf delta

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

        set hep := higher_eq_priority.

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

1 subgoal (ID 242)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  total_hep_workload t (t + delta) <= total_hep_rbf delta

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

        apply leq_trans with
            (n := \sum_(tsk' <- ts | hep tsk' tsk)
                   (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).

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

2 subgoals (ID 259)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  total_hep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

subgoal 2 (ID 260) is:
 \sum_(tsk' <- ts | hep tsk' tsk)
    \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= 
 total_hep_rbf delta

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

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

1 subgoal (ID 259)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  total_hep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 265)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk)
    (arrivals_between t (t + delta)) <=
  \sum_(tsk' <- ts | hep tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          have EXCHANGE := exchange_big_dep (fun x ⇒ hep (job_task x) tsk).

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

1 subgoal (ID 284)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 : Type) (j : JobType) (l : seq T0) 
               (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j)
               (j0 : JobTask j Task) (F : T0 -> j -> T),
             (forall (i : T0) (j1 : j),
              p i -> p0 i j1 -> hep (job_task j1) tsk) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j1 <- l0 | p0 i j1) F i j1 =
             \big[c/y]_(j1 <- l0 | hep (job_task j1) tsk)
                \big[c/y]_(i <- l | p i && p0 i j1) F i j1
  ============================
  workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk)
    (arrivals_between t (t + delta)) <=
  \sum_(tsk' <- ts | hep tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          rewrite EXCHANGE /=; clear EXCHANGE; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.

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

1 subgoal (ID 302)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk)
    (arrivals_between t (t + delta)) <=
  \sum_(j0 <- l | hep (job_task j0) tsk)
     \sum_(i <- ts | hep i tsk && (job_task j0 == i)) job_cost j0

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

          rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.

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

1 subgoal (ID 371)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  \sum_(i <- l | (i \in l) && hep_task (job_task i) tsk) job_cost i <=
  \sum_(i <- l | (i \in l) && hep (job_task i) tsk)
     \sum_(i0 <- ts | hep i0 tsk && (job_task i == i0)) job_cost i

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

          apply leq_sum; move ⇒ j0 /andP [IN0 HP0].

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

1 subgoal (ID 413)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  j0 : Job
  IN0 : j0 \in l
  HP0 : hep (job_task j0) tsk
  ============================
  job_cost j0 <= \sum_(i <- ts | hep i tsk && (job_task j0 == i)) job_cost j0

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

          rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.

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

1 subgoal (ID 446)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  j0 : Job
  IN0 : j0 \in l
  HP0 : hep (job_task j0) tsk
  ============================
  job_task j0 \in ts

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

            by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.

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

1 subgoal (ID 260)

subgoal 1 (ID 260) is:
 \sum_(tsk' <- ts | hep tsk' tsk)
    \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= 
 total_hep_rbf delta

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

        }

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

1 subgoal (ID 260)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  ============================
  \sum_(tsk' <- ts | hep tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= 
  total_hep_rbf delta

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

        apply leq_sum_seq; intros tsk0 INtsk0 HP0.

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

1 subgoal (ID 465)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_request_bound_function tsk0 delta

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

        apply leq_trans with
            (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + delta))).

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

2 subgoals (ID 472)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))

subgoal 2 (ID 473) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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

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

1 subgoal (ID 472)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))

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

rewrite -sum1_size big_distrr /= big_filter.

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

1 subgoal (ID 498)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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

          rewrite -/l /workload_of_jobs.

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

1 subgoal (ID 504)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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

          rewrite muln1.

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

1 subgoal (ID 509)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0

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

          apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.

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

1 subgoal (ID 546)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost tsk0

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

          rewrite -EQ.

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

1 subgoal (ID 548)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost (job_task j0)

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

          apply H_job_cost_le_task_cost.

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

1 subgoal (ID 549)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = tsk0
  ============================
  arrives_in arr_seq j0

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

            by apply in_arrivals_implies_arrived in IN0.

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

1 subgoal (ID 473)

subgoal 1 (ID 473) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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

        }

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

1 subgoal (ID 473)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  task_request_bound_function tsk0 delta

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

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

1 subgoal (ID 473)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  task_request_bound_function tsk0 delta

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

rewrite leq_mul2l; apply/orP; right.

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

1 subgoal (ID 583)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  max_arrivals tsk0 delta

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

          rewrite -{2}[delta](addKn t).

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

1 subgoal (ID 589)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  hep := higher_eq_priority : FP_policy Task
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : higher_eq_priority tsk0 tsk
  ============================
  size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  max_arrivals tsk0 (t + delta - t)

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

            by apply H_is_arrival_bound; last rewrite leq_addr.

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

No more subgoals.

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

        }

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

No more subgoals.

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

      Qed.

Next, we prove that total workload of tasks is no larger than the total request bound function.
      Lemma total_workload_le_total_rbf'':
        total_workload t (t + delta) ≤ total_rbf delta.

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

1 subgoal (ID 239)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  ============================
  total_workload t (t + delta) <= total_rbf delta

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

      Proof.
        set l := arrivals_between t (t + delta).

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

1 subgoal (ID 241)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  total_workload t (t + delta) <= total_rbf delta

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

        apply leq_trans with
            (n := \sum_(tsk' <- ts)
                   (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).

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

2 subgoals (ID 258)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  total_workload t (t + delta) <=
  \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

subgoal 2 (ID 259) is:
 \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
 total_rbf delta

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

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

1 subgoal (ID 258)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  total_workload t (t + delta) <=
  \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

rewrite /total_workload.

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

1 subgoal (ID 260)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  workload_of_jobs (pred_of_simpl (T:=Job) predT)
    (arrivals_between t (t + delta)) <=
  \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          have EXCHANGE := exchange_big_dep predT.

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

1 subgoal (ID 275)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  EXCHANGE : forall (T : Type) (y : T) (c : Monoid.com_law y) 
               (T0 T1 : Type) (l : seq T0) (l0 : seq T1) 
               (p : pred T0) (p0 : T0 -> pred T1) 
               (F : T0 -> T1 -> T),
             (forall (i : T0) (j : T1), p i -> p0 i j -> predT j) ->
             \big[c/y]_(i <- l | p i) \big[c/y]_(j <- l0 | p0 i j) F i j =
             \big[c/y]_(j <- l0 | pred_of_simpl predT j)
                \big[c/y]_(i <- l | p i && p0 i j) F i j
  ============================
  workload_of_jobs (pred_of_simpl (T:=Job) predT)
    (arrivals_between t (t + delta)) <=
  \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

          rewrite EXCHANGE /=; clear EXCHANGE; last by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 292)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  workload_of_jobs (pred_of_simpl (T:=Job) predT)
    (arrivals_between t (t + delta)) <=
  \sum_(j0 <- l) \sum_(i <- ts | job_task j0 == i) job_cost j0

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

          rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.

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

1 subgoal (ID 326)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  \sum_(i <- l | (i \in l) && pred_of_simpl predT i) job_cost i <=
  \sum_(i <- l | (i \in l) && true)
     \sum_(i0 <- ts | job_task i == i0) job_cost i

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

          apply leq_sum; move ⇒ j0 /andP [IN0 HP0].

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

1 subgoal (ID 368)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  j0 : Job
  IN0 : j0 \in l
  HP0 : true
  ============================
  job_cost j0 <= \sum_(i <- ts | job_task j0 == i) job_cost j0

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

          rewrite big_mkcond (big_rem (job_task j0)) /=.

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

2 subgoals (ID 400)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  j0 : Job
  IN0 : j0 \in l
  HP0 : true
  ============================
  job_cost j0 <=
  (if job_task j0 == job_task j0 then job_cost j0 else 0) +
  \sum_(y <- rem (T:=Task) (job_task j0) ts)
     (if job_task j0 == y then job_cost j0 else 0)

subgoal 2 (ID 401) is:
 job_task j0 \in ts

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

          rewrite eq_refl; apply leq_addr.

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

1 subgoal (ID 401)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  j0 : Job
  IN0 : j0 \in l
  HP0 : true
  ============================
  job_task j0 \in ts

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

            by apply in_arrivals_implies_arrived in IN0;
              apply H_all_jobs_from_taskset.

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

1 subgoal (ID 259)

subgoal 1 (ID 259) is:
 \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
 total_rbf delta

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

        }

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

1 subgoal (ID 259)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  ============================
  \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
  total_rbf delta

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

        apply leq_sum_seq; intros tsk0 INtsk0 HP0.

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

1 subgoal (ID 413)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_request_bound_function tsk0 delta

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

        apply leq_trans with
            (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + delta))).

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

2 subgoals (ID 420)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))

subgoal 2 (ID 421) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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

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

1 subgoal (ID 420)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))

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

rewrite -sum1_size big_distrr /= big_filter.

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

1 subgoal (ID 446)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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

          rewrite -/l /workload_of_jobs.

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

1 subgoal (ID 452)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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

          rewrite muln1.

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

1 subgoal (ID 457)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrival_sequence.arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0

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

          apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.

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

1 subgoal (ID 494)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost tsk0

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

          rewrite -EQ.

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

1 subgoal (ID 496)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost (job_task j0)

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

          apply H_job_cost_le_task_cost.

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

1 subgoal (ID 497)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  j0 : Job
  IN0 : j0 \in arrival_sequence.arrivals_between arr_seq t (t + delta)
  EQ : job_task j0 = tsk0
  ============================
  arrives_in arr_seq j0

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

            by apply in_arrivals_implies_arrived in IN0.

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

1 subgoal (ID 421)

subgoal 1 (ID 421) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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

        }

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

1 subgoal (ID 421)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  task_request_bound_function tsk0 delta

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

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

1 subgoal (ID 421)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  task_request_bound_function tsk0 delta

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

rewrite leq_mul2l; apply/orP; right.

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

1 subgoal (ID 531)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  max_arrivals tsk0 delta

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

          rewrite -{2}[delta](addKn t).

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

1 subgoal (ID 537)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : 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 (ideal.processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  higher_eq_priority : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  arrivals_between := arrival_sequence.arrivals_between arr_seq
   : instant -> instant -> seq Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H3 : MaxArrivals Task
  H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts
  task_rbf := task_request_bound_function tsk : duration -> nat
  total_rbf := total_request_bound_function ts : 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
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  other_higher_eq_priority := fun j1 j2 : Job =>
                              jlfp_higher_eq_priority j1 j2 &&
                              ~~ same_task j1 j2 : 
  Job -> Job -> bool
  total_workload := fun t1 t2 : instant =>
                    workload_of_jobs (pred_of_simpl (T:=Job) predT)
                      (arrivals_between t1 t2) : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between t1 t2) : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  ============================
  size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
  max_arrivals tsk0 (t + delta - t)

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

            by apply H_is_arrival_bound; last rewrite leq_addr.

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

No more subgoals.

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

        }

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

No more subgoals.

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

      Qed.

    End WorkloadIsBoundedByRBF.

  End ProofWorkloadBound.

End TaskWorkloadBoundedByArrivalCurves.