diff --git a/analysis/abstract/IBF/task.v b/analysis/abstract/IBF/task.v
index 564378bba1048db5e9f848c6b1f03810018ac205..e0da8be375623e196019f55b9508808dbfb5b57a 100644
--- a/analysis/abstract/IBF/task.v
+++ b/analysis/abstract/IBF/task.v
@@ -136,9 +136,8 @@ Section TaskIBFtoJobIBF.
   (** We assume that the schedule is work-conserving. *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-  (** Let's define some local names for clarity. *)
+  (** Let us abbreviate task [tsk]'s RBF for clarity. *)
   Let task_rbf := task_request_bound_function tsk.
-  Let arrivals_between := arrivals_between arr_seq.
 
   (** When assuming sequential tasks, we need to introduce an
       additional hypothesis to ensure that the values of interference
@@ -174,7 +173,7 @@ Section TaskIBFtoJobIBF.
       job_cost j > 0 ->
       busy_interval sched j t1 t2 ->
       task_workload_between arr_seq tsk 0 t1
-      = task_service_of_jobs_in sched tsk (arrivals_between 0 t1) 0 t1.
+      = task_service_of_jobs_in sched tsk (arrivals_between arr_seq 0 t1) 0 t1.
 
   (** To prove the reduction from [task_IBF] to [job_IBF], we need to
       ensure that the scheduling policy, interference, and interfering
@@ -303,7 +302,7 @@ Section TaskIBFtoJobIBF.
               1]. *)
           Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_idle :
             interference j t + service_at sched j t
-            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
               + task_interference arr_seq sched j t.
           Proof.
             replace (service_of_jobs_at _ _ _ _) with 0; last first.
@@ -336,7 +335,7 @@ Section TaskIBFtoJobIBF.
               1]. *)
           Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_task:
             interference j t + service_at sched j t
-            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
               + task_interference arr_seq sched j t.
           Proof.
             have ARRs : arrives_in arr_seq j'.
@@ -373,7 +372,7 @@ Section TaskIBFtoJobIBF.
               1]. *)
           Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_job :
             interference j t + service_at sched j t
-            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
               + task_interference arr_seq sched j t.
           Proof.
             rewrite /task_interference /cond_interference.
@@ -438,7 +437,7 @@ Section TaskIBFtoJobIBF.
               service_at = 1], we get the inequality to [1 ≤ 1]. *)
           Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_j :
             interference j t + service_at sched j t
-            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+            <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
               + task_interference arr_seq sched j t.
           Proof.
             rewrite interference_and_service_eq_1 -addn1 addnC leq_add //.
@@ -467,7 +466,7 @@ Section TaskIBFtoJobIBF.
             [task_iterference tsk t]. *)
         Lemma interference_plus_sched_le_serv_of_task_plus_task_interference:
           interference j t + service_at sched j t
-          <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+          <= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
             + task_interference arr_seq sched j t.
         Proof.
           rewrite /task_interference /cond_interference.
@@ -489,17 +488,17 @@ Section TaskIBFtoJobIBF.
       (** Next we prove cumulative version of the lemma above. *)
       Lemma cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference:
         cumulative_interference j t1 (t1 + x)
-        <= (task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
+        <= (task_service_of_jobs_in sched tsk (arrivals_between arr_seq t1 (t1 + A + ε)) t1 (t1 + x)
            - service_during sched j t1 (t1 + x)) + cumul_task_interference arr_seq sched j t1 (t1 + x).
       Proof.
-        have j_is_in_arrivals_between: j \in arrivals_between t1 (t1 + A + ε).
+        have j_is_in_arrivals_between: j \in arrivals_between arr_seq t1 (t1 + A + ε).
         { eapply arrived_between_implies_in_arrivals => //.
           by apply/andP; split; last rewrite /A subnKC // addn1.
         }
         rewrite /task_service_of_jobs_in /service_of_jobs.task_service_of_jobs_in /service_of_jobs exchange_big //=.
         rewrite -(leq_add2r (\sum_(t1 <= t < (t1 + x)) service_at sched j t)).
         rewrite [X in _ <= X]addnC addnA subnKC; last first.
-        { rewrite (exchange_big _ _ (arrivals_between _ _)) /= (big_rem j) //=.
+        { rewrite (exchange_big _ _ (arrivals_between _ _ _)) /= (big_rem j) //=.
           by rewrite H_job_of_tsk leq_addr. }
         rewrite -big_split -big_split //=.
         rewrite big_nat_cond [X in _ <= X]big_nat_cond leq_sum //; move => t /andP [NEQ _].
@@ -509,16 +508,16 @@ Section TaskIBFtoJobIBF.
       (** As the next step, the service terms in the inequality above
           can be upper-bound by the workload terms. *)
       Lemma serv_of_task_le_workload_of_task_plus:
-        task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
+        task_service_of_jobs_in sched tsk (arrivals_between arr_seq t1 (t1 + A + ε)) t1 (t1 + x)
         - service_during sched j t1 (t1 + x) + cumul_task_interference arr_seq sched j t1 (t1 + x)
         <= (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
           + cumul_task_interference arr_seq sched j t1 (t1 + x).
       Proof.
-        have j_is_in_arrivals_between: j \in arrivals_between t1 (t1 + A + ε).
+        have j_is_in_arrivals_between: j \in arrivals_between arr_seq t1 (t1 + A + ε).
         { eapply arrived_between_implies_in_arrivals => //.
           by apply/andP; split; last rewrite /A subnKC // addn1. }
         rewrite leq_add2r.
-        rewrite /task_workload /task_service_of_jobs_in/task_service_of_jobs_in/service_of_jobs.
+        rewrite /task_workload_between/task_service_of_jobs_in/task_service_of_jobs_in/service_of_jobs.
         rewrite (big_rem j) ?[X in _ <= X - _](big_rem j) //=; auto using j_is_in_arrivals_between.
         rewrite H_job_of_tsk addnC -addnBA// [X in _ <= X - _]addnC -addnBA//.
         rewrite !subnn !addn0.
@@ -536,7 +535,7 @@ Section TaskIBFtoJobIBF.
           + cumul_task_interference arr_seq sched j t1 (t1 + x).
       Proof.
         by apply leq_trans with
-          (task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
+          (task_service_of_jobs_in sched tsk (arrivals_between arr_seq t1 (t1 + A + ε)) t1 (t1 + x)
            - service_during sched j t1 (t1 + x)
            + cumul_task_interference arr_seq sched j t1 (t1 + x));
         [ apply cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference
@@ -552,7 +551,7 @@ Section TaskIBFtoJobIBF.
       <= (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference arr_seq sched j t1 (t1 + x).
     Proof.
       set (y := t1 + x) in *.
-      have IN: j \in arrivals_between t1 (t1 + A + ε).
+      have IN: j \in arrivals_between arr_seq t1 (t1 + A + ε).
       { apply: arrived_between_implies_in_arrivals => //.
         by apply/andP; split; last rewrite /A subnKC // addn1. }
       apply leq_trans with (
diff --git a/analysis/abstract/ideal/abstract_seq_rta.v b/analysis/abstract/ideal/abstract_seq_rta.v
index 0783e0855e7d7524827acdf84705346cf98abdc9..c4791653ae49fabdb96c1585d3e2714a87884f24 100644
--- a/analysis/abstract/ideal/abstract_seq_rta.v
+++ b/analysis/abstract/ideal/abstract_seq_rta.v
@@ -105,9 +105,8 @@ Section Sequential_Abstract_RTA.
   Hypothesis H_task_interference_is_bounded :
     task_interference_is_bounded_by arr_seq sched tsk task_IBF.
 
-  (** Let's define some local names for clarity. *)
+  (** Let us abbreviate task [tsk]'s RBF for clarity. *)
   Let task_rbf := task_request_bound_function tsk.
-  Let arrivals_between := arrivals_between arr_seq.
 
   (** Given any job [j] of task [tsk] that arrives exactly [A] units
       after the beginning of the busy interval, the bound on the total
diff --git a/analysis/abstract/restricted_supply/bounded_bi/aux.v b/analysis/abstract/restricted_supply/bounded_bi/aux.v
index 6c5134a00d8b488406ec76fb918d5c3a12fd40b0..555ce0a923b696277603f02a1682e590f6899c79 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/aux.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/aux.v
@@ -96,7 +96,8 @@ Section BoundedBusyIntervalsAux.
   Lemma service_lt_workload_in_busy :
     forall t,
       t1 < t < t2 ->
-      service_of_hep_jobs arr_seq sched j t1 t < workload_of_hep_jobs arr_seq j t1 t.
+      service_of_hep_jobs arr_seq sched j t1 t
+      < workload_of_hep_jobs arr_seq j t1 t.
   Proof.
     move=> t /andP [LT1 LT2]; move: (H_busy_prefix) => PREF.
     move_neq_up LE.
@@ -154,7 +155,7 @@ Section BoundedBusyIntervalsAux.
     }
     rewrite cumulative_interfering_workload_split // cumulative_interference_split //.
     rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //; last by apply PREF.
-    rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _ )]addnC.
+    rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _)]addnC.
     rewrite workload_job_and_ahep_eq_workload_hep //.
     rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.
     rewrite service_plus_ahep_eq_service_hep //; last by move: PREF => [_ [_ [_ /andP [A B]]]].
diff --git a/analysis/abstract/restricted_supply/bounded_bi/edf.v b/analysis/abstract/restricted_supply/bounded_bi/edf.v
index 0eb61050f3abe0d1da0344634afeb0afbdee6915..e51401d7b39613f0d9f690e1225de1ff2e3b418e 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/edf.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/edf.v
@@ -174,7 +174,9 @@ Section BoundedBusyIntervals.
           by rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline; lia. }
         erewrite workload_of_jobs_partitioned_by_tasks with (ts := undup ts).
         + eapply leq_trans; first by apply sum_le_subseq, undup_subseq.
-          apply leq_sum_seq => tsk_o INo HEP; rewrite -(leqRW (workload_le_rbf' _ _ _ _ _ _ _)) //.
+          apply leq_sum_seq => tsk_o INo HEP.
+          set P := (fun j' : Job => hep_job j' jlp && (job_task j' == tsk_o)).
+          rewrite -(leqRW (rbf_spec' _ _ P _ _ _ _ _)) /P //; last by move=> ? /andP[].
           have [A | B] := (leqP δ (task_deadline (job_task jlp) - task_deadline tsk_o)).
           { by apply workload_of_jobs_reduce_range; lia. }
           { have EQt: forall a b, a = b -> a <= b; [by lia | apply: EQt].
diff --git a/analysis/definitions/request_bound_function.v b/analysis/definitions/request_bound_function.v
index b80aa9b95aaf469ad10678dadb62df916c6ec5cb..3f9284c74ce97e85a32f2581b595b932e32862fe 100644
--- a/analysis/definitions/request_bound_function.v
+++ b/analysis/definitions/request_bound_function.v
@@ -10,91 +10,57 @@ Require Export prosa.util.sum.
 
 Section TaskWorkloadBoundedByArrivalCurves.
 
-  (** Consider any type of tasks ... *)
+  (** Consider any type of task characterized by a WCET bound and an arrival curve. *)
   Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-
-  (** ... and any type of jobs associated with these tasks, where each task has
-      a cost. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobCost Job}.
-
-  (** Also assume an FP policy that indicates a higher-or-equal priority
-      relation. *)
-  Context `{FP_policy Task}.
-
-  (** Let [MaxArrivals] denote any function that takes a task and an interval length
-      and returns the associated number of job arrivals of the task. *)
-  Context `{MaxArrivals Task}.
+  Context `{TaskCost Task} `{MaxArrivals Task}.
 
   (** ** RBF of a Single Task *)
 
-  (** In this section, we define a bound for the workload of a single task
-      under uni-processor FP scheduling. *)
-  Section SingleTask.
+  (** We define the classic notion of an RBF, which for a given task [tsk]
+      and interval length [Δ], bounds the maximum cumulative processor demand
+      of all jobs released by [tsk] in any interval of length [Δ]. *)
+  Definition task_request_bound_function (tsk : Task) (Δ : duration) :=
+    task_cost tsk * max_arrivals tsk Δ.
 
-    (** Consider any task [tsk] that is to be scheduled in an interval of length delta. *)
-    Variable tsk : Task.
-    Variable delta : duration.
+  (** ** Total RBF of Multiple Tasks *)
 
-    (** We define the following workload bound for the task. *)
-    Definition task_request_bound_function :=
-      task_cost tsk * max_arrivals tsk delta.
+  (** Next, we extend the notion of an RBF to multiple tasks in the obvious way. *)
 
-  End SingleTask.
+  (** Consider a set of tasks [ts]. *)
+  Variable ts : seq Task.
 
-  (** ** Total RBF of Multiple Tasks *)
+  (** The joint total RBF of all tasks in [ts] is simply the sum of each task's RBF. *)
+  Definition total_request_bound_function (Δ : duration) :=
+    \sum_(tsk <- ts) task_request_bound_function tsk Δ.
+
+  (** For convenience, we additionally introduce specialized notions of total RBF for use 
+      under FP scheduling that consider only certain tasks.
+      relation. *)
+  Context `{FP_policy Task}.
 
-  (** In this section, we define a bound for the workload of multiple tasks. *)
-  Section AllTasks.
-
-    (** Consider a task set ts... *)
-    Variable ts : list Task.
-
-    (** ...and let [tsk] be any task in task set. *)
-    Variable tsk : Task.
-
-    (** Let delta be the length of the interval of interest. *)
-    Variable delta : duration.
-
-    (** Recall the definition of higher-or-equal-priority task for FP scheduling. *)
-    Let is_hep_task tsk_other := hep_task tsk_other tsk.
-    Let is_other_hep_task tsk_other := hep_task tsk_other tsk && (tsk_other != tsk).
-    Let is_hp_task tsk_other := hp_task tsk_other tsk.
-    Let is_ep_task tsk_other := ep_task tsk_other tsk.
-
-    (** Using the sum of individual workload bounds, we define the following
-        bound for the total workload of tasks in any interval of length
-        delta. *)
-    Definition total_request_bound_function :=
-      \sum_(tsk <- ts) task_request_bound_function tsk delta.
-
-    (** Similarly, we define the following bound for the total workload of
-        tasks of higher-or-equal priority (with respect to [tsk]) in any interval
-        of length delta. *)
-    Definition total_hep_request_bound_function_FP :=
-      \sum_(tsk_other <- ts | is_hep_task tsk_other)
-       task_request_bound_function tsk_other delta.
-
-    (** We also define a bound for the total workload of higher-or-equal-priority
-        tasks other than [tsk] in any interval of length [delta]. *)
-    Definition total_ohep_request_bound_function_FP :=
-      \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
-        task_request_bound_function tsk_other delta.
-
-    (** We also define a bound for the total workload of higher-or-equal-priority
-        tasks other than [tsk] in any interval of length [delta]. *)
-    Definition total_ep_request_bound_function_FP :=
-      \sum_(tsk_other <- ts | is_ep_task tsk_other)
-        task_request_bound_function tsk_other delta.
-
-    (** Finally, we define a bound for the total workload of higher-priority
-        tasks in any interval of length delta. *)
-    Definition total_hp_request_bound_function_FP :=
-      \sum_(tsk_other <- ts | is_hp_task tsk_other)
-       task_request_bound_function tsk_other delta.
-
-  End AllTasks.
+  (** We define the following bound for the total workload of
+      tasks of higher-or-equal priority (with respect to [tsk]) in any interval
+      of length Δ. *)
+  Definition total_hep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | hep_task tsk_other tsk)
+     task_request_bound_function tsk_other Δ.
+
+  (** We also define a bound for the total workload of higher-or-equal-priority
+      tasks other than [tsk] in any interval of length [Δ]. *)
+  Definition total_ohep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | hep_task tsk_other tsk && (tsk_other != tsk))
+      task_request_bound_function tsk_other Δ.
+
+  (** We also define a bound for the total workload of higher-or-equal-priority
+      tasks other than [tsk] in any interval of length [Δ]. *)
+  Definition total_ep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | ep_task tsk_other tsk)
+      task_request_bound_function tsk_other Δ.
+
+  (** Finally, we define a bound for the total workload of higher-priority
+      tasks in any interval of length [Δ]. *)
+  Definition total_hp_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | hp_task tsk_other tsk)
+     task_request_bound_function tsk_other Δ.
 
 End TaskWorkloadBoundedByArrivalCurves.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index 4eccd7890dcfe492dc0a91026767448c07e40eaf..c1064028084e57a43ac41802cc7240d6c8e05256 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -113,12 +113,8 @@ Section BusyIntervalExistence.
   (** We now introduce the central assumption from which we deduce the existence
       of a busy interval. *)
 
-  (** To this end, recall the notion of workload of all jobs released in a
-      given interval <<[t1, t2)>>... *)
-  Let total_workload t1 t2 :=
-    workload_of_jobs predT (arrivals_between arr_seq t1 t2).
-
-  (** ... and total service of jobs within some time interval <<[t1, t2)>>. *)
+  (** To this end, recall the notion of the total service of all jobs within
+      some time interval <<[t1, t2)>>. *)
   Let total_service t1 t2 :=
     service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2.
 
@@ -133,7 +129,7 @@ Section BusyIntervalExistence.
   Hypothesis H_workload_is_bounded :
     forall t,
       no_carry_in arr_seq sched t ->
-      blackout_during sched t (t + Δ) + total_workload t (t + Δ) <= Δ.
+      blackout_during sched t (t + Δ) + total_workload_between arr_seq t (t + Δ) <= Δ.
 
   (** In the following, we also require a unit-speed processor. *)
   Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
@@ -226,7 +222,7 @@ Section BusyIntervalExistence.
       Proof.
         rewrite /total_service => EQserv s ARR BEF.
         move: (H_workload_is_bounded t) => WORK.
-        have EQ: total_workload 0 (t + Δ)
+        have EQ: total_workload_between arr_seq 0 (t + Δ)
                  = service_of_jobs sched predT (arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ);
           last exact: workload_eq_service_impl_all_jobs_have_completed.
         have CONSIST: consistent_arrival_times arr_seq by [].
@@ -242,7 +238,7 @@ Section BusyIntervalExistence.
                         by apply: (in_arrivals_implies_arrived_between arr_seq). }
         apply/eqP; rewrite eqn_leq; apply/andP; split;
           last by apply: service_of_jobs_le_workload.
-        rewrite /total_workload (workload_of_jobs_cat arr_seq t);
+        rewrite /total_workload_between/total_workload (workload_of_jobs_cat arr_seq t);
           last by apply/andP; split; [|rewrite leq_addr].
         - rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t) //;
             last by apply/andP; split; [|rewrite leq_addr].
diff --git a/analysis/facts/busy_interval/existence.v b/analysis/facts/busy_interval/existence.v
index e2184fa921590f148fad1912e445712de4561155..2582a5d48114e21f6afea659b2c5c1ef4bd5b1ef 100644
--- a/analysis/facts/busy_interval/existence.v
+++ b/analysis/facts/busy_interval/existence.v
@@ -348,7 +348,7 @@ Section ExistsBusyIntervalJLFP.
         a given interval <<[t1, t2)>> that have higher-or-equal
         priority w.r.t. the job [j] being analyzed. *)
     Let hp_workload t1 t2 :=
-      workload_of_higher_or_equal_priority_jobs j (arrivals_between arr_seq t1 t2).
+      workload_of_hep_jobs arr_seq j t1 t2.
 
     (** With regard to the jobs with higher-or-equal priority that are released
            in a given interval <<[t1, t2)>>, we also recall the service received by these
@@ -516,7 +516,7 @@ Section ExistsBusyIntervalJLFP.
             set l := arrivals_between arr_seq t1 (t1 + delta).
             set hep := hep_job.
             unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs,
-            hp_workload, workload_of_higher_or_equal_priority_jobs, workload_of_jobs.
+            hp_workload, workload_of_hep_jobs, workload_of_jobs.
             fold l hep.
             move: (PREFIX) => [_ [QUIET _]].
             move: (NOTQUIET) => NOTQUIET'.
diff --git a/analysis/facts/model/dbf.v b/analysis/facts/model/dbf.v
index 96830fd44c5fbc828f17b88ccfab00d59f253516..16b90904c4a7699dc8f2264146457ba124670434 100644
--- a/analysis/facts/model/dbf.v
+++ b/analysis/facts/model/dbf.v
@@ -87,15 +87,15 @@ Section ProofDemandBoundDefinition.
   Proof.
     move=> tsk t delta IN0.
     have ->: task_demand_within tsk t (t + delta)
-      = task_workload_between arr_seq tsk t (t + (delta - (task_deadline tsk - 1))).
-      { rewrite /task_demand_within/task_workload_between/task_workload/workload_of_jobs.
-        under eq_bigl do rewrite andbC.
-        rewrite -big_filter.
-        move: (task_arrivals_with_deadline_within_eq tsk t delta).
-        rewrite /task_arrivals_with_deadline_within/task_arrivals_between => ->.
-        by rewrite big_filter. }
-    rewrite /task_demand_bound_function/task_workload_between/task_workload.
-    by apply workload_le_rbf.
+             = task_workload tsk (arrivals_between arr_seq t (t + (delta - (task_deadline tsk - 1)))).
+    { rewrite /task_demand_within/task_workload/workload_of_jobs.
+      under eq_bigl do rewrite andbC.
+      rewrite -big_filter.
+      move: (task_arrivals_with_deadline_within_eq tsk t delta).
+      rewrite /task_arrivals_with_deadline_within/task_arrivals_between => ->.
+      by rewrite big_filter. }
+    rewrite /task_demand_bound_function/task_workload.
+    by apply: rbf_spec.
   Qed.
 
   (** We also prove that [task_demand_within] is less than shifted RBF. *)
@@ -119,43 +119,15 @@ Section ProofDemandBoundDefinition.
   (** Assume that all jobs come from the task set [ts]. *)
   Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
 
-  (** We relate [total_demand_within] to the sum of each task's demand [task_demand_within]. *)
-  Lemma total_demand_within_le_sum_over_partitions:
-    forall (t : instant) (delta : duration),
-      total_demand_within t (t + delta) <= \sum_(tsk <- ts) task_demand_within tsk t (t + delta).
-  Proof.
-    move=> t delta.
-    rewrite /total_demand_within/task_demand_within.
-    rewrite /workload_of_jobs.
-    apply sum_over_partitions_le.
-    move=> j' IN ?.
-    apply H_all_jobs_from_taskset.
-    by apply in_arrivals_implies_arrived in IN.
-  Qed.
-
-  (** Here we prove a stronger version of the above lemma by assuming that the task set [ts] is indeed a set. *)
-  Lemma total_demand_within_partitioned_by_tasks:
-    forall (t : instant) (delta : duration),
-      uniq ts ->
-      total_demand_within t (t + delta) = \sum_(tsk <- ts) task_demand_within tsk t (t + delta).
-  Proof.
-    move=> t delta UniqTS.
-    rewrite /total_demand_within/task_demand_within.
-    rewrite /job_of_task.
-    apply workload_of_jobs_partitioned_by_tasks => //=.
-    move=> j' IN.
-    apply H_all_jobs_from_taskset.
-    by apply in_arrivals_implies_arrived in IN.
-  Qed.
-
   (** Finally we establish that [total_demand_within] is bounded by [total_demand_bound_function]. *)
   Lemma total_demand_within_le_total_dbf:
     forall (t : instant) (delta : duration),
       total_demand_within t (t + delta) <= total_demand_bound_function ts delta.
   Proof.
     move=> t delta.
-    apply (@leq_trans (\sum_(tsk <- ts) task_demand_within tsk t (t + delta)));
-      first by apply total_demand_within_le_sum_over_partitions.
+    apply (@leq_trans (\sum_(tsk <- ts) task_demand_within tsk t (t + delta))).
+    { apply workload_of_jobs_le_sum_over_partitions => //.
+      move=> j IN; by apply in_arrivals_implies_arrived in IN. }
     rewrite /total_demand_bound_function.
     apply leq_sum_seq => tsk' tsk_IN P_tsk.
     by apply task_demand_within_le_task_dbf.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 2846036e0c0d8f211561d6751f3193c54dfc0427..ff828aaa777eab25fe74794b1e7e85fd5bb61548 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -1,24 +1,23 @@
 Require Export prosa.analysis.facts.model.workload.
 Require Export prosa.analysis.facts.model.arrival_curves.
+Require Export prosa.analysis.facts.model.task_cost.
 Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.definitions.request_bound_function.
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.util.tactics.
 Require Export prosa.analysis.definitions.workload.bounded.
 
-(** * Facts about Request Bound Functions (RBFs) *)
+(** * Facts about Request-Bound Functions (RBFs) *)
 
-(** In this file, we prove some lemmas about request bound functions. *)
+(** In this file, we prove some lemmas about RBFs. *)
 
 (** ** RBF is a Bound on Workload *)
 
-(** First, we show that a task's RBF is indeed an upper bound on its
-    workload. *)
-Section ProofWorkloadBound.
+Section ProofRequestBoundFunction.
 
-  (** Consider any type of tasks ... *)
+  (** Consider any type of tasks characterized by WCETs and arrival curves ... *)
   Context {Task : TaskType}.
-  Context `{TaskCost Task}.
+  Context `{TaskCost Task} `{MaxArrivals Task}.
 
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
@@ -26,252 +25,241 @@ Section ProofWorkloadBound.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (** Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
+  (** Consider any valid arrival sequence ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
 
-  (** ... any schedule corresponding to this arrival sequence, ... *)
+  (** ... and any schedule corresponding to this arrival sequence. *)
   Context {PState : ProcessorState Job}.
   Variable sched : schedule PState.
-  Hypothesis H_jobs_come_from_arrival_sequence :
-    jobs_come_from_arrival_sequence sched arr_seq.
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
 
-  (** ... and an FP policy that indicates a higher-or-equal priority relation. *)
-  Context `{FP_policy Task}.
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
 
-  (** Further, consider a task set [ts]... *)
-  Variable ts : seq Task.
+  (** In this section, we establish that a task's RBF is indeed an upper bound
+      on the task's workload. *)
+  Section RBF.
 
-  (** ... and let [tsk] be any task in [ts]. *)
-  Variable tsk : Task.
-  Hypothesis H_tsk_in_ts : tsk \in ts.
+    (** Consider a given task [tsk]. *)
+    Variable tsk : Task.
 
-  (** Assume that the job costs are no larger than the task costs ... *)
-  Hypothesis H_valid_job_cost :
-    arrivals_have_valid_job_costs arr_seq.
+    (** First, as a stepping stone, we observe that any sequence of jobs of the
+        task jointly satisfy the task's WCET. *)
+    Lemma task_workload_between_bounded :
+      forall t1 t2,
+        task_workload_between arr_seq tsk t1 t2
+        <= task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2.
+    Proof.
+      move=> t Δ.
+      rewrite /number_of_task_arrivals/task_arrivals_between.
+      rewrite /task_workload_between/task_workload/workload_of_jobs -big_filter.
+      apply: sum_job_costs_bounded.
+      move=> j /[! mem_filter ] /andP [TSK IN]; apply /andP; split => //.
+      by apply/H_valid_job_cost/in_arrivals_implies_arrived.
+    Qed.
 
-  (** ... and that all jobs come from the task set. *)
-  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+    (** Next, suppose that task [tsk] respects its arrival curve [max_arrivals]. *)
+    Hypothesis H_tsk_arrivals_bounded : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
-  (** Let [max_arrivals] be any arrival bound for task-set [ts]. *)
-  Context `{MaxArrivals Task}.
-  Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
+    (** From this assumption, we establish the RBF spec: In any interval of any
+        length, the RBF upper-bounds the task's actual workload. *)
+    Lemma rbf_spec :
+      forall t Δ,
+        task_workload_between arr_seq tsk t (t + Δ)
+        <= task_request_bound_function tsk Δ.
+    Proof.
+      move=> t Δ.
+      apply: leq_trans; first by apply: task_workload_between_bounded.
+      rewrite /task_request_bound_function.
+      rewrite leq_mul2l; apply/orP; right.
+      rewrite -{2}[Δ](addKn t).
+      by apply/H_tsk_arrivals_bounded/leq_addr.
+    Qed.
 
-  (** Next, recall the notions of total workload of jobs... *)
-  Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).
+  End RBF.
 
-  (** ... and the workload of jobs of the same task as job j. *)
-  Let task_workload t1 t2 :=
-    workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
+  (** In this section, we prove a trivial corollary stating that the RBF still
+      upper-bounds the workload when considering only a subset of a task's jobs
+      (namely those satisfying a filter predicate). *)
+  Section SubsetOfJobs.
 
-  (** Finally, let us define some local names for clarity. *)
-  Let rbf := task_request_bound_function.
-  Let total_rbf := total_request_bound_function ts.
-  Let total_hep_rbf := total_hep_request_bound_function_FP ts.
-  Let total_ohep_rbf := total_ohep_request_bound_function_FP ts.
+    (** Consider any predicate [P] on jobs. *)
+    Variable P : pred Job.
 
-  (** In this section, we prove that the workload of all jobs is
-      no larger than the request bound function. *)
-  Section WorkloadIsBoundedByRBF.
+    (** Consider any task [tsk] that respects its arrival curve [max_arrivals] *)
+    Variable tsk : Task.
+    Hypothesis H_tsk_arrivals_bounded : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
-    (** Consider any time [t] and any interval of length [Δ]. *)
-    Variable t : instant.
-    Variable Δ : instant.
+    (** Assume that all jobs that satisfy [P] come from task [tsk]. *)
+    Hypothesis H_jobs_of_tsk : forall j, P j -> job_of_task tsk j.
 
-    (** 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 + Δ)
-      <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + Δ).
+    (** Trivially, the workload of jobs from task [tsk] that satisfy the
+        predicate [P] is bounded by the task's RBF. *)
+    Corollary rbf_spec' :
+      forall t Δ,
+        workload_of_jobs P
+          (arrivals_between arr_seq t (t + Δ))
+        <= task_request_bound_function tsk Δ.
     Proof.
-      rewrite /task_workload /workload_of_jobs/ number_of_task_arrivals
-              /task_arrivals_between -big_filter -sum1_size big_distrr big_filter.
-      destruct (task_arrivals_between arr_seq tsk t (t + Δ)) eqn:TASK.
-      { unfold task_arrivals_between in TASK.
-        by rewrite -big_filter !TASK !big_nil. }
-      { rewrite //= big_filter big_seq_cond [in X in _ <= X]big_seq_cond.
-        apply leq_sum.
-        move => j' /andP [IN TSKj'].
-        rewrite muln1.
-        move: TSKj' => /eqP TSKj'; rewrite -TSKj'.
-        apply H_valid_job_cost.
-        by apply in_arrivals_implies_arrived in IN. }
+      move=> t Δ.
+      apply: leq_trans; last by apply: rbf_spec.
+      rewrite /task_workload_between/task_workload/workload_of_jobs.
+      by apply leq_sum_seq_pred.
     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 + Δ) <= rbf tsk Δ.
-    Proof.
-      eapply leq_trans; first by apply task_workload_le_num_of_arrivals_times_cost.
-      rewrite leq_mul2l; apply/orP; right.
-      rewrite -{2}[Δ](addKn t).
-      by apply H_is_arrival_bound; last rewrite leq_addr.
-    Qed.
+  End SubsetOfJobs.
 
-    (** 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 + Δ) <= total_rbf Δ.
-    Proof.
-      set l := arrivals_between arr_seq t (t + Δ).
-      apply (@leq_trans (\sum_(tsk' <- ts) (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).
-      { rewrite /total_workload.
-        have EXCHANGE := exchange_big_dep predT.
-        rewrite EXCHANGE //=; clear EXCHANGE.
-        rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
-        apply leq_sum; move => j0 /andP [IN0 HP0].
-        rewrite big_mkcond (big_rem (job_task j0)) /=.
-        - by rewrite eq_refl; apply leq_addr.
-        - by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset. }
-      apply leq_sum_seq; intros tsk0 INtsk0 HP0.
-      apply (@leq_trans (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).
-      { rewrite -sum1_size big_distrr /= big_filter -/l /workload_of_jobs muln1.
-        apply leq_sum_seq => j0 IN0 /eqP <-.
-        apply H_valid_job_cost.
-        by apply in_arrivals_implies_arrived in IN0. }
-      { rewrite leq_mul2l; apply/orP; right.
-        rewrite -{2}[Δ](addKn t).
-        by apply H_is_arrival_bound; last rewrite leq_addr. }
-    Qed.
+  (** Now, consider a task set [ts] ... *)
+  Variable ts : seq Task.
 
-    (** Next, we consider any job [j] of [tsk]. *)
-    Variable j : Job.
-    Hypothesis H_job_of_tsk : job_of_task tsk j.
+  (** ... and assume that all jobs come from the task set. *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
 
-    (** We prove that the sum of job cost of jobs whose corresponding
-        task satisfies a predicate [pred] is bounded by the RBF of
-        these tasks. *)
-    Lemma sum_of_jobs_le_sum_rbf :
-      forall (pred : pred Task),
-        \sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred (job_task j'))
-         job_cost j' <=
-          \sum_(tsk' <- ts| pred tsk')
-           task_request_bound_function tsk' Δ.
-    Proof.
-      move => pred.
-      apply (@leq_trans (\sum_(tsk' <- filter pred ts)
-                           (\sum_(j' <-  arrivals_between arr_seq t (t + Δ)
-                                 | job_task j' == tsk') job_cost j'))).
-      - move: (H_job_of_tsk) => /eqP TSK.
-        rewrite [X in _ <= X]big_filter.
-        set P := fun x => pred (job_task x).
-        rewrite (exchange_big_dep P) //=; last by rewrite /P; move => ???/eqP->.
-        rewrite  /P /workload_of_jobs big_seq_cond [X in _ <= X]big_seq_cond.
-        apply leq_sum => j0 /andP [IN0 HP0].
-        rewrite big_mkcond (big_rem (job_task j0)).
-        + by rewrite HP0 andTb eq_refl; apply leq_addr.
-        + by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
-      - rewrite big_filter.
-        apply leq_sum_seq => tsk0 INtsk0 HP0.
-        apply (@leq_trans (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).
-        + rewrite -sum1_size big_distrr /= big_filter /workload_of_jobs.
-          rewrite  muln1  /arrivals_between /arrival_sequence.arrivals_between.
-          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
-          by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
-        + rewrite leq_mul2l; apply/orP; right.
-          rewrite -{2}[Δ](addKn t).
-          by apply H_is_arrival_bound; last by rewrite leq_addr.
-    Qed.
+  (** Assume that all tasks in the task set respect [max_arrivals]. *)
+  Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
 
-    (** Using lemma [sum_of_jobs_le_sum_rbf], we prove that the
-        workload of higher-or-equal priority jobs (w.r.t. task [tsk])
-        is no larger than the total request-bound function of
-        higher-or-equal priority tasks. *)
-    Lemma hep_workload_le_total_hep_rbf :
-      workload_of_hep_jobs arr_seq j t (t + Δ) <= total_hep_rbf tsk Δ.
+  (** Next, we prove that total workload is upper-bounded by the total RBF. *)
+  Lemma total_workload_le_total_rbf :
+    forall t Δ,
+      total_workload_between arr_seq t (t + Δ) <= total_request_bound_function ts Δ.
+  Proof.
+    move=> t Δ.
+    apply leq_trans with (n := \sum_(tsk <- ts) task_workload_between arr_seq tsk t (t + Δ)).
+    { apply: workload_of_jobs_le_sum_over_partitions => //.
+      move=> j IN; by apply in_arrivals_implies_arrived in IN. }
+    rewrite /total_request_bound_function.
+    apply leq_sum_seq => tsk' tsk_IN ?.
+    by apply rbf_spec.
+  Qed.
+
+  (** In this section, we prove a more general result about the workload of
+      arbitrary sets of jobs. *)
+  Section SumRBF.
+
+    (** Consider two predicates, one on jobs and one on tasks. *)
+    Variable pred1 : pred Job.
+    Variable pred2 : pred Task.
+
+    (** Assume that for all jobs satisfying [pred1], the task it belongs to
+        satisfies [pred2]. *)
+    Hypothesis H_also_satisfied : forall j, pred1 j -> pred2 (job_task j).
+
+    (** We prove that the workload of all jobs satisfying predicate [pred1] is
+        bounded by the sum of task RBFs over tasks that satisfy the predicate
+        [pred2]. *)
+    Lemma workload_of_jobs_bounded :
+      forall t Δ,
+        workload_of_jobs (pred1) (arrivals_between arr_seq t (t + Δ))
+        <= \sum_(tsk' <- ts | pred2 tsk') task_request_bound_function tsk' Δ.
     Proof.
-      rewrite /workload_of_hep_jobs /workload_of_jobs /total_hep_rbf /total_hep_request_bound_function_FP.
-      rewrite /another_task_hep_job /hep_job /FP_to_JLFP.
-      set (pred_task tsk_other := hep_task tsk_other tsk).
-      rewrite (eq_big (fun j=> pred_task (job_task j)) job_cost) //;
-              last by move=> j'; rewrite /pred_task; move: H_job_of_tsk => /eqP ->.
-      erewrite (eq_big pred_task); [|by done|by move=> tsk'; eauto].
-      by apply: sum_of_jobs_le_sum_rbf.
+      move=> t Δ.
+      rewrite /workload_of_jobs.
+      apply (@leq_trans (\sum_(tsk <- ts | pred2 tsk)
+                (\sum_(j <- arrivals_between arr_seq t (t + Δ) | (job_task j == tsk) && (pred1 j))
+                    job_cost j))).
+      { rewrite (exchange_big_dep pred1) //=;
+          last by move=> ? ? ? /andP[].
+        rewrite big_seq_cond [X in _ <= X]big_seq_cond.
+        rewrite leq_sum //= => j' /andP [IN' Pj'].
+        rewrite Pj'.
+        under eq_bigl do [rewrite andbA; rewrite andbT].
+        rewrite (big_rem (job_task j')) //=;
+          last by apply/H_all_jobs_from_taskset/in_arrivals_implies_arrived.
+        rewrite (H_also_satisfied _  Pj') eq_refl //=.
+        by apply leq_addr. }
+      { rewrite leq_sum_seq //=.
+        move=> tsk' tsk_in_ts' P_tsk'.
+        apply (@leq_trans (\sum_(j <- arrivals_between arr_seq t (t + Δ)
+                | job_task j == tsk') job_cost j)).
+        - rewrite leq_sum_seq_pred //=.
+          by move=> ? ? /andP[].
+        - exact: rbf_spec. }
     Qed.
 
-  End WorkloadIsBoundedByRBF.
+  End SumRBF.
 
-  (** We next prove that the higher-or-equal-priority workload of
-      tasks different from [tsk] is bounded by [total_ohep_rbf].
 
-      The [athep_workload_is_bounded] predicate allows the workload
-      bound to depend on two arguments: the relative offset [A]
-      (w.r.t. the beginning of the corresponding busy interval) of a
-      job to be analyzed and the length of an interval [Δ]. In the
-      case of FP and [total_ohep_rbf] function, the relative offset
-      ([A]) does not play a role and is therefore ignored. *)
-  Lemma athep_workload_le_total_ohep_rbf :
-    athep_workload_is_bounded
-      arr_seq sched tsk (fun (A Δ : duration) => total_ohep_rbf tsk Δ).
-  Proof.
-    move => j t1 Δ POS TSK _.
-    rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
-    rewrite /another_task_hep_job /hep_job /FP_to_JLFP.
-    set (pred_task tsk_other := hep_task tsk_other tsk && (tsk_other != tsk)).
-    rewrite (eq_big (fun j=> pred_task (job_task j)) job_cost) //;
-            last by move=> j'; rewrite /pred_task; move: TSK => /eqP ->.
-    erewrite (eq_big pred_task) => //.
-    by eapply sum_of_jobs_le_sum_rbf => //.
-  Qed.
+  (** Next, we establish bounds specific to fixed-priority scheduling. *)
+  Section FP.
 
-End ProofWorkloadBound.
+    (** Consider an arbitrary fixed-priority policy ... *)
+    Context {FP : FP_policy Task}.
 
-(** In this section, we show that total RBF is a bound on
-    higher-or-equal priority workload under any JLFP policy. *)
-Section TotalRBFBound.
+    (** ... and any given task. *)
+    Variable tsk : Task.
 
-  (** Consider any type of tasks ... *)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
+    (** The [athep_workload_is_bounded] predicate used below allows the workload
+        bound to depend on two arguments: the relative offset [A] (w.r.t. the
+        beginning of the corresponding busy interval) of a job to be analyzed
+        and the length of an interval [Δ]. In the case of FP scheduling, the
+        relative offset ([A]) does not play a role and is therefore ignored.
 
-  (**  ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
+        Let's abbreviate [total_ohep_request_bound_function_FP] such that the
+        [A] argument is ignored. *)
+    Let total_ohep_rbf (_A Δ : duration) :=
+          total_ohep_request_bound_function_FP ts tsk Δ.
 
-  (** Consider a JLFP policy that indicates a higher-or-equal priority
-      relation ... *)
-  Context `{JLFP_policy Job}.
+    (** We next prove that the higher-or-equal-priority workload of tasks
+        different from [tsk] is bounded by [total_ohep_rbf]. *)
+    Lemma athep_workload_le_total_ohep_rbf :
+      athep_workload_is_bounded arr_seq sched tsk total_ohep_rbf.
+    Proof.
+      move => j t1 Δ POS TSK _.
+      rewrite /workload_of_jobs /total_ohep_request_bound_function_FP.
+      rewrite /another_task_hep_job /hep_job /FP_to_JLFP.
+      apply: workload_of_jobs_bounded.
+      by move: TSK => /eqP ->.
+    Qed.
 
-  (** ... and any valid arrival sequence. *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+    (** Consider any job [j] of [tsk]. *)
+    Variable j : Job.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
 
-  (** Further, consider a task set [ts]. *)
-  Variable ts : seq Task.
+    (** Using lemma [workload_of_jobs_bounded], we prove that the
+        workload of higher-or-equal priority jobs (w.r.t. task [tsk])
+        is no larger than the total request-bound function of
+        higher-or-equal priority tasks. *)
+    Lemma hep_workload_le_total_hep_rbf :
+      forall t Δ,
+        workload_of_hep_jobs arr_seq j t (t + Δ)
+        <= total_hep_request_bound_function_FP ts tsk Δ.
+    Proof.
+      move=> t Δ.
+      apply workload_of_jobs_bounded.
+      rewrite /hep_job /FP_to_JLFP.
+      by move: H_job_of_tsk => /eqP <-.
+    Qed.
 
-  (** Assume that the job costs are no larger than the task costs ... *)
-  Hypothesis H_valid_job_cost :
-    arrivals_have_valid_job_costs arr_seq.
+  End FP.
 
-  (** ... and that all jobs come from the task set. *)
-  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+  (** In this section, we show that the total RBF is a bound on higher-or-equal
+      priority workload under any JLFP policy. *)
+  Section JLFP.
 
-  (** Let [max_arrivals] be any arrival bound for task set [ts]. *)
-  Context `{MaxArrivals Task}.
-  Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
+    (** Consider a JLFP policy that indicates a higher-or-equal priority
+        relation ... *)
+    Context `{JLFP_policy Job}.
 
-  (** Consider any time [t] and any interval of length [Δ]. *)
-  Variable t : instant.
-  Variable Δ : duration.
+    (** ... and any job [j]. *)
+    Variable j : Job.
 
-  (** Next, we consider any job [j]. *)
-  Variable j : Job.
+    (** A simple consequence of lemma [hep_workload_le_total_hep_rbf] is that
+        the workload of higher-or-equal priority jobs is bounded by the total
+        request-bound function. *)
+    Corollary hep_workload_le_total_rbf :
+      forall t Δ,
+        workload_of_hep_jobs arr_seq j t (t + Δ)
+        <= total_request_bound_function ts Δ.
+    Proof.
+      move=> t Δ.
+      rewrite /workload_of_hep_jobs (leqRW (workload_of_jobs_weaken _ predT _ _ )); last by done.
+      by apply total_workload_le_total_rbf.
+    Qed.
 
-  (** A simple consequence of lemma [hep_workload_le_total_hep_rbf] is
-      that the workload of higher-or-equal priority jobs is bounded by
-      the total request-bound function. *)
-  Corollary hep_workload_le_total_rbf :
-    workload_of_hep_jobs arr_seq j t (t + Δ)
-    <= total_request_bound_function ts Δ.
-  Proof.
-    rewrite /workload_of_hep_jobs (leqRW (workload_of_jobs_weaken _ predT _ _ )); last by done.
-    by apply total_workload_le_total_rbf.
-  Qed.
+  End JLFP.
 
-End TotalRBFBound.
+End ProofRequestBoundFunction.
 
 (** ** RBF Properties *)
 (** In this section, we prove simple properties and identities of RBFs. *)
@@ -302,24 +290,21 @@ Section RequestBoundFunctions.
   Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
   Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
-  (** Let's define some local names for clarity. *)
-  Let task_rbf := task_request_bound_function tsk.
-
-  (** We prove that [task_rbf 0] is equal to [0]. *)
+  (** We prove that [task_request_bound_function 0] is equal to [0]. *)
   Lemma task_rbf_0_zero:
-    task_rbf 0 = 0.
+    task_request_bound_function tsk 0 = 0.
   Proof.
-    rewrite /task_rbf /task_request_bound_function.
+    rewrite /task_request_bound_function.
     apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
     by move: H_valid_arrival_curve => [T1 T2].
   Qed.
 
-  (** We prove that [task_rbf] is monotone. *)
+  (** We prove that [task_request_bound_function] is monotone. *)
   Lemma task_rbf_monotone:
-    monotone leq task_rbf.
+    monotone leq (task_request_bound_function tsk).
   Proof.
-    rewrite /monotone; intros ? ? LE.
-    rewrite /task_rbf /task_request_bound_function leq_mul2l.
+    rewrite /monotone => ? ? LE.
+    rewrite /task_request_bound_function leq_mul2l.
     apply/orP; right.
     by move: H_valid_arrival_curve => [_ T]; apply T.
   Qed.
@@ -331,30 +316,30 @@ Section RequestBoundFunctions.
   (** ... and [max_arrivals tsk ε] is positive. *)
   Hypothesis H_arrival_curve_positive : max_arrivals tsk ε > 0.
 
-  (** Then we prove that [task_rbf] at [ε] is greater than or equal to the task's WCET. *)
+  (** Then we prove that [task_request_bound_function] at [ε] is greater than or equal to the task's WCET. *)
   Lemma task_rbf_1_ge_task_cost:
-    task_rbf ε >= task_cost tsk.
+    task_request_bound_function tsk ε >= task_cost tsk.
   Proof.
     have ALT: forall n, n = 0 \/ n > 0 by clear; intros n; destruct n; [left | right].
     specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
-    rewrite -[task_cost tsk]muln1 /task_rbf /task_request_bound_function.
+    rewrite -[task_cost tsk]muln1 /task_request_bound_function.
     by rewrite leq_pmul2l //=.
   Qed.
 
-  (** As a corollary, we prove that the [task_rbf] at any point [A] greater than
+  (** As a corollary, we prove that the [task_request_bound_function] at any point [A] greater than
       [0] is no less than the task's WCET. *)
   Lemma task_rbf_ge_task_cost:
     forall A,
       A > 0 ->
-      task_rbf A >= task_cost tsk.
+      task_request_bound_function tsk A >= task_cost tsk.
   Proof.
     case => // A GEQ.
     apply: (leq_trans task_rbf_1_ge_task_cost).
     exact: task_rbf_monotone.
   Qed.
 
-  (** Then, we prove that [task_rbf] at [ε] is greater than [0]. *)
-  Lemma task_rbf_epsilon_gt_0 : 0 < task_rbf ε.
+  (** Then, we prove that [task_request_bound_function] at [ε] is greater than [0]. *)
+  Lemma task_rbf_epsilon_gt_0 : 0 < task_request_bound_function tsk ε.
   Proof.
     apply leq_trans with (task_cost tsk) => [//|].
     exact: task_rbf_1_ge_task_cost.
@@ -668,7 +653,7 @@ Section RBFFOrFP.
     rewrite (eq_big (fun j=> pred_task (job_task j)) job_cost) //;
       last by move=> j'; rewrite /pred_task; move: H_job_of_task => /eqP ->.
     erewrite (eq_big pred_task); [|by done|by move=> tsk'; eauto].
-    by apply: sum_of_jobs_le_sum_rbf.
+    by apply: workload_of_jobs_bounded.
   Qed.
 
 End RBFFOrFP.
@@ -742,8 +727,7 @@ Section TaskWorkload.
     <= task_cost tsk * number_of_task_arrivals arr_seq tsk (job_arrival j) (t1 + Δ)
        - task_cost tsk.
   Proof.
-    rewrite /task_workload_between /workload.task_workload_between /task_workload
-      /workload_of_jobs /number_of_task_arrivals /task_arrivals_between.
+    rewrite /task_workload_between /task_workload /workload_of_jobs /number_of_task_arrivals.
     rewrite (big_rem j) //= addnC //= H_job_of_task addnK (filter_size_rem j)//.
     rewrite mulnDr mulnC muln1 addnK mulnC.
     apply sum_majorant_constant => j' ARR' /eqP TSK2.
@@ -774,7 +758,7 @@ Section TaskWorkload.
       rewrite /task_workload_between /task_workload (workload_of_jobs_cat _ (job_arrival j) );
         last by apply/andP; split; lia.
       rewrite -!addnBA; first last.
-      + by rewrite /task_workload_between /task_workload
+      + by rewrite /task_workload
           /workload_of_jobs (big_rem j) //= H_job_of_task leq_addr.
       + rewrite -{1}[task_cost tsk]muln1 leq_mul2l; apply/orP; right.
         rewrite /number_of_task_arrivals /task_arrivals_between.
@@ -782,11 +766,9 @@ Section TaskWorkload.
         apply (mem_bigcat _ Job _ (job_arrival j) _); last by apply job_in_arrivals_at => //=.
         rewrite mem_index_iota.
         by apply /andP;split.
-      + have ->: job_arrival j =  t1 + (job_arrival j - t1) by lia.
-        have ->: t1 + (job_arrival j - t1) = job_arrival j by lia.
-        rewrite leq_add//; last by apply task_rbf_without_job_under_analysis_from_arrival => //=.
-        have ->: job_arrival j =  t1 + (job_arrival j - t1) by lia.
-        by eapply (task_workload_le_num_of_arrivals_times_cost ) => //=.
+      + rewrite leq_add //; last by apply: task_rbf_without_job_under_analysis_from_arrival.
+        rewrite -/(task_workload _ _) -/(task_workload_between _ _ _ _).
+        by apply: task_workload_between_bounded.
   Qed.
 
 End TaskWorkload.
diff --git a/analysis/facts/model/workload.v b/analysis/facts/model/workload.v
index 276d99954e14168f58f762f177c9490789f9bf98..935f2641c3bd74fb7d9295a57777ca8d59330186 100644
--- a/analysis/facts/model/workload.v
+++ b/analysis/facts/model/workload.v
@@ -1,9 +1,7 @@
 Require Export prosa.model.aggregate.workload.
 Require Export prosa.analysis.facts.behavior.arrivals.
-Require Export prosa.analysis.definitions.request_bound_function.
 Require Export prosa.analysis.facts.model.task_arrivals.
 
-
 (** * Lemmas about Workload of Sets of Jobs *)
 (** In this file, we establish basic facts about the workload of sets of jobs. *)
 Section WorkloadFacts.
@@ -53,6 +51,22 @@ Section WorkloadFacts.
     forall (P : pred Job), workload_of_jobs P [::] = 0.
   Proof. by move => ?; rewrite /workload_of_jobs big_nil. Qed.
 
+  (** Now we relate the workload of jobs satisfying a predicate [P] to the sum over tasks. *)
+  Lemma workload_of_jobs_le_sum_over_partitions :
+    forall {P : pred Job} (Q : pred Task) {js : seq Job} (ts : seq Task),
+      {in js, forall j, (job_task j) \in ts} ->
+      {in js, forall j, P j -> Q (job_task j)} ->
+      let P_and_job_of tsk_o j := P j && (job_task j == tsk_o) in
+      workload_of_jobs P js
+      <= \sum_(tsk_o <- ts | Q tsk_o ) workload_of_jobs (P_and_job_of tsk_o) js.
+  Proof.
+    move=> P Q js ts IN_ts PQ //=.
+    rewrite -big_filter.
+    apply: sum_over_partitions_le => j IN Px.
+    rewrite mem_filter.
+    by apply/andP.
+  Qed.
+
   (** The workload of a set of jobs can be equivalently rewritten as sum over
       their tasks. *)
   Lemma workload_of_jobs_partitioned_by_tasks :
@@ -156,56 +170,6 @@ Section WorkloadFacts.
 
   End PredicateProperties.
 
-  (** In this section, we bound the workload of jobs of a particular task by the task's [RBF]. *)
-  Section WorkloadRBF.
-
-    (** Consider an arbitrary task. *)
-    Variable tsk : Task.
-
-    (** Consider a valid arrival curve that is respected by the task [tsk]. *)
-    Context `{MaxArrivals Task}.
-    Hypothesis H_task_repsects_max_arrivals : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
-
-    (** Suppose all arrivals have WCET-compliant job costs. *)
-    Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
-
-    (** Consider an instant [t1] and a duration [Δ]. *)
-    Variable t1 : instant.
-    Variable Δ : duration.
-
-    (** We prove that the workload of jobs of a task [tsk] in any interval is
-        bound by the request bound function of the task in that interval. *)
-    Lemma workload_le_rbf :
-      workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + Δ))
-      <= task_request_bound_function tsk Δ.
-    Proof.
-      apply: (@leq_trans (task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ))).
-      { rewrite /workload_of_jobs /number_of_task_arrivals/task_arrivals_between/job_of_task.
-        apply: sum_majorant_constant => j IN TSK.
-        have: valid_job_cost j; last by rewrite /valid_job_cost; move: TSK => /eqP ->.
-        exact/H_valid_job_cost/in_arrivals_implies_arrived. }
-      { rewrite leq_mul2l; apply/orP; right.
-        rewrite -{2}[Δ](addKn t1).
-        by apply H_task_repsects_max_arrivals; lia. }
-    Qed.
-
-    (** For convenience, we combine the preceding bound with
-        [workload_of_jobs_weaken], as the two are often used together. *)
-    Corollary workload_le_rbf' :
-      forall P,
-        workload_of_jobs (fun j => (P j) && (job_task j == tsk))
-          (arrivals_between arr_seq t1 (t1 + Δ))
-        <= task_request_bound_function tsk Δ.
-    Proof.
-      move=> P.
-      have LEQ: forall ar, workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) ar
-                      <= workload_of_jobs (job_of_task tsk) ar
-        by move=> ar; apply: workload_of_jobs_weaken => j /andP [_ +].
-      by apply/(leq_trans (LEQ _))/workload_le_rbf.
-    Qed.
-
-  End WorkloadRBF.
-
   (** In this section, we prove one equality about the workload of a job. *)
   Section WorkloadOfJob.
 
@@ -286,19 +250,16 @@ Section WorkloadFacts.
     by move: (IMPL j IN TAIL) => /negP.
   Qed.
 
-  (** For simplicity, let's define a local name. *)
-  Let arrivals_between := arrivals_between arr_seq.
-
   (** We observe that the cumulative workload of all jobs arriving in a time
       interval <<[t1, t2)>> and respecting a predicate [P] can be split into two parts. *)
    Lemma workload_of_jobs_cat:
     forall t t1 t2 P,
       t1 <= t <= t2 ->
-      workload_of_jobs P (arrivals_between t1 t2) =
-      workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2).
+      workload_of_jobs P (arrivals_between arr_seq t1 t2) =
+      workload_of_jobs P (arrivals_between arr_seq t1 t) + workload_of_jobs P (arrivals_between arr_seq t t2).
   Proof.
     move => t t1 t2 P /andP [GE LE].
-    rewrite /workload_of_jobs /arrivals_between.
+    rewrite /workload_of_jobs.
     by rewrite (arrivals_between_cat _ _ t) // big_cat.
   Qed.
 
@@ -308,8 +269,8 @@ Section WorkloadFacts.
       forall t1 t2 t3 P,
         t1 <= t2 ->
         t2 <= t3 ->
-        workload_of_jobs P (arrivals_between t1 t2)
-        <= workload_of_jobs P (arrivals_between t1 t3).
+        workload_of_jobs P (arrivals_between arr_seq t1 t2)
+        <= workload_of_jobs P (arrivals_between arr_seq t1 t3).
     Proof.
       move => t1 t2 t3 P ??.
       rewrite (workload_of_jobs_cat t2 t1 t3 P _  ) //=; [| apply /andP; split; done].
@@ -379,8 +340,8 @@ Section WorkloadFacts.
         arriving in <<[t1,t)>>. Note that we only require [t1] to be less-or-equal
         than [t2]. Consequently, the interval <<[t1,t)>> may be empty. *)
     Lemma workload_equal_subset :
-      workload_of_jobs (fun j => (job_arrival j <= t) && P j) (arrivals_between t1 t2)
-      <= workload_of_jobs (fun j => P j) (arrivals_between t1 (t + ε)).
+      workload_of_jobs (fun j => (job_arrival j <= t) && P j) (arrivals_between arr_seq t1 t2)
+      <= workload_of_jobs (fun j => P j) (arrivals_between arr_seq t1 (t + ε)).
     Proof.
       clear H_jobs_uniq H_j_in_jobs H_t1_le_t2.
       rewrite /workload_of_jobs big_seq_cond.
diff --git a/analysis/facts/priority/fifo_ahep_bound.v b/analysis/facts/priority/fifo_ahep_bound.v
index 58f3420064550fd359a3f1797d9958cb73e6f205..167a2f69c2e41fea4b1b1095667d383d84cb4b49 100644
--- a/analysis/facts/priority/fifo_ahep_bound.v
+++ b/analysis/facts/priority/fifo_ahep_bound.v
@@ -110,9 +110,9 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
           apply leq_sum => tsk' _; rewrite andbC //=.
           destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by [].
           apply rem_in in IN.
-          eapply leq_trans;
-            last by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
-          by rewrite addnBAC //= subnKC //= addn1; apply leqW.
+          rewrite addnBAC //=.
+          apply: leq_trans; last by apply rbf_spec with (t := t1) (Δ := job_arrival j + 1 - t1).
+          by rewrite subnKC //= addn1; apply leqW.
       + move : H_job_of_task => TSKj.
         rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=;
                 first by rewrite TSKj; apply leq_addr.
diff --git a/analysis/facts/priority/jlfp_with_fp.v b/analysis/facts/priority/jlfp_with_fp.v
index 7be811219768409a54a0717c4401830d2bf1ed38..b7900aed4270bf60b86c25f87c80179ca288b3c4 100644
--- a/analysis/facts/priority/jlfp_with_fp.v
+++ b/analysis/facts/priority/jlfp_with_fp.v
@@ -45,7 +45,6 @@ Section WorkloadTaskSum.
 
   (** ... and focus on the jobs arriving in an arbitrary interval <<[t1, t2)>>. *)
   Variable t1 t2 : duration.
-  Let jobs_arrived := arrivals_between arr_seq t1 t2.
 
   (** We first consider jobs that belong to other tasks that have equal priority
       as [tsk] and have higher-or-equal priority [JLFP] than [j]. *)
@@ -58,11 +57,11 @@ Section WorkloadTaskSum.
   (** We then establish that the cumulative workload of these jobs can be partitioned
       task-wise. *)
   Lemma hep_workload_from_other_ep_partitioned_by_tasks :
-    workload_of_jobs hep_job_of_ep_other_task jobs_arrived
+    workload_of_jobs hep_job_of_ep_other_task (arrivals_between arr_seq t1 t2)
       = \sum_(tsk_o <- ts | other_ep_task tsk_o)
         workload_of_jobs
           (fun j0 => hep_job_of_ep_other_task j0 && (job_task j0 == tsk_o))
-          jobs_arrived.
+          (arrivals_between arr_seq t1 t2).
   Proof.
     apply: workload_of_jobs_partitioned_by_tasks => //.
     - by move=> j' IN'; apply/H_all_jobs_from_taskset/in_arrivals_implies_arrived/IN'.
@@ -71,7 +70,6 @@ Section WorkloadTaskSum.
         => /andP [/andP [_ EP] NEQ].
       apply/andP; split => //.
       by rewrite ep_task_sym.
-    - by apply: arrivals_uniq.
   Qed.
 
   (** Now we focus on jobs belonging to tasks which have higher priority than [tsk]. *)
@@ -91,7 +89,8 @@ Section WorkloadTaskSum.
       jobs belonging to tasks having higher priority than [tsk] is equal to the
       cumulative workload of jobs belonging to higher-priority tasks. *)
   Lemma hep_hp_workload_hp :
-    workload_of_jobs hep_from_hp_task jobs_arrived = workload_of_jobs from_hp_task jobs_arrived.
+    workload_of_jobs hep_from_hp_task (arrivals_between arr_seq t1 t2)
+    = workload_of_jobs from_hp_task (arrivals_between arr_seq t1 t2).
   Proof.
     apply/eq_bigl =>j0; apply /idP/idP.
     - by move=> /andP[].
@@ -104,11 +103,11 @@ Section WorkloadTaskSum.
       belonging to higher-priority tasks and the cumulative workload of
       higher-or-equal-priority jobs belonging to equal-priority tasks. *)
   Lemma hep_workload_partitioning_taskwise :
-    workload_of_higher_or_equal_priority_jobs j jobs_arrived
-    = workload_of_jobs hep_from_hp_task jobs_arrived
-      + workload_of_jobs hep_from_ep_task jobs_arrived.
+    workload_of_hep_jobs arr_seq j t1 t2
+    = workload_of_jobs hep_from_hp_task (arrivals_between arr_seq t1 t2)
+      + workload_of_jobs hep_from_ep_task (arrivals_between arr_seq t1 t2).
   Proof.
-    rewrite /workload_of_higher_or_equal_priority_jobs /workload_of_jobs.
+    rewrite /workload_of_hep_jobs /workload_of_jobs.
     rewrite (bigID from_hp_task) /=; congr (_ + _); apply: eq_bigl => j0.
     apply: andb_id2l => HEPj.
     have HEPt : hep_task (job_task j0) (job_task j) by apply (hep_job_implies_hep_task JLFP).
diff --git a/analysis/facts/workload/edf_athep_bound.v b/analysis/facts/workload/edf_athep_bound.v
index 1cdc19b5a3a919a06e214e185608c918b30dfc85..7579895843b396b810af2643ab26a82c570afd26 100644
--- a/analysis/facts/workload/edf_athep_bound.v
+++ b/analysis/facts/workload/edf_athep_bound.v
@@ -1,10 +1,9 @@
 Require Export prosa.model.priority.edf.
 Require Export prosa.model.task.absolute_deadline.
 Require Export prosa.analysis.definitions.workload.bounded.
-Require Export prosa.analysis.facts.model.workload.
+Require Export prosa.analysis.facts.model.rbf.
 Require Export prosa.analysis.definitions.workload.edf_athep_bound.
 
-
 (** * Bound on Higher-or-Equal Priority Workload under EDF Scheduling is Valid *)
 
 (** In this file, we prove that the upper bound on interference
@@ -133,11 +132,10 @@ Section ATHEPWorkloadBoundIsValidForEDF.
       \sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (EDF_from tsk_o) jobs
       <= bound_on_athep_workload ts tsk A Δ.
     Proof.
-      apply leq_sum_seq => tsko INtsko NEQT; fold (D tsk) (D tsko).
-      edestruct (leqP Δ (A + ε + D tsk - D tsko)) as [NEQ|NEQ]; [ | apply ltnW in NEQ].
-      - exact: (workload_le_rbf' arr_seq tsko).
-      - eapply leq_trans; first by eapply total_workload_shorten_range; eauto 2.
-        exact: workload_le_rbf'.
+      apply: leq_sum_seq => tsko INtsko NEQT; fold (D tsk) (D tsko).
+      have [LEQ|LT] := leqP Δ (A + ε + D tsk - D tsko);
+        last (apply: leq_trans; first by apply: total_workload_shorten_range).
+      all: by apply: rbf_spec' => // ? /andP[].
     Qed.
 
   End HepWorkloadBound.
diff --git a/model/aggregate/workload.v b/model/aggregate/workload.v
index 0e693e222e4cc371fe5298704f19d03b6178fea6..574c50267a3f8fb02107eb1306a58d3fe4d2ff48 100644
--- a/model/aggregate/workload.v
+++ b/model/aggregate/workload.v
@@ -3,7 +3,7 @@ Require Export prosa.model.priority.classes.
 (** * Cumulative Workload of Sets of Jobs *)
 
 (** In this module, we define the notion of the cumulative workload of
-    a set of jobs. *)  
+    a set of jobs. *)
 Section WorkloadOfJobs.
 
   (** Consider any type of tasks ... *)
@@ -16,23 +16,38 @@ Section WorkloadOfJobs.
   Context `{JobTask Job Task}.
   Context `{JobCost Job}.
 
-  (** Consider any job arrival sequence. *)
+  (** We define the workload of jobs that satisfy a predicate. *)
+  Definition workload_of_jobs (P : pred Job) (jobs : seq Job) :=
+    \sum_(j <- jobs | P j) job_cost j.
+
+  (** We define the task workload as the workload of jobs of task [tsk]. *)
+  Definition task_workload (tsk : Task) (jobs : seq Job) :=
+    workload_of_jobs (job_of_task tsk) jobs.
+
+  (** Now consider an arbitrary job arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
-  
-  (** First, we define the workload for generic sets of jobs. *)
-  Section WorkloadOfJobs.
-    
-    (** Given any computable predicate on jobs, ... *)
-    Variable P : pred Job.
-
-    (** ... and any (finite) set of jobs, ... *)
-    Variable jobs : seq Job.
-
-    (** ... we define the total workload of the jobs that satisfy
-        predicate [P]. *)
-    Definition workload_of_jobs := \sum_(j <- jobs | P j) job_cost j.
-    
-  End WorkloadOfJobs.
+
+  (** We define a task's workload in a given interval [[t1, t2)]. *)
+  Definition task_workload_between (tsk : Task) (t1 t2 : instant) :=
+    task_workload tsk (arrivals_between arr_seq t1 t2).
+
+  (** Further, we define (trivially) the workload of a given job. While this
+      definition may appear of little use, it is in fact useful for certain
+      rewriting steps. *)
+  Definition workload_of_job (j : Job) (t1 t2 : instant) :=
+    workload_of_jobs (xpred1 j) (arrivals_between arr_seq t1 t2).
+
+  (** In this section, we add definitions for total workload. *)
+  Section TotalWorkload.
+
+    (** We define the total workload as the sum of workloads of all incoming jobs. *)
+    Definition total_workload (jobs : seq Job) := workload_of_jobs predT jobs.
+
+    (** We also define the total workload in a given interval [[t1, t2)]. *)
+    Definition total_workload_between (t1 t2 : instant) :=
+      total_workload (arrivals_between arr_seq t1 t2).
+
+  End TotalWorkload.
 
   (** Next, we define the workload of jobs with higher or
       equal priority under JLFP policies. *)
@@ -42,52 +57,18 @@ Section WorkloadOfJobs.
         higher or equal priority. *)
     Context `{JLFP_policy Job}.
 
-    (** Let j be the job to be analyzed. *)
-    Variable j : Job.
-
-    (** Recall the notion of a job of higher or equal priority. *)
-    Let of_higher_or_equal_priority j_hp := hep_job j_hp j.
-
-    (** Then, we define the workload of higher or equal priority of all jobs
-        with higher-or-equal priority than j. *)
-    Definition workload_of_higher_or_equal_priority_jobs jobs :=
-      workload_of_jobs of_higher_or_equal_priority jobs.
-
     (** We extend the prior notion to define the workload all jobs
         with higher-or-equal priority than [j] in a given interval. *)
     Definition workload_of_hep_jobs (j : Job) (t1 t2 : instant) :=
-      workload_of_jobs
-        (fun jhp => hep_job jhp j)
-        (arrivals_between arr_seq t1 t2).
+      let is_hep j' := hep_job j' j in
+        workload_of_jobs is_hep (arrivals_between arr_seq t1 t2).
 
     (** We define a similar _non-reflexive_ notion of higher-or-equal
         priority workload in an interval. *)
     Definition workload_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=
-      workload_of_jobs
-        (fun jhp => another_hep_job jhp j)
-        (arrivals_between arr_seq t1 t2).
-
-    (** For analysis purposes, we define the workload of a given job. *)
-    Definition workload_of_job (j : Job) (t1 t2 : instant) :=
-      workload_of_jobs (xpred1 j) (arrivals_between arr_seq t1 t2).
+      let is_ahep j' := another_hep_job j' j in
+        workload_of_jobs is_ahep (arrivals_between arr_seq t1 t2).
 
   End PerJobPriority.
 
-  (** We also define workload of a task. *)
-  Section TaskWorkload.
-
-    (** Let [tsk] be the task to be analyzed. *)
-    Variable tsk : Task.
-
-    (** We define the task workload as the workload of jobs of task
-        [tsk]. *)
-    Definition task_workload jobs := workload_of_jobs (job_of_task tsk) jobs.
-
-    (** Finally, we define the task's workload in a given interval [[t1,
-        t2)]. *)
-    Definition task_workload_between (t1 t2 : instant) :=
-      task_workload (arrivals_between arr_seq t1 t2).
-
-  End TaskWorkload.
-
 End WorkloadOfJobs.
diff --git a/results/elf/rta/bounded_pi.v b/results/elf/rta/bounded_pi.v
index d04b10eb47bf7ae3e11ff2f249c66d430d3b6403..488b69d1f801ee1dd623030af2d66cc457845268 100644
--- a/results/elf/rta/bounded_pi.v
+++ b/results/elf/rta/bounded_pi.v
@@ -263,7 +263,7 @@ Section AbstractRTAforELFwithArrivalCurves.
     { rewrite {2}H_fixed_point => t.
       apply leq_trans with (priority_inversion_lp_tasks_bound
                             + priority_inversion_ep_tasks_bound (job_arrival j - t)
-                            + workload_of_higher_or_equal_priority_jobs j (arrivals_between arr_seq t (t + L)));
+                            + workload_of_hep_jobs arr_seq j t (t + L));
         first by rewrite leq_add2r max_leq_add.
       rewrite -addnA leq_add2l /total_hep_rbf.
       rewrite hep_rbf_taskwise_partitioning /total_ep_request_bound_function_FP (bigID (is_ep_causing_intf j t)) /=.
@@ -280,8 +280,10 @@ Section AbstractRTAforELFwithArrivalCurves.
         apply leq_trans with (task_request_bound_function tsk_other ε).
         - by apply: leq_pmulr.
         - by apply/leq_mul/(H_valid_arrival_curve _ _).2. }
-      { rewrite hep_hp_workload_hp =>//. rewrite /from_hp_task TSK'; exact: sum_of_jobs_le_sum_rbf. }
-      { apply: leq_trans; last by apply: sum_of_jobs_le_sum_rbf.
+      { rewrite hep_hp_workload_hp =>//. rewrite /from_hp_task TSK'; exact: workload_of_jobs_bounded. }
+      { apply leq_trans with (n := workload_of_jobs
+          (fun j0 : Job => ep_task (job_task j0) tsk && is_ep_causing_intf j t (job_task j0))
+          (arrivals_between arr_seq t (t + L))); last by apply workload_of_jobs_bounded.
         rewrite /workload_of_jobs big_seq_cond [leqRHS]big_seq_cond.
         apply: sub_le_big => //; first by move => ? ?; apply: leq_addr.
         move=> j0; case eq: (_ \in _) =>//=.
@@ -462,7 +464,7 @@ Section AbstractRTAforELFwithArrivalCurves.
              => i /andP[/andP[? ?] ?].
         by apply/andP; split. }
       { have [LEQ|GT] := leqP Δ `|Num.max 0%R (ep_task_intf_interval tsk_o A)%R|; [| apply ltnW in GT].
-        { apply: leq_trans; last by eapply task_workload_le_task_rbf.
+        { apply: leq_trans; last by eapply rbf_spec.
           apply: (workload_of_jobs_weaken _ (fun j0 => (job_task j0 == tsk_o))).
           by move => j'/ andP[_ EXACT]. }
         { apply: leq_trans;
@@ -473,7 +475,7 @@ Section AbstractRTAforELFwithArrivalCurves.
             have -> : `|Num.max 0%R (t1%:R + ep_task_intf_interval tsk_o A)%R|
                      = t1 + `|Num.max 0%R (ep_task_intf_interval tsk_o A)|
               by clear -EQ; lia.
-            by apply: (workload_le_rbf' arr_seq tsk_o _ _  t1 _ (fun jo => hep_job jo j)). }
+            by apply: rbf_spec' => // ? /andP[]. }
           { move => j' IN1.
             have [TSK'|_] := (eqVneq  (job_task j') tsk_o).
             - by rewrite !andbT TSK TSK' ep_task_sym EP andbT.
@@ -492,7 +494,7 @@ Section AbstractRTAforELFwithArrivalCurves.
         first by apply: service_of_jobs_le_workload.
       rewrite /workload_of_jobs /total_hp_request_bound_function_FP.
       rewrite [X in X <= _](eq_big (fun j0 => hp_task (job_task j0) tsk) job_cost) //;
-        first by apply: sum_of_jobs_le_sum_rbf; eauto.
+        first by apply: workload_of_jobs_bounded; eauto.
       rewrite /hp_task_hep_job  => j'.
       rewrite andb_idl => [|?].
       - by move: H_job_of_task => /eqP ->.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 227fa8f43e3161fd804846c3f3104e735e719500..9853d4bd1f63ff058319824bf02af71a69ada583 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -206,11 +206,11 @@ Section AbstractRTAforFPwithArrivalCurves.
       { exists t1, t2; split=> [//|]; split=> [//|].
         by eapply instantiated_busy_interval_equivalent_busy_interval. }
       { intros; rewrite {2}H_fixed_point leq_add //.
-        rewrite /workload_of_higher_or_equal_priority_jobs /total_hep_rbf
+        rewrite /workload_of_hep_jobs /total_hep_rbf
           /total_hep_request_bound_function_FP
           /workload_of_jobs /hep_job /FP_to_JLFP.
         move: (TSK) =>  /eqP ->.
-        exact: sum_of_jobs_le_sum_rbf. }
+        exact: workload_of_jobs_bounded. }
     Qed.
 
     (** Next, we prove that [task_IBF] is indeed an interference
@@ -257,7 +257,7 @@ Section AbstractRTAforFPwithArrivalCurves.
           rewrite (eq_big (fun j=> pred_task (job_task j)) job_cost) //;
             last by move=> j'; rewrite /pred_task; move: TSK => /eqP ->.
           erewrite (eq_big pred_task); [|by done|by move=> tsk'; eauto].
-          by apply: sum_of_jobs_le_sum_rbf; eauto. } }
+          by apply: workload_of_jobs_bounded; eauto. } }
     Qed.
 
     (** Finally, we show that there exists a solution for the
diff --git a/results/gel/rta/bounded_pi.v b/results/gel/rta/bounded_pi.v
index 55e0da7067e4840c27a8a671340538c226d60fba..4a83ea11b545d759239eab2d67160bbfd04269e6 100644
--- a/results/gel/rta/bounded_pi.v
+++ b/results/gel/rta/bounded_pi.v
@@ -209,15 +209,15 @@ Section AbstractRTAforGELwithArrivalCurves.
         <= bound_on_total_hep_workload A Δ.
       Proof.
         apply leq_sum_seq => tsko INtsko NEQT.
-        have [EQ|EQ] := leqP Δ `|Num.max 0%R (interval tsko A)|.
-          { exact: (workload_le_rbf' arr_seq tsko). }
-        apply: (leq_trans (total_workload_shorten_range _ _ _ _)) => //; [lia|].
-        rewrite /GEL_from.
-        have [EQ1|EQ1] := lerP 0%R (interval tsko A).
+        have [LEQ|LT] := leqP Δ `|Num.max 0%R (interval tsko A)|;
+          first by apply: rbf_spec' => // ? /andP[].
+        apply: leq_trans;
+          first by apply: total_workload_shorten_range => //; lia.
+        have [POS0|NEG] := lerP 0%R (interval tsko A).
         - have -> : `|Num.max 0%R (t1%:R + interval tsko A)%R|
             = t1 + `|interval tsko A| by lia.
-          exact: workload_le_rbf'.
-        - rewrite arrivals_between_geq /workload_of_jobs ?big_nil//; lia.
+          by apply: rbf_spec' => // ? /andP[].
+        - by rewrite arrivals_between_geq /workload_of_jobs ?big_nil//; lia.
       Qed.
 
     End HepWorkloadBound.
diff --git a/results/rs/fifo/bounded_nps.v b/results/rs/fifo/bounded_nps.v
index 4f311265bde1da23d03113996f14a59f54acf4ee..e593ce2f1b5f6176fedbaa7c5a1beb1371bd3796 100644
--- a/results/rs/fifo/bounded_nps.v
+++ b/results/rs/fifo/bounded_nps.v
@@ -213,9 +213,6 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
       all: try done.
       apply instantiated_busy_interval_equivalent_busy_interval => //.
     - apply: soln_abstract_response_time_recurrence => //.
-      move: TSKs => /eqP <-.
-      apply: leq_trans; first by apply POS.
-      by apply H_valid_job_cost.
   Qed.
 
 End RTAforFullyPreemptiveFIFOModelwithArrivalCurves.