Library prosa.analysis.facts.model.rbf


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.

Facts about Request Bound Functions (RBFs)

In this file, we prove some lemmas about request bound functions.

RBF is a Bound on Workload

First, we show that a task's RBF is indeed an upper bound on its workload.
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...
... and any ideal uni-processor schedule of this arrival sequence.
Consider an FP policy that indicates a higher-or-equal priority relation.
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.
Next, we assume that all jobs come from the task set.
Let max_arrivals be any arrival bound for task-set [ts].
Let's define some local names for clarity.
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.
Next, we recall the notions of total workload of jobs...
...notions of workload of higher or equal priority jobs...
... workload of other higher or equal priority jobs...
... and the workload of jobs of the same task as job j.
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 704)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq 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 758)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  ============================
  task_workload t (t + delta) <=
  \sum_(i <- 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 782)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  ============================
  \sum_(j0 <- arrivals_between arr_seq t (t + delta) | 
  job_of_task tsk j0) job_cost j0 <=
  \sum_(i <- 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 796)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  ============================
  \sum_(j0 <- arrivals_between arr_seq t (t + delta) | 
  job_of_task (job_task j) j0) job_cost j0 <=
  \sum_(i <- arrivals_between arr_seq t (t + delta) | 
  job_task i == job_task j) task_cost (job_task j)

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


      apply leq_sum_seq; movej0 IN0 /eqP EQ.

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

1 subgoal (ID 833)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  j0 : Job
  IN0 : j0 \in 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 837)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq 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_valid_job_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 705)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq 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 712)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq 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 743)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq 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 749)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq 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 706)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  ============================
  total_ohep_workload t (t + delta) <= total_ohep_rbf delta

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


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

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

1 subgoal (ID 709)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  total_ohep_workload t (t + delta) <= total_ohep_rbf delta

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


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

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

2 subgoals (ID 729)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  total_ohep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

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


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

1 subgoal (ID 729)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  total_ohep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep_task 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 737)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  \sum_(j0 <- arrivals_between arr_seq t (t + delta) | 
  jlfp_higher_eq_priority j0 j && ~~ same_task j0 j) 
  job_cost j0 <=
  \sum_(tsk' <- ts | hep_task 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 748)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  \sum_(j0 <- arrivals_between arr_seq t (t + delta) | 
  hep_task (job_task j0) tsk && (job_task j0 != tsk)) 
  job_cost j0 <=
  \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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


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

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

1 subgoal (ID 774)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  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)
               (f : FP_policy Task) (j0 j1 : JobTask j Task)
               (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i ->
              p0 i j2 -> hep_task (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_task (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 arr_seq t (t + delta) | 
  hep_task (job_task j0) tsk && (job_task j0 != tsk)) 
  job_cost j0 <=
  \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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


        rewrite EXCHANGE /=; last by movetsk0 j0 HEP /eqP JOB0; rewrite JOB0.

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

1 subgoal (ID 792)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  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)
               (f : FP_policy Task) (j0 j1 : JobTask j Task)
               (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i ->
              p0 i j2 -> hep_task (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_task (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 arr_seq t (t + delta) | 
  hep_task (job_task j0) tsk && (job_task j0 != tsk)) 
  job_cost j0 <=
  \sum_(j0 <- l | hep_task (job_task j0) tsk && (job_task j0 != tsk))
     \sum_(i <- ts | hep_task 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 861)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  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)
               (f : FP_policy Task) (j0 j1 : JobTask j Task)
               (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i ->
              p0 i j2 -> hep_task (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_task (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_task (job_task i) tsk & job_task i != tsk])
     \sum_(i0 <- ts | hep_task i0 tsk && (i0 != tsk) && (job_task i == i0))
        job_cost i

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


        apply leq_sum; movej0 /andP [IN0 HP0].

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

1 subgoal (ID 903)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  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)
               (f : FP_policy Task) (j0 j1 : JobTask j Task)
               (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i ->
              p0 i j2 -> hep_task (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_task (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_task (job_task j0) tsk && (job_task j0 != tsk)
  ============================
  job_cost j0 <=
  \sum_(i <- ts | hep_task 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 936)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  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)
               (f : FP_policy Task) (j0 j1 : JobTask j Task)
               (F : T0 -> j -> T),
             (forall (i : T0) (j2 : j),
              p i ->
              p0 i j2 -> hep_task (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_task (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_task (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 730)

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

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


      }

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

1 subgoal (ID 730)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  \sum_(tsk' <- ts | hep_task 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 955)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 962)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 963) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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


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

1 subgoal (ID 962)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 988)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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


        rewrite /workload_of_jobs.

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

1 subgoal (ID 993)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- 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 1005)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
  ============================
  \sum_(j0 <- \cat_(t<=t0<t + delta|true)arrivals_at arr_seq t0 | 
  job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- \cat_(t<=t0<t + delta|true)arrivals_at arr_seq t0 | 
  job_task i == tsk0) task_cost tsk0

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


        apply leq_sum_seq; movej0 IN0 /eqP EQ.

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

1 subgoal (ID 1042)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
  j0 : Job
  IN0 : j0 \in \cat_(t<=t<t + delta|true)arrivals_at arr_seq t
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost tsk0

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


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

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

1 subgoal (ID 963)

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

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


      }

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

1 subgoal (ID 963)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 963)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 1079)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 1085)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 707)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  ============================
  total_hep_workload t (t + delta) <= total_hep_rbf delta

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


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

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

1 subgoal (ID 710)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  total_hep_workload t (t + delta) <= total_hep_rbf delta

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


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

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

2 subgoals (ID 729)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  total_hep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep_task tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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

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


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

1 subgoal (ID 729)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  total_hep_workload t (t + delta) <=
  \sum_(tsk' <- ts | hep_task 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 735)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk)
    (arrivals_between arr_seq t (t + delta)) <=
  \sum_(tsk' <- ts | hep_task tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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


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

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

1 subgoal (ID 756)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  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)
               (f : FP_policy Task) (j0 : JobTask j Task) 
               (F : T0 -> j -> T),
             (forall (i : T0) (j1 : j),
              p i -> p0 i j1 -> hep_task (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_task (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 arr_seq t (t + delta)) <=
  \sum_(tsk' <- ts | hep_task tsk' tsk)
     \sum_(j0 <- l | job_task j0 == tsk') job_cost j0

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


        rewrite EXCHANGE /=; clear EXCHANGE; last by movetsk0 j0 HEP /eqP JOB0; rewrite JOB0.

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

1 subgoal (ID 775)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk)
    (arrivals_between arr_seq t (t + delta)) <=
  \sum_(j0 <- l | hep_task (job_task j0) tsk)
     \sum_(i <- ts | hep_task 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 844)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  \sum_(i <- l | (i \in l) && hep_task (job_task i) tsk) job_cost i <=
  \sum_(i <- l | (i \in l) && hep_task (job_task i) tsk)
     \sum_(i0 <- ts | hep_task i0 tsk && (job_task i == i0)) job_cost i

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


        apply leq_sum; movej0 /andP [IN0 HP0].

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

1 subgoal (ID 886)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  j0 : Job
  IN0 : j0 \in l
  HP0 : hep_task (job_task j0) tsk
  ============================
  job_cost j0 <=
  \sum_(i <- ts | hep_task 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 919)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  j0 : Job
  IN0 : j0 \in l
  HP0 : hep_task (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 730)

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

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


      }

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

1 subgoal (ID 730)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  \sum_(tsk' <- ts | hep_task 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 938)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 945)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 946) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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


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

1 subgoal (ID 945)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 971)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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


        rewrite -/l /workload_of_jobs.

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

1 subgoal (ID 977)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- l | job_task i == tsk0) task_cost tsk0 * 1

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


        rewrite muln1.

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

1 subgoal (ID 982)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk
  ============================
  \sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
  \sum_(i <- l | job_task i == tsk0) task_cost tsk0

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


        apply leq_sum_seq; movej0 IN0 /eqP EQ.

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

1 subgoal (ID 1019)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk
  j0 : Job
  IN0 : j0 \in l
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost tsk0

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


        rewrite -EQ.

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

1 subgoal (ID 1021)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk
  j0 : Job
  IN0 : j0 \in l
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost (job_task j0)

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


        apply H_valid_job_cost.

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

1 subgoal (ID 1022)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task tsk0 tsk
  j0 : Job
  IN0 : j0 \in l
  EQ : job_task j0 = tsk0
  ============================
  arrives_in arr_seq j0

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


          by apply in_arrivals_implies_arrived in IN0.

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

1 subgoal (ID 946)

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

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


      }

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

1 subgoal (ID 946)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 946)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 1056)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 1062)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : hep_task 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 708)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  ============================
  total_workload t (t + delta) <= total_rbf delta

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


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

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

1 subgoal (ID 711)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 728)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 729) is:
 \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
 total_rbf delta

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


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

1 subgoal (ID 728)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 730)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  workload_of_jobs predT (arrivals_between arr_seq 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 745)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 | predT j)
                \big[c/y]_(i <- l | p i && p0 i j) F i j
  ============================
  workload_of_jobs predT (arrivals_between arr_seq 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 762)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  workload_of_jobs predT (arrivals_between arr_seq 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 796)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  ============================
  \sum_(i <- l | (i \in l) && 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; movej0 /andP [IN0 HP0].

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

1 subgoal (ID 838)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 870)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 871) is:
 job_task j0 \in ts

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


        rewrite eq_refl; apply leq_addr.

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

1 subgoal (ID 871)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 729)

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

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


      }

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

1 subgoal (ID 729)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 883)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 890)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 891) is:
 task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta)) <=
 task_request_bound_function tsk0 delta

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


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

1 subgoal (ID 890)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 916)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 <- arrivals_between arr_seq t (t + delta) | 
  job_task i == tsk0) task_cost tsk0 * 1

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


        rewrite -/l /workload_of_jobs.

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

1 subgoal (ID 922)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 <- l | job_task i == tsk0) task_cost tsk0 * 1

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


        rewrite muln1.

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

1 subgoal (ID 927)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 <- l | job_task i == tsk0) task_cost tsk0

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


        apply leq_sum_seq; movej0 IN0 /eqP EQ.

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

1 subgoal (ID 964)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  j0 : Job
  IN0 : j0 \in l
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost tsk0

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


        rewrite -EQ.

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

1 subgoal (ID 966)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  j0 : Job
  IN0 : j0 \in l
  EQ : job_task j0 = tsk0
  ============================
  job_cost j0 <= task_cost (job_task j0)

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


        apply H_valid_job_cost.

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

1 subgoal (ID 967)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq t (t + delta) : seq Job
  tsk0 : Task
  INtsk0 : tsk0 \in ts
  HP0 : true
  j0 : Job
  IN0 : j0 \in l
  EQ : job_task j0 = tsk0
  ============================
  arrives_in arr_seq j0

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


          by apply in_arrivals_implies_arrived in IN0.

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

1 subgoal (ID 891)

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

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


      }

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

1 subgoal (ID 891)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 891)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 1001)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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 1007)
  
  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
  H3 : FP_policy Task
  jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job
  ts : seq Task
  tsk : Task
  H_tsk_in_ts : tsk \in ts
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  H4 : 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 predT (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_hep_workload := fun t1 t2 : instant =>
                        workload_of_jobs (jlfp_higher_eq_priority^~ j)
                          (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  total_ohep_workload := fun t1 t2 : instant =>
                         workload_of_jobs (other_higher_eq_priority^~ j)
                           (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  task_workload := fun t1 t2 : instant =>
                   workload_of_jobs (job_of_task tsk)
                     (arrivals_between arr_seq t1 t2)
   : instant -> instant -> nat
  t, delta : instant
  l := arrivals_between arr_seq 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.

RBF Properties

In this section, we prove simple properties and identities of RBFs.
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}.

Consider any arrival sequence.
Let [tsk] be any task.
  Variable tsk : Task.

Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
Let's define some local names for clarity.
We prove that [task_rbf 0] is equal to 0.
  Lemma task_rbf_0_zero:
    task_rbf 0 = 0.

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

1 subgoal (ID 638)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  task_rbf 0 = 0

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


  Proof.
    rewrite /task_rbf /task_request_bound_function.

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

1 subgoal (ID 646)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  task_cost tsk * max_arrivals tsk 0 = 0

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


    apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.

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

1 focused subgoal
(shelved: 1) (ID 759)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  max_arrivals tsk 0 = 0

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


      by move: H_valid_arrival_curve ⇒ [T1 T2].

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

No more subgoals.

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


  Qed.

We prove that [task_rbf] is monotone.
  Lemma task_rbf_monotone:
    monotone task_rbf leq.

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

1 subgoal (ID 640)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  monotone task_rbf leq

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


  Proof.
    rewrite /monotone; intros ? ? LE.

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

1 subgoal (ID 646)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  x, y : duration
  LE : x <= y
  ============================
  task_rbf x <= task_rbf y

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


    rewrite /task_rbf /task_request_bound_function leq_mul2l.

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

1 subgoal (ID 659)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  x, y : duration
  LE : x <= y
  ============================
  (task_cost tsk == 0) || (max_arrivals tsk x <= max_arrivals tsk y)

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


    apply/orP; right.

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

1 subgoal (ID 685)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  x, y : duration
  LE : x <= y
  ============================
  max_arrivals tsk x <= max_arrivals tsk y

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


      by move: H_valid_arrival_curve ⇒ [_ T]; apply T.

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

No more subgoals.

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


  Qed.

Consider any job j of [tsk]. This guarantees that there exists at least one job of task [tsk].
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_task j = tsk.

Then we prove that [task_rbf 1] is greater than or equal to task cost.
  Lemma task_rbf_1_ge_task_cost:
    task_rbf 1 task_cost tsk.

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

1 subgoal (ID 649)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  ============================
  task_cost tsk <= task_rbf 1

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


  Proof.
    have ALT: n, n = 0 n > 0
      by clear; intros n; destruct n; [left | right].

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

1 subgoal (ID 668)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  ALT : forall n : nat, n = 0 \/ 0 < n
  ============================
  task_cost tsk <= task_rbf 1

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


    specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.

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

1 subgoal (ID 679)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ============================
  task_cost tsk <= task_rbf 1

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


    rewrite leqNgt; apply/negP; intros CONTR.

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

1 subgoal (ID 707)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ============================
  False

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


    move: H_is_arrival_curveARRB.

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

1 subgoal (ID 709)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  ============================
  False

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


    specialize (ARRB (job_arrival j) (job_arrival j + 1)).

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

1 subgoal (ID 715)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : job_arrival j <= job_arrival j + 1 ->
         number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <=
         max_arrivals tsk (job_arrival j + 1 - job_arrival j)
  ============================
  False

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


    feed ARRB; first by rewrite leq_addr.

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

1 subgoal (ID 721)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <=
         max_arrivals tsk (job_arrival j + 1 - job_arrival j)
  ============================
  False

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


    rewrite addKn in ARRB.

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

1 subgoal (ID 757)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  ============================
  False

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


    move: CONTR; rewrite /task_rbf /task_request_bound_function; moveCONTR.

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

1 subgoal (ID 768)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  CONTR : task_cost tsk * max_arrivals tsk 1 < task_cost tsk
  ============================
  False

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


    move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move ⇒ /andP [_ CONTR].

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

1 subgoal (ID 822)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  CONTR : max_arrivals tsk 1 < 1
  ============================
  False

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


    move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move ⇒ /eqP CONTR.

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

1 subgoal (ID 874)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  CONTR : max_arrivals tsk 1 = 0
  ============================
  False

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


    move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move ⇒ /negP T; apply: T.

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

1 subgoal (ID 916)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  0 < number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + 1)

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


    rewrite /number_of_task_arrivals -has_predT.

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

1 subgoal (ID 927)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  has predT
    (task_arrivals_between arr_seq tsk (job_arrival j) (job_arrival j + 1))

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


    rewrite /task_arrivals_between.

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

1 subgoal (ID 934)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  has predT
    [seq j0 <- arrivals_between arr_seq (job_arrival j) (job_arrival j + 1)
       | job_task j0 == tsk]

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


    apply/hasP; j; last by done.

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

1 subgoal (ID 964)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j
    \in [seq j0 <- arrivals_between arr_seq (job_arrival j)
                     (job_arrival j + 1)
           | job_task j0 == tsk]

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


    rewrite /arrivals_between addn1 big_nat_recl; last by done.

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

1 subgoal (ID 980)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j
    \in [seq j0 <- arrivals_at arr_seq (job_arrival j) ++
                   \cat_(job_arrival j<=i<job_arrival j|true)
                    arrivals_at arr_seq (succn i)
           | job_task j0 == tsk]

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


    rewrite big_geq ?cats0; last by done.

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

1 subgoal (ID 996)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j \in [seq j0 <- arrivals_at arr_seq (job_arrival j) | job_task j0 == tsk]

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


    rewrite mem_filter.

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

1 subgoal (ID 1006)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  (job_task j == tsk) && (j \in arrivals_at arr_seq (job_arrival j))

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


    apply/andP; split.

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

2 subgoals (ID 1032)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  job_task j == tsk

subgoal 2 (ID 1033) is:
 j \in arrivals_at arr_seq (job_arrival j)

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


    - by apply/eqP.

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

1 subgoal (ID 1033)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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


    - move: H_j_arrives ⇒ [t ARR].

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

1 subgoal (ID 1073)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  t : instant
  ARR : j \in arrivals_at arr_seq t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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


      move: (ARR) ⇒ CONS.

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

1 subgoal (ID 1075)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  t : instant
  ARR, CONS : j \in arrivals_at arr_seq t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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


      apply H_arrival_times_are_consistent in CONS.

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

1 subgoal (ID 1076)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  t : instant
  ARR : j \in arrivals_at arr_seq t
  CONS : job_arrival j = t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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


      by rewrite CONS.

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

No more subgoals.

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


  Qed.

End RequestBoundFunctions.