move lemmas to avoid duplication

analysis/abstract/busy_interval.v

 Require Export prosa.analysis.abstract.iw_auxiliary.
 Require Export prosa.analysis.facts.model.workload.
+Require Export prosa.analysis.abstract.definitions.
 
 (** * Lemmas About Abstract Busy Intervals *)
 

analysis/abstract/ideal/iw_instantiation.v

@@ -344,42 +344,6 @@ Section JLFPInstantiation.
 
     End InstantiatedWorkloadEquivalence.
 
-    (** In this section, we prove that the (abstract) cumulative
-        interference of jobs with higher or equal priority is equal to
-        total service of jobs with higher or equal priority. *)
-    Section InstantiatedServiceEquivalences.
-
-      (** Consider any job [j] of [tsk]. *)
-      Variable j : Job.
-      Hypothesis H_j_arrives : arrives_in arr_seq j.
-      Hypothesis H_job_of_tsk : job_of_task tsk j.
-
-      (** We consider an arbitrary time interval <<[t1, t)>> that
-          starts with a quiet time. *)
-      Variable t1 t : instant.
-      Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
-
-      (** As follows from lemma [cumulative_pred_served_eq_service],
-          the (abstract) instantiated function of interference is
-          equal to the total service of any subset of jobs with higher
-          or equal priority. *)
-
-      (** The above is in particular true for the jobs other
-          than [j] with higher or equal priority... *)
-      Lemma  cumulative_i_ohep_eq_service_of_ohep :
-        cumulative_another_hep_job_interference arr_seq sched j t1 t
-        = service_of_other_hep_jobs arr_seq sched j t1 t.
-      Proof. by apply: cumulative_pred_served_eq_service => // => ? /andP[]. Qed.
-
-      (** ...and for jobs from other tasks than [j] with higher
-          or equal priority. *)
-      Lemma cumulative_i_thep_eq_service_of_othep :
-        cumulative_another_task_hep_job_interference arr_seq sched j t1 t
-        = service_of_other_task_hep_jobs arr_seq sched j t1 t.
-      Proof. by apply: cumulative_pred_served_eq_service => // => ? /andP[]. Qed.
-
-    End InstantiatedServiceEquivalences.
-
     (** In this section we prove that the abstract definition of busy
         interval is equivalent to the conventional, concrete
         definition of busy interval for JLFP scheduling. *)
@@ -390,15 +354,15 @@ Section JLFPInstantiation.
           notion of quiet time in the _abstract_ sense as
           [quiet_time_ab]. *)
       Let quiet_time_cl := classical.quiet_time arr_seq sched.
-      Let quiet_time_ab := definitions.quiet_time sched.
+      Let quiet_time_ab := abstract.definitions.quiet_time sched.
 
       (** Same for the two notions of a busy interval prefix ... *)
       Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
-      Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
+      Let busy_interval_prefix_ab := abstract.definitions.busy_interval_prefix sched.
 
       (** ... and the two notions of a busy interval. *)
       Let busy_interval_cl := classical.busy_interval arr_seq sched.
-      Let busy_interval_ab := definitions.busy_interval sched.
+      Let busy_interval_ab := abstract.definitions.busy_interval sched.
 
       (** Consider any job j of [tsk]. *)
       Variable j : Job.
@@ -445,8 +409,7 @@ Section JLFPInstantiation.
         erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
         erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
         replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
-        rewrite -/(service_of_other_hep_jobs arr_seq _ j 0 t) -cumulative_i_ohep_eq_service_of_ohep; eauto;
-          last by move => ? _ _ ; unfold arrived_before; lia.
+        rewrite -/(service_of_other_hep_jobs arr_seq _ j 0 t) -cumulative_i_ohep_eq_service_of_ohep => //.
         rewrite -/(workload_of_other_hep_jobs _ j 0 t) -cumulative_iw_hep_eq_workload_of_ohep; eauto.
         move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
         { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.

analysis/abstract/iw_auxiliary.v

@@ -2,6 +2,9 @@ Require Export prosa.analysis.definitions.interference.
 Require Export prosa.analysis.definitions.task_schedule.
 Require Export prosa.analysis.facts.priority.classes.
 Require Export prosa.analysis.abstract.restricted_supply.busy_prefix.
+Require Export prosa.model.aggregate.service_of_jobs.
+Require Export prosa.analysis.facts.model.service_of_jobs.
+
 
 (** * Auxiliary Lemmas About Interference and Interfering Workload. *)
 
@@ -416,6 +419,53 @@ Section InterferenceAndInterferingWorkloadAuxiliary.
 
     End SupplyAndScheduledJob.
 
+    (** In this section, we prove that the (abstract) cumulative
+        interference of jobs with higher or equal priority is equal to
+        total service of jobs with higher or equal priority. *)
+    Section InstantiatedServiceEquivalences.
+
+      (** First, let us assume that the introduced processor model is
+          unit-service. *)
+      Hypothesis H_unit_service : unit_service_proc_model PState.
+
+      (** Consider any job [j] of [tsk]. *)
+      Variable j : Job.
+      Hypothesis H_j_arrives : arrives_in arr_seq j.
+      Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+      (** We consider an arbitrary time interval <<[t1, t)>> that
+          starts with a (classic) quiet time. *)
+      Variable t1 t : instant.
+      Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
+
+      (** As follows from lemma [cumulative_pred_served_eq_service],
+          the (abstract) instantiated function of interference is
+          equal to the total service of any subset of jobs with higher
+          or equal priority. *)
+
+      (** The above is in particular true for the jobs other
+          than [j] with higher or equal priority... *)
+      Lemma  cumulative_i_ohep_eq_service_of_ohep :
+        cumulative_another_hep_job_interference arr_seq sched j t1 t
+        = service_of_other_hep_jobs arr_seq sched j t1 t.
+      Proof.
+        apply: cumulative_pred_served_eq_service => //.
+        - by move => ? /andP[].
+      Qed.
+
+      (** ...and for jobs from other tasks than [j] with higher
+          or equal priority. *)
+      Lemma cumulative_i_thep_eq_service_of_othep :
+        cumulative_another_task_hep_job_interference arr_seq sched j t1 t
+        = service_of_other_task_hep_jobs arr_seq sched j t1 t.
+      Proof.
+        apply: cumulative_pred_served_eq_service => //.
+        by move => ? /andP[].
+      Qed.
+
+    End InstantiatedServiceEquivalences.
+
+
   End Equivalences.
 
 End InterferenceAndInterferingWorkloadAuxiliary.

analysis/abstract/restricted_supply/bounded_bi/aux.v

@@ -156,7 +156,10 @@ 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 cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //;
+            [
+            | exact: unit_supply_is_unit_service
+            | by apply PREF ].
     rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _ )]addnC.
     rewrite workload_job_and_ahep_eq_workload_hep //.
     rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.

analysis/abstract/restricted_supply/iw_instantiation.v

@@ -249,50 +249,6 @@ Section JLFPInstantiation.
 
     End InstantiatedWorkloadEquivalence.
 
-    (** In this section, we prove that the (abstract) cumulative
-        interference of jobs with higher or equal priority is equal to
-        total service of jobs with higher or equal priority. *)
-    Section InstantiatedServiceEquivalences.
-
-      (** Consider any job [j] of [tsk]. *)
-      Variable j : Job.
-      Hypothesis H_j_arrives : arrives_in arr_seq j.
-      Hypothesis H_job_of_tsk : job_of_task tsk j.
-
-      (** We consider an arbitrary time interval <<[t1, t)>> that
-          starts with a (classic) quiet time. *)
-      Variable t1 t : instant.
-      Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
-
-      (** As follows from lemma [cumulative_pred_served_eq_service],
-          the (abstract) instantiated function of interference is
-          equal to the total service of any subset of jobs with higher
-          or equal priority. *)
-
-      (** The above is in particular true for the jobs other
-          than [j] with higher or equal priority... *)
-      Lemma  cumulative_i_ohep_eq_service_of_ohep :
-        cumulative_another_hep_job_interference arr_seq sched j t1 t
-        = service_of_other_hep_jobs arr_seq sched j t1 t.
-      Proof.
-        apply: cumulative_pred_served_eq_service => //.
-        - by apply unit_supply_is_unit_service.
-        - by move => ? /andP[].
-      Qed.
-
-      (** ...and for jobs from other tasks than [j] with higher
-          or equal priority. *)
-      Lemma cumulative_i_thep_eq_service_of_othep :
-        cumulative_another_task_hep_job_interference arr_seq sched j t1 t
-        = service_of_other_task_hep_jobs arr_seq sched j t1 t.
-      Proof.
-        apply: cumulative_pred_served_eq_service => //.
-        - by apply unit_supply_is_unit_service.
-        - by move => ? /andP[].
-      Qed.
-
-    End InstantiatedServiceEquivalences.
-
     (** In this section we prove that the abstract definition of busy
         interval is equivalent to the conventional, concrete
         definition of busy interval for JLFP scheduling. *)
@@ -303,15 +259,15 @@ Section JLFPInstantiation.
           notion of quiet time in the _abstract_ sense as
           [quiet_time_ab]. *)
       Let quiet_time_cl := classical.quiet_time arr_seq sched.
-      Let quiet_time_ab := definitions.quiet_time sched.
+      Let quiet_time_ab := abstract.definitions.quiet_time sched.
 
       (** Same for the two notions of a busy interval prefix ... *)
       Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
-      Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
+      Let busy_interval_prefix_ab := abstract.definitions.busy_interval_prefix sched.
 
       (** ... and the two notions of a busy interval. *)
       Let busy_interval_cl := classical.busy_interval arr_seq sched.
-      Let busy_interval_ab := definitions.busy_interval sched.
+      Let busy_interval_ab := abstract.definitions.busy_interval sched.
 
       (** Consider any job [j] of [tsk]. *)
       Variable j : Job.
@@ -332,7 +288,8 @@ Section JLFPInstantiation.
         { rewrite negb_and negbK; apply/orP.
           by case ARR: (arrived_before j t); [right | left]; [apply QT | ]. }
         { erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l.
-          rewrite cumulative_i_ohep_eq_service_of_ohep//.
+          rewrite cumulative_i_ohep_eq_service_of_ohep //=; last first.
+          { exact: unit_supply_is_unit_service. }
           rewrite //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
           apply all_jobs_have_completed_equiv_workload_eq_service => //.
           { by apply unit_supply_is_unit_service. }
@@ -357,7 +314,8 @@ Section JLFPInstantiation.
         erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
         erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
         replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
-        rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //.
+        rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //; last first.
+        { exact: unit_supply_is_unit_service. }
         rewrite -/(workload_of_other_hep_jobs arr_seq j 0 t) -cumulative_iw_hep_eq_workload_of_ohep //.
         move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
         { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
@@ -586,8 +544,8 @@ Section JLFPInstantiation.
     Proof.
       move=> j t1.
       rewrite cumulative_interference_split cumulative_interfering_workload_split.
-      rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep; last first.
-      { by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
+      rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep //=; last first.
+      { exact: unit_supply_is_unit_service. }
       rewrite cumulative_iw_hep_eq_workload_of_ohep.
       apply service_of_jobs_le_workload => //.
       by apply unit_supply_is_unit_service.

analysis/abstract/restricted_supply/task_intra_interference_bound.v

@@ -110,6 +110,7 @@ Section TaskIntraInterferenceIsBounded.
       by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + Δ)) //= leq_addr. }
     { erewrite cumulative_i_thep_eq_service_of_othep; eauto 2 => //; last first.
       { by apply instantiated_quiet_time_equivalent_quiet_time => //; apply BUSY. }
+      { exact: unit_supply_is_unit_service. }
       apply: leq_trans.
       { by apply service_of_jobs_le_workload => //; apply unit_supply_is_unit_service. }
       { apply H_workload_is_bounded => //; apply: abstract_busy_interval_classic_quiet_time => //. }

analysis/facts/priority/fifo_ahep_bound.v

+Require Export prosa.analysis.abstract.iw_auxiliary.
+Require Export prosa.analysis.facts.model.restricted_supply.schedule.
+Require Import prosa.analysis.facts.priority.fifo.
+Require Import prosa.analysis.facts.model.rbf.
+
+
+(** * Higher-or-Equal-Priority Interference Bound under FIFO *)
+
+(** In this file, we introduce a bound on the cumulative interference
+    from higher- and equal-priority under FIFO scheduling. *)
+Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost] and an arrival curve [max_arrivals] ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{MaxArrivals Task}.
+
+  (** ... and any type of jobs associated with these tasks, where each
+      job has a task [job_task], a cost [job_cost], and an arrival
+      time [job_arrival]. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (** Consider any kind of unit-supply uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+
+  (** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** We further require that a job's cost cannot exceed its task's stated WCET. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** We consider an arbitrary task set [ts] ... *)
+  Variable ts : seq Task.
+
+  (** ... and assume that all jobs stem from tasks in this task set. *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** We assume that [max_arrivals] is a family of valid arrival
+      curves that constrains the arrival sequence [arr_seq], i.e., for
+      any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+      bound of [tsk], and ... *)
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
+  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider any schedule ... *)
+  Variable sched : schedule PState.
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Next, we establish a bound on the interference produced by higher- and
+      equal-priority jobs. *)
+
+  (** Consider a job [j] of the task under analysis [tsk] with a positive cost. *)
+  Variable j : Job.
+  Hypothesis H_job_of_task : job_of_task tsk j.
+  Hypothesis H_j_in_arrivals : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** Consider the busy window of [j] and denote it as <<[t1, t2)>>. *)
+  Variable t1 t2 : instant.
+  Hypothesis H_busy_window : classical.busy_interval arr_seq sched j t1 t2.
+
+  (** Consider any arbitrary sub-interval <<[t1, Δ)>> within the busy
+      window of [j]. *)
+  Variable Δ : instant.
+  Hypothesis H_in_busy : t1 + Δ < t2.
+
+  (** The cumulative interference from higher- and equal-priority jobs
+      during <<[t1, Δ)>> is bounded as follows. *)
+  Lemma bound_on_hep_workload :
+    cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <=
+      \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + ε) - task_cost tsk.
+  Proof.
+    move: (H_busy_window) => [[_ [_ [_ /andP [ARR1 ARR2]]]] _].
+    rewrite (cumulative_i_ohep_eq_service_of_ohep _ arr_seq) => //; last  eauto 6 with basic_rt_facts; last first.
+    { by move: (H_busy_window) => [[_ [Q _]] _]. }
+    { exact: unit_supply_is_unit_service. }
+    eapply leq_trans.
+    { apply service_of_jobs_le_workload => //.
+      by apply unit_supply_is_unit_service. }
+    rewrite (leqRW (workload_equal_subset _ _ _ _ _ _  _)) => //.
+    rewrite (workload_minus_job_cost j)//;
+            last by apply job_in_arrivals_between => //; last by rewrite addn1.
+    rewrite /workload_of_jobs (big_rem tsk) //=
+            (addnC (task_request_bound_function tsk (job_arrival j - t1 + ε))).
+    rewrite -addnBA; last first.
+    - apply leq_trans with (task_request_bound_function tsk ε).
+      { by apply: task_rbf_1_ge_task_cost; exact: non_pathological_max_arrivals. }
+      { by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
+    - eapply leq_trans; last first.
+      { by erewrite leq_add2l; apply task_rbf_without_job_under_analysis; (try apply ARR1) => //; lia. }
+      rewrite addnBA.
+      + rewrite leq_sub2r //; eapply leq_trans.
+        * apply sum_over_partitions_le => j' inJOBS => _.
+          by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
+        * rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite addnA subnKC.
+          rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.
+          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.
+      + 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.
+        apply job_in_arrivals_between => //.
+        by lia.
+  Qed.
+
+End RTAforFullyPreemptiveFIFOModelwithArrivalCurves.

results/fifo/rta.v

 Require Import prosa.model.readiness.basic.
 Require Import prosa.analysis.facts.priority.fifo.
+Require Export prosa.analysis.facts.priority.fifo_ahep_bound.
 Require Export prosa.analysis.abstract.ideal.cumulative_bounds.
 Require Export prosa.analysis.abstract.ideal.abstract_rta.
 Require Export prosa.analysis.facts.model.task_cost.
@@ -274,70 +275,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
 
   (** *** Higher- and Equal-Priority Interference *)
 
-  (** Next, we establish a bound on the interference produced by higher- and
-      equal-priority jobs. *)
-  Section BoundOnHEPWorkload.
-
-    (** Consider again a job [j] of the task under analysis [tsk] with a positive cost. *)
-    Variable j : Job.
-    Hypothesis H_job_of_task : job_of_task tsk j.
-    Hypothesis H_j_in_arrivals : arrives_in arr_seq j.
-    Hypothesis H_job_cost_positive : job_cost_positive j.
-
-    (** Consider the (abstract) busy window of [j] and denote it as  <<[t1, t2)>>. *)
-    Variable t1 t2 : instant.
-    Hypothesis H_busy_window :
-      definitions.busy_interval sched j t1 t2.
-
-    (** Consider any arbitrary sub-interval <<[t1, Δ)>> within the busy window
-        of [j]. *)
-    Variable Δ : instant.
-    Hypothesis H_in_busy : t1 + Δ < t2.
-
-    (** The cumulative interference from higher- and equal-priority jobs during
-        <<[t1, Δ)>> is bounded as follows. *)
-    Lemma bound_on_hep_workload :
-      cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <=
-        \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + ε) - task_cost tsk.
-    Proof.
-      rewrite (cumulative_i_ohep_eq_service_of_ohep arr_seq) => //;
-        last by eauto 6 with basic_rt_facts.
-      eapply leq_trans; first exact: service_of_jobs_le_workload.
-      rewrite (leqRW (workload_equal_subset _ _ _ _ _ _  _)) => //.
-      rewrite (workload_minus_job_cost j)//;
-        last by apply job_in_arrivals_between => //; last by rewrite addn1.
-      rewrite /workload_of_jobs /IBF (big_rem tsk) //=
-        (addnC (task_request_bound_function tsk (job_arrival j - t1 + ε))).
-      rewrite -addnBA; last first.
-      - apply leq_trans with (task_request_bound_function tsk ε).
-        { by apply: task_rbf_1_ge_task_cost; exact: non_pathological_max_arrivals. }
-        { by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
-      - eapply leq_trans;
-          last by (
-            erewrite leq_add2l;
-            eapply task_rbf_without_job_under_analysis with (t1 := t1) =>//;
-            lia).
-        rewrite addnBA.
-        + rewrite leq_sub2r //; eapply leq_trans.
-          * apply sum_over_partitions_le => j' inJOBS => _.
-            by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
-          * rewrite (big_rem tsk) //= addnC leq_add //;
-              last by rewrite addnBAC //= subnKC // addn1; apply leqW.
-            rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.
-            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.
-        + 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.
-          apply job_in_arrivals_between => //.
-          by lia.
-    Qed.
-
-  End BoundOnHEPWorkload.
+  (** We establish a bound on the interference produced by higher- and
+      equal-priority jobs in a separate file. To see the result,
+      simply click on the link bellow. *)
+  Let bound_on_hep_workload :=
+    @analysis.facts.priority.fifo_ahep_bound.bound_on_hep_workload.
 
   (** *** Correctness of [IBF]  *)
 
@@ -361,7 +303,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
     have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; lia.
     rewrite (no_priority_inversion j ARRj _ JPOS _ t2) //= add0n.
     have ->: A = job_arrival j - t1 by erewrite Pred with (t1 := t1); [lia | apply BUSY].
-    exact: bound_on_hep_workload.
+    apply: bound_on_hep_workload; (try apply IN_BUSY) => //.
+    by apply instantiated_busy_interval_equivalent_busy_interval.
   Qed.
 
   (** The preceding lemma [IBF_correct] corresponds to Lemma 3 in the paper. To