diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 0ef944e27c193b36189cb5ec7fe07a1b8665d896..37cfb8f646098506435bf6658fa4a3d891e3bd01 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -200,8 +200,9 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Let interfering_workload (j : Job) (t : instant) :=
     ideal_jlfp_rta.interfering_workload arr_seq sched j t.
 
-  (** Finally, we define the interference bound function as the sum of the priority 
-     interference bound and the higher-or-equal-priority workload. *)
+  (** Finally, we define the interference bound function (IBF_other). IBF_other bounds the interference if tasks are sequential.
+      Since tasks are sequential, we exclude interference from other jobs of the same task. For EDF, we define IBF_other as the sum of the priority 
+      interference bound and the higher-or-equal-priority workload. *)
   Let IBF_other (A R : duration) := priority_inversion_bound + bound_on_total_hep_workload A R.
 
   (** ** Filling Out Hypothesis Of Abstract RTA Theorem *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index f336a702a1602b6a4cd70e032ae5d4e5862099b0..13d5c467013d71ff1220f9c4012f6644acade164 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -171,7 +171,8 @@ Section AbstractRTAforFPwithArrivalCurves.
   Let interfering_workload (j : Job) (t : instant) :=
     ideal_jlfp_rta.interfering_workload arr_seq sched j t.
   
-  (** Finally, we define the interference bound function as the sum of the priority 
+  (** Finally, we define the interference bound function (IBF_other). IBF_other bounds the interference if tasks are sequential.
+      Since tasks are sequential, we exclude interference from other jobs of the same task. For FP, we define IBF_other as the sum of the priority 
       interference bound and the higher-or-equal-priority workload. *)
   Let IBF_other (R : duration) := priority_inversion_bound + total_ohep_rbf R.