diff --git a/analysis/abstract/restricted_supply/abstract_rta.v b/analysis/abstract/restricted_supply/abstract_rta.v
index 672a6176701bfe90b550ccfa2251cd981f048ac1..4057100a7d016634470cc3a0b96de2ccfddc5cb4 100644
--- a/analysis/abstract/restricted_supply/abstract_rta.v
+++ b/analysis/abstract/restricted_supply/abstract_rta.v
@@ -85,12 +85,12 @@ Section AbstractRTARestrictedSupply.
   Hypothesis H_busy_interval_exists :
     busy_intervals_are_bounded_by arr_seq sched tsk L.
 
-  (** Consider a valid, unit supply-bound function [SBF]. That is,
-      (1) [SBF 0 = 0], (2) for any duration [Δ], the supply produced
-      during a busy interval of length [Δ] is at least [SBF Δ], and
-      (3) [SBF] makes steps of at most one. *)
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
   Context {SBF : SupplyBoundFunction}.
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
   Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
 
   (** Next, we assume that [intra_IBF] is a bound on the intra-supply
@@ -203,7 +203,7 @@ Section AbstractRTARestrictedSupply.
         <= (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
       Proof.
         rewrite -blackout_plus_local_is_interference_cumul leq_add2r.
-        by apply: blackout_during_bound => //.
+        by eapply blackout_during_bound with (t2 := t2) => //.
       Qed.
 
       (** Next, consider a duration [F] such that [F <= Δ] and job [j]
@@ -308,7 +308,7 @@ Section AbstractRTARestrictedSupply.
         rewrite -/(cumulative_interference _ _ _).
         erewrite <-blackout_plus_local_is_interference_cumul with (t2 := t2) => //; last by apply BUSY. 
         rewrite addnC leq_add //; last first.
-        { by eapply blackout_during_bound with (t2 := t2) => //; apply BUSY. }
+        { by eapply blackout_during_bound with (t2 := t2) => //; split; [ | apply BUSY]. }
         rewrite /cumul_intra_interference (cumulative_interference_cat _ j (t1 + F)) //=; last by lia.
         rewrite -!/(cumul_intra_interference _ _ _ _).
         rewrite (no_intra_interference_after_F _ _ _ _ _ t2) //; last by move: BUSY => [].
diff --git a/analysis/abstract/restricted_supply/abstract_seq_rta.v b/analysis/abstract/restricted_supply/abstract_seq_rta.v
index d445abe843a808c1ff83e3431721927610275bcb..078d50265f9bfd33ff77a6b23e73d93ab5ca39cf 100644
--- a/analysis/abstract/restricted_supply/abstract_seq_rta.v
+++ b/analysis/abstract/restricted_supply/abstract_seq_rta.v
@@ -97,12 +97,12 @@ Section AbstractRTARestrictedSupplySequential.
   Hypothesis H_busy_interval_exists :
     busy_intervals_are_bounded_by arr_seq sched tsk L.
 
-  (** Consider a unit SBF valid in busy intervals. That is, (1) [SBF 0
-      = 0], (2) for any duration [Δ], the supply produced during a
-      busy-interval prefix of length [Δ] is at least [SBF Δ], and (3)
-      [SBF] makes steps of at most one. *)
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
   Context {SBF : SupplyBoundFunction}.
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
   Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
 
   (** Next, we assume that [task_intra_IBF] is a bound on intra-supply
diff --git a/analysis/abstract/restricted_supply/bounded_bi/edf.v b/analysis/abstract/restricted_supply/bounded_bi/edf.v
index 47c13e80dba4fdf6361a86199eb062eaf8cca3d0..b7c3dabeed069eda52da76408d82ba198d5a26c1 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/edf.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/edf.v
@@ -98,14 +98,6 @@ Section BoundedBusyIntervals.
   (** ... and that the cost of a job does not exceed its task's WCET. *)
   Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
 
-  (** Consider a unit SBF valid in busy intervals. That is, (1) [SBF 0
-      = 0], (2) for any duration [Δ], the supply produced during a
-      busy-interval prefix of length [Δ] is at least [SBF Δ], and (3)
-      [SBF] makes steps of at most one. *)
-  Context {SBF : SupplyBoundFunction}.
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
-  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
-
   (** Let [max_arrivals] be a family of valid arrival curves. *)
   Context `{MaxArrivals Task}.
   Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
@@ -115,6 +107,14 @@ Section BoundedBusyIntervals.
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
   (** First, we show that the constant [longest_busy_interval_with_pi
       ts tsk] indeed bounds the cumulative interference incurred by
       job [j]. *)
@@ -255,7 +255,7 @@ Section BoundedBusyIntervals.
         eapply workload_exceeds_interval with (Δ := L) in PREFIX => //; last first.
         move_neq_down PREFIX.
         rewrite (cumulative_interfering_workload_split _ _ _).
-        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ _ _ _ _)); (try apply GTC) => //.
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
         rewrite addnC -!addnA.
         have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
         apply: E; first by lia.
@@ -290,13 +290,7 @@ Section BoundedBusyIntervals.
         workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
       Proof.
         rewrite (cumulative_interfering_workload_split _ _ _).
-        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ _ _ _ _)); (try apply H_busy_prefix_L); first last.
-        { by done. }
-        { by done. }
-        { split; first by apply H_valid_SBF.
-          move => *; destruct H_valid_SBF as [A B].
-          by apply: B => //; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //. }
-        { by done. }
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
         rewrite // addnC -!addnA.
         have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
         apply: E; first by lia.
diff --git a/analysis/abstract/restricted_supply/bounded_bi/fp.v b/analysis/abstract/restricted_supply/bounded_bi/fp.v
index 36dcae178565c56d4ed0060f60f8f1362f4e2c19..2311d885c7eb831597aeb47bb81d543a49b3f129 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/fp.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/fp.v
@@ -91,14 +91,6 @@ Section BoundedBusyIntervals.
   (** ... and that the cost of a job does not exceed its task's WCET. *)
   Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
 
-  (** Consider a unit SBF valid in busy intervals. That is, (1) [SBF 0
-      = 0], (2) for any duration [Δ], the supply produced during a
-      busy-interval prefix of length [Δ] is at least [SBF Δ], and (3)
-      [SBF] makes steps of at most one. *)
-  Context {SBF : SupplyBoundFunction}.
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
-  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
-
   (** 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
@@ -111,6 +103,14 @@ Section BoundedBusyIntervals.
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
   (** Let [L] be any positive fixed point of the busy-interval recurrence. *)
   Variable L : duration.
   Hypothesis H_L_positive : 0 < L.
@@ -155,7 +155,7 @@ Section BoundedBusyIntervals.
         workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
       Proof.
         rewrite (cumulative_interfering_workload_split _ _ _).
-        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ _ _ _ _)) => //.
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
         rewrite // addnC -!addnA.
         have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
         apply: E; first by lia.
@@ -217,12 +217,7 @@ Section BoundedBusyIntervals.
         eapply workload_exceeds_interval with (Δ := L) in PREFIX => //.
         { move_neq_down PREFIX.
           rewrite (cumulative_interfering_workload_split _ _ _).
-          (rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ _ _ _ _)); try apply GTC) => //; first last.
-          { move=> *; split; first by apply H_valid_SBF.
-            move => *; destruct H_valid_SBF as [A B].
-            apply: B => //.
-            by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
-          }
+          rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
           rewrite addnC -!addnA.
           have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
           apply: E; first by lia.
diff --git a/analysis/abstract/restricted_supply/bounded_bi/jlfp.v b/analysis/abstract/restricted_supply/bounded_bi/jlfp.v
index 4762a585a3445b1ff2cd21e0365d626de835e01e..044c60cda29cefd0b7ec87d33d082fbfa90b59e3 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/jlfp.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/jlfp.v
@@ -94,14 +94,6 @@ Section BoundedBusyIntervals.
   (** ... and that the cost of a job does not exceed its task's WCET. *)
   Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
 
-  (** Consider a unit SBF valid in busy intervals. That is, (1) [SBF 0
-      = 0], (2) for any duration [Δ], the supply produced during a
-      busy-interval prefix of length [Δ] is at least [SBF Δ], and (3)
-      [SBF] makes steps of at most one. *)
-  Context {SBF : SupplyBoundFunction}.
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
-  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
-
   (** Let [max_arrivals] be a family of valid arrival curves. *)
   Context `{MaxArrivals Task}.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
@@ -110,6 +102,14 @@ Section BoundedBusyIntervals.
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
   (** Let [blocking_bound] be a function that bounds the priority
       inversion caused by lower-priority jobs, where the argument
       [blocking_bound] takes is the relative offset (w.r.t. the
@@ -171,7 +171,7 @@ Section BoundedBusyIntervals.
         workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
       Proof.
         rewrite (cumulative_interfering_workload_split _ _ _).
-        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ _ _ _ _)); (try apply H_busy_prefix_L) => //.
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
         rewrite // addnC -!addnA.
         have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
         apply: E; first by lia.
@@ -230,12 +230,7 @@ Section BoundedBusyIntervals.
         eapply workload_exceeds_interval with (Δ := L) in PREFIX => //.
         { move_neq_down PREFIX.
           rewrite (cumulative_interfering_workload_split _ _ _).
-          (rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ _ _ _ _)); try apply GTC) => //; first last.
-          { move=> *; split; first by apply H_valid_SBF.
-            move => *; destruct H_valid_SBF as [A B].
-            apply: B => //.
-            by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
-          }
+          rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
           rewrite addnC -!addnA.
           have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
           apply: E; first by lia.
diff --git a/analysis/abstract/restricted_supply/busy_sbf.v b/analysis/abstract/restricted_supply/busy_sbf.v
index 9b203b7a3cca715acb14d7797ff5c871b3b7b99a..7e8ede6b55c5e4c26c63df9713dc1d209942dab4 100644
--- a/analysis/abstract/restricted_supply/busy_sbf.v
+++ b/analysis/abstract/restricted_supply/busy_sbf.v
@@ -6,13 +6,17 @@ Require Export prosa.analysis.abstract.definitions.
 
 (** In the following, we define a weak notion of a supply bound
     function, which is a valid SBF only within an abstract busy
-    interval of a job. *)
+    interval of a task's job. *)
 Section BusySupplyBoundFunctions.
 
-  (** Consider any type of jobs, ... *)
+  (** Consider any type of tasks, ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs. *)
   Context {Job : JobType}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
 
   (** ... any kind of processor state model, ... *)
   Context `{PState : ProcessorState Job}.
@@ -23,20 +27,28 @@ Section BusySupplyBoundFunctions.
   (** ... and any schedule. *)
   Variable sched : schedule PState.
 
+  (** Consider a task [tsk]. *)
+  Variable tsk : Task.
+
   (** Assume we are provided with abstract functions for Interference
       and Interfering Workload. *)
   Context `{Interference Job}.
   Context `{InterferingWorkload Job}.
 
-  (** We say that the SBF is respected in an (abstract) busy interval
-      if, for any busy interval <<[t1, t2)>> and a subinterval <<[t1,
-      t) ⊆ [t1, t2)>>, at least [SBF (t - t1)] cumulative supply is
-      provided. *)
+  (** We define a predicate that determines whether an interval <<[t1,
+      t2)>> is a busy-interval prefix of a job [j] of task [tsk]. *)
+  Let bi_prefix_of_tsk j t1 t2 :=
+    job_of_task tsk j /\ busy_interval_prefix sched j t1 t2.
+
+  (** We say that the SBF is respected in a busy interval w.r.t. task
+      [tsk] if, for any busy interval <<[t1, t2)>> of a job [j ∈ tsk]
+      and a subinterval <<[t1, t) ⊆ [t1, t2)>>, at least [SBF (t -
+      t1)] cumulative supply is provided. *)
   Definition sbf_respected_in_busy_interval (SBF : duration -> work) :=
-    pred_sbf_respected arr_seq sched (busy_interval_prefix sched) SBF.
+    pred_sbf_respected arr_seq sched bi_prefix_of_tsk SBF.
 
   (** Next, we define an SBF that is valid within an (abstract) busy interval. *)
   Definition valid_busy_sbf (SBF : duration -> work) :=
-    valid_pred_sbf arr_seq sched (busy_interval_prefix sched) SBF.
+    valid_pred_sbf arr_seq sched bi_prefix_of_tsk SBF.
 
 End BusySupplyBoundFunctions.
diff --git a/analysis/abstract/restricted_supply/search_space/fifo_fixpoint.v b/analysis/abstract/restricted_supply/search_space/fifo_fixpoint.v
index 21427087c2efc037cdef882497b72c7061b83d7d..07d8b8f5d16241f35a00a33db46a2b5483254fce 100644
--- a/analysis/abstract/restricted_supply/search_space/fifo_fixpoint.v
+++ b/analysis/abstract/restricted_supply/search_space/fifo_fixpoint.v
@@ -58,10 +58,10 @@ Section ConcreteToAbstractFixpointReduction.
   Variable sched : schedule PState.
 
   (** Next, we assume that [SBF] properly characterizes all busy
-      intervals in [sched]. That is, (1) [SBF 0 = 0] and (2) for any
-      duration [Δ], at least [SBF Δ] supply is available in any
-      busy-interval prefix of length [Δ]. *)
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+      intervals (w.r.t. task [tsk]) in [sched]. That is, (1) [SBF 0 =
+      0] and (2) for any duration [Δ], at least [SBF Δ] supply is
+      available in any busy-interval prefix of length [Δ]. *)
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
 
   (** We assume that [tsk] is described by a valid task
       run-to-completion threshold_ *)
diff --git a/analysis/definitions/sbf/busy.v b/analysis/definitions/sbf/busy.v
index afede54d41f00f7303053ec451e4c1b70d638d70..a59fc45610a2706361cfe34c3fd4b75747113613 100644
--- a/analysis/definitions/sbf/busy.v
+++ b/analysis/definitions/sbf/busy.v
@@ -6,15 +6,19 @@ Require Export prosa.analysis.definitions.busy_interval.classical.
 
 (** In the following, we define a weak notion of a supply bound
     function, which is a valid SBF only within a busy interval of a
-    job. *)
+    task's job. *)
 Section BusySupplyBoundFunctions.
 
-  (** Consider any type of jobs, ... *)
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs. *)
   Context {Job : JobType}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
 
-  (** ... any kind of processor state model, ... *)
+  (** Consider any kind of processor state model, ... *)
   Context `{PState : ProcessorState Job}.
 
   (** ... any valid arrival sequence, and ... *)
@@ -26,14 +30,23 @@ Section BusySupplyBoundFunctions.
   (** Assume a given JLFP policy. *)
   Context `{JLFP_policy Job}.
 
-  (** We say that the SBF is respected in a busy interval if, for any
-      busy interval <<[t1, t2)>> and a subinterval <<[t1, t) ⊆ [t1,
-      t2)>>, at least [SBF (t - t1)] cumulative supply is provided. *)
+  (** Consider a task [tsk]. *)
+  Variable tsk : Task.
+
+  (** We define a predicate that determines whether an interval <<[t1,
+      t2)>> is a busy-interval prefix of a job [j] of task [tsk]. *)
+  Let bi_prefix_of_tsk j t1 t2 :=
+    job_of_task tsk j /\ busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** We say that the SBF is respected in a busy interval w.r.t. task
+      [tsk] if, for any busy interval <<[t1, t2)>> of a job [j ∈ tsk]
+      and a subinterval <<[t1, t) ⊆ [t1, t2)>>, at least [SBF (t -
+      t1)] cumulative supply is provided. *)
   Definition sbf_respected_in_busy_interval (SBF : duration -> work) :=
-    pred_sbf_respected arr_seq sched (busy_interval_prefix arr_seq sched) SBF.
+    pred_sbf_respected arr_seq sched bi_prefix_of_tsk SBF.
 
   (** Next, we define an SBF that is valid within a busy interval. *)
   Definition valid_busy_sbf (SBF : duration -> work) :=
-    valid_pred_sbf arr_seq sched (busy_interval_prefix arr_seq sched) SBF.
+    valid_pred_sbf arr_seq sched bi_prefix_of_tsk SBF.
 
 End BusySupplyBoundFunctions.
diff --git a/results/rs/edf/fully_nonpreemptive.v b/results/rs/edf/fully_nonpreemptive.v
index 165f9b43f99b925134d381a0fb0f053f13669c8b..5aed50b6a9639cec140ed242f19b533da4762744 100644
--- a/results/rs/edf/fully_nonpreemptive.v
+++ b/results/rs/edf/fully_nonpreemptive.v
@@ -125,10 +125,11 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** Last but not least, we assume that [SBF] properly characterizes
-      all busy intervals in [sched]. That is, (1) [SBF 0 = 0] and (2)
-      for any duration [Δ], at least [SBF Δ] supply is available in
-      any busy-interval prefix of length [Δ]. *)
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+      all busy intervals (w.r.t. task [tsk]) in [sched]. That is, (1)
+      [SBF 0 = 0] and (2) for any duration [Δ], at least [SBF Δ]
+      supply is available in any busy-interval prefix of length
+      [Δ]. *)
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
 
   (** ** Workload Abbreviation *)
 
@@ -195,7 +196,8 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - apply: busy_intervals_are_bounded_rs_edf => //.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
-      by move => ? ? ? ? ?; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+      move => ? ? ? ? [? ?]; split => //.
+      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
     - apply: instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last.
       + by (apply: bound_on_athep_workload_is_valid; try apply H_fixed_point) => //.
       + apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
diff --git a/results/rs/edf/fully_preemptive.v b/results/rs/edf/fully_preemptive.v
index 3e8222883890db46e6134877154256def3e9a770..7a865caf37f023d33ce2d40b610246dc0d2c41c2 100644
--- a/results/rs/edf/fully_preemptive.v
+++ b/results/rs/edf/fully_preemptive.v
@@ -124,10 +124,11 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
     respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** Last but not least, we assume that [SBF] properly characterizes
-      all busy intervals in [sched]. That is, (1) [SBF 0 = 0] and (2)
-      for any duration [Δ], at least [SBF Δ] supply is available in
-      any busy-interval prefix of length [Δ]. *)
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+      all busy intervals (w.r.t. task [tsk]) in [sched]. That is, (1)
+      [SBF 0 = 0] and (2) for any duration [Δ], at least [SBF Δ]
+      supply is available in any busy-interval prefix of length
+      [Δ]. *)
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
 
   (** ** Workload Abbreviation *)
 
@@ -188,7 +189,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
         exact: nonpreemptive_segments_bounded_by_blocking.
       + by rewrite BLOCK add0n; apply H_fixed_point.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
-      by move => ? ? ? ? ?; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+      move => ? ? ? ? [? ?]; split => //.
+      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
     - apply: instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last.
       + by (apply: bound_on_athep_workload_is_valid; try apply H_fixed_point) => //.
       + apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
diff --git a/results/rs/fifo/bounded_nps.v b/results/rs/fifo/bounded_nps.v
index 4f3bc630182a7dd558beb782eb5f6172380d8531..0eb2b8f48edd4cf188d3045884de54e39de2c508 100644
--- a/results/rs/fifo/bounded_nps.v
+++ b/results/rs/fifo/bounded_nps.v
@@ -138,10 +138,10 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
   Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
 
   (** Next, we assume that [SBF] properly characterizes all busy
-      intervals in [sched]. That is, (1) [SBF 0 = 0] and (2) for any
-      duration [Δ], at least [SBF Δ] supply is available in any
-      busy-interval prefix of length [Δ]. *)
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+      intervals (w.r.t. task [tsk]) in [sched]. That is, (1) [SBF 0 =
+      0] and (2) for any duration [Δ], at least [SBF Δ] supply is
+      available in any busy-interval prefix of length [Δ]. *)
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
 
   (** ** Length of Busy Interval *)
 
@@ -192,7 +192,8 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
     - eapply busy_intervals_are_bounded_rs_jlfp with (blocking_bound := fun _ => 0)=> //.
       by apply: FIFO_implies_no_service_inversion.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
-      by move => ? ? ? ? ?; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+      move => ? ? ? ? [? ?]; split => //.
+      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
     - move => t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
       move: (OFF _ _ BUSY) => EQA; subst A.
       have [ZERO|POSj] := posnP (job_cost j).
diff --git a/results/rs/fp/fully_preemptive.v b/results/rs/fp/fully_preemptive.v
index 4fe4e02cde4146e1c8e981c5a763cb69109db8a8..110b7fa4c07bba4a399c461dab5196d97d3a6abb 100644
--- a/results/rs/fp/fully_preemptive.v
+++ b/results/rs/fp/fully_preemptive.v
@@ -128,10 +128,10 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
 
   (** We assume that [SBF] properly characterizes all busy intervals
-      in [sched]. That is, (1) [SBF 0 = 0] and (2) for any duration
-      [Δ], at least [SBF Δ] supply is available in any busy-interval
-      prefix of length [Δ]. *)
-  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
+      (w.r.t. task [tsk]) in [sched]. That is, (1) [SBF 0 = 0] and (2)
+      for any duration [Δ], at least [SBF Δ] supply is available in
+      any busy-interval prefix of length [Δ]. *)
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
 
   (** ** Workload Abbreviation *)
 
@@ -203,7 +203,8 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - by apply: busy_intervals_are_bounded_rs_fp => //; rewrite BLOCK add0n.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
-      by move => *; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+      move => ? ? ? ? [? ?]; split => //.
+      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
     - apply: instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last.
       + by apply athep_workload_le_total_ohep_rbf.
       + apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.