diff --git a/analysis/abstract/restricted_supply/fp_bounded_bi.v b/analysis/abstract/restricted_supply/fp_bounded_bi.v
index 93d678eeeea6678ef14805874d890e03c2afd136..f4ebfe7468d786beb2cb7303d8cd16830750ab5f 100644
--- a/analysis/abstract/restricted_supply/fp_bounded_bi.v
+++ b/analysis/abstract/restricted_supply/fp_bounded_bi.v
@@ -1,4 +1,4 @@
- Require Export prosa.analysis.facts.blocking_bound_fp.
+ Require Export prosa.analysis.facts.blocking_bound.fp.
 Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
 Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
 Require Export prosa.analysis.definitions.sbf.busy.
@@ -184,7 +184,7 @@ Section BoundedBusyIntervals.
         rewrite -(leqRW H_fixed_point); apply leq_add.
         - apply: leq_trans; first apply: service_inversion_is_bounded => //.
           + instantiate (1 := fun _ => blocking_bound ts tsk) => //=.
-            by move=> jo t t' ARRo TSKo PREFo; apply: priority_inversion_is_bounded_by_blocking => //.
+            by move=> jo t t' ARRo TSKo PREFo; apply: nonpreemptive_segments_bounded_by_blocking => //.
           + by done.
         - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
           by apply hep_workload_le_total_hep_rbf.
@@ -339,7 +339,7 @@ Section BoundedBusyIntervals.
             - apply: leq_trans.
               + apply: service_inversion_is_bounded => //.
                 move => *; instantiate (1 := fun _ => blocking_bound ts tsk) => //.
-                by apply: priority_inversion_is_bounded_by_blocking => //.
+                by apply: nonpreemptive_segments_bounded_by_blocking => //.
               + by done.
             - by done.
             - lia.
diff --git a/analysis/abstract/restricted_supply/search_space_fp.v b/analysis/abstract/restricted_supply/search_space_fp.v
index fcb0fdfd19407753d56be9afa65461be0cf92c12..9459d14c74f992821f808755a110e1f7c457f2dd 100644
--- a/analysis/abstract/restricted_supply/search_space_fp.v
+++ b/analysis/abstract/restricted_supply/search_space_fp.v
@@ -1,6 +1,6 @@
 Require Export prosa.analysis.facts.model.rbf.
 Require Export prosa.analysis.abstract.search_space.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
 
 
 (** * Abstract Search Space is a Subset of Restricted Supply FP Search Space *)
@@ -50,9 +50,10 @@ Section SearchSpaceSubset.
   Let task_rbf := task_request_bound_function tsk.
   Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
 
-  (** Let [L] be any positive constant. Typically, [L] denotes an
-      upper bound on the length of a busy interval of a [tsk]'s upper
-      bound on the length of a busy interval of any job of [tsk]. *)
+  (** Let [L] be an arbitrary positive constant. Typically, [L]
+      denotes an upper bound on the length of a busy interval of a job
+      of [tsk]. In this file, however, [L] can be any positive
+      constant. *)
   Variable L : duration.
   Hypothesis H_L_positive : 0 < L.
 
diff --git a/analysis/definitions/blocking_bound_edf.v b/analysis/definitions/blocking_bound/edf.v
similarity index 100%
rename from analysis/definitions/blocking_bound_edf.v
rename to analysis/definitions/blocking_bound/edf.v
diff --git a/analysis/definitions/blocking_bound_fp.v b/analysis/definitions/blocking_bound/fp.v
similarity index 100%
rename from analysis/definitions/blocking_bound_fp.v
rename to analysis/definitions/blocking_bound/fp.v
diff --git a/analysis/facts/blocking_bound/edf.v b/analysis/facts/blocking_bound/edf.v
new file mode 100644
index 0000000000000000000000000000000000000000..1747816672096c3241fbe43bc324d23a3c33d92a
--- /dev/null
+++ b/analysis/facts/blocking_bound/edf.v
@@ -0,0 +1,103 @@
+Require Export prosa.analysis.definitions.blocking_bound.edf.
+Require Export prosa.analysis.facts.busy_interval.pi.
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.facts.model.arrival_curves.
+
+(** * Lower-Priority Non-Preemptive Segment is Bounded *)
+(** In this file, we prove that, under the EDF scheduling policy, the
+    length of the maximum non-preemptive segment of a lower-priority
+    job (w.r.t. a job of a task [tsk]) is bounded by
+    [blocking_bound]. *)
+Section  MaxNPSegmentIsBounded.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost], an arrival curve [max_arrivals], a relative
+      deadline [task_deadline], and a bound on the the task's longest
+      non-preemptive segment [task_max_nonpreemptive_segment] ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{MaxArrivals Task}.
+  Context `{TaskDeadline Task}.
+  Context `{TaskMaxNonpreemptiveSegment 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 processor state model. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider the EDF policy. *)
+  Let EDF := EDF Job.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** 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.
+
+  (** ... and assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : seq Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let [max_arrivals] be a family of arrival curves. *)
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Consider any job [j] of [tsk]. *)
+  Variable j : Job.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+  (** Then, the maximum length of a nonpreemptive segment among all
+      lower-priority jobs (w.r.t. the given job [j]) arrived so far is
+      bounded by [blocking_bound]. *)
+  Lemma nonpreemptive_segments_bounded_by_blocking :
+    forall t1 t2,
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).
+  Proof.
+    move=> t1 t2 BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound.
+    apply: leq_trans;first by exact: max_np_job_segment_bounded_by_max_np_task_segment.
+    apply /bigmax_leq_seqP => j' JINB NOTHEP.
+    have ARR': arrives_in arr_seq j'
+      by apply: in_arrivals_implies_arrived; exact: JINB.
+    apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
+      first by apply H_all_jobs_from_taskset.
+    apply in_arrivals_implies_arrived_between in JINB => [|//].
+    move: JINB; move => /andP [_ TJ'].
+    repeat (apply/andP; split); last first.
+    { rewrite /hep_job -ltnNge in NOTHEP.
+      move: H_job_of_tsk => /eqP <-.
+      have ARRLE: job_arrival j' < job_arrival j.
+      { by apply: (@leq_trans t1) => //; move: BUSY => [ _  [ _ [ _ /andP [F G]]] ]. } 
+      move: NOTHEP; rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline.
+      by lia. }
+    { move: NOTHEP => /andP [_ NZ].
+      move: (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.
+      by lia. }
+    { apply: non_pathological_max_arrivals; last first.
+      - exact: ARR'.
+      - by rewrite /job_of_task.
+      - by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
+  Qed.
+
+End MaxNPSegmentIsBounded.
diff --git a/analysis/facts/blocking_bound_fp.v b/analysis/facts/blocking_bound/fp.v
similarity index 96%
rename from analysis/facts/blocking_bound_fp.v
rename to analysis/facts/blocking_bound/fp.v
index 45f83b186207b5d0de09e0554565ccb6562184e4..168efede0cd7dad5e85e6da09e147a35c6e44d23 100644
--- a/analysis/facts/blocking_bound_fp.v
+++ b/analysis/facts/blocking_bound/fp.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
 Require Export prosa.analysis.facts.busy_interval.pi.
 
 
@@ -57,7 +57,7 @@ Section  MaxNPSegmentIsBounded.
   (** Then, the maximum length of a nonpreemptive segment among all
       lower-priority jobs (w.r.t. the given job [j]) arrived so far is
       bounded by [blocking_bound]. *)
-  Lemma priority_inversion_is_bounded_by_blocking :
+  Lemma nonpreemptive_segments_bounded_by_blocking :
     forall t,
       max_lp_nonpreemptive_segment arr_seq j t <= blocking_bound ts tsk.
   Proof.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index bb9605acf4763315a03c0c457710bcbb51ad7d00..15ac234bb9af835b8e383e3d9c0533d287bb396f 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -3,9 +3,9 @@ Require Import prosa.model.readiness.basic.
 Require Export prosa.analysis.facts.busy_interval.pi_bound.
 Require Export prosa.analysis.facts.busy_interval.arrival.
 Require Export prosa.results.edf.rta.bounded_pi.
-Require Export model.schedule.work_conserving.
-Require Export analysis.definitions.busy_interval.
-Require Export analysis.definitions.blocking_bound_edf.
+Require Export prosa.model.schedule.work_conserving.
+Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.facts.blocking_bound.edf.
 
 (** * RTA for EDF  with Bounded Non-Preemptive Segments *)
 
@@ -199,51 +199,6 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
    Qed.
 
 
-  (** ** Priority inversion is bounded *)
-  (** In this section, we prove that a priority inversion for task [tsk] is bounded by
-      the maximum length of non-preemptive segments among the tasks with lower priority. *)
-  Section PriorityInversionIsBounded.
-
-    (** Since EDF is a JLFP policy, the maximum non-preemptive segment length of any task
-        that releases a job with an earlier absolute deadline (w.r.t. a given job [j]) and
-        non-zero execution cost upper-bounds the maximum possible length of priority
-        inversion (experienced by said job [j]). *)
-
-    (** Using this fact, we prove that the maximum length of a priority inversion of a given
-        job [j] is indeed bounded by the defined blocking bound. *)
-    Lemma priority_inversion_is_bounded_by_blocking:
-      forall j t1 t2,
-        arrives_in arr_seq j ->
-        job_of_task tsk j ->
-        busy_interval_prefix  arr_seq sched j t1 t2 ->
-        max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).
-    Proof.
-      move=> j t1 t2 ARR TSK BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound.
-      apply: leq_trans;first by exact: max_np_job_segment_bounded_by_max_np_task_segment.
-      apply /bigmax_leq_seqP => j' JINB NOTHEP.
-      have ARR': arrives_in arr_seq j'
-        by apply: in_arrivals_implies_arrived; exact: JINB.
-      apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
-        first by apply H_all_jobs_from_taskset.
-      apply in_arrivals_implies_arrived_between in JINB => [|//].
-      move: JINB; move => /andP [_ TJ'].
-      repeat (apply/andP; split); last first.
-      { rewrite /EDF -ltnNge in NOTHEP.
-        move: TSK => /eqP <-.
-        have ARRLE: job_arrival j' < job_arrival j by apply: (@leq_trans t1).
-        move: NOTHEP; rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline /D.
-        by lia. }
-      { move: NOTHEP => /andP [_ NZ].
-        move: (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.
-        by lia. }
-      { apply: non_pathological_max_arrivals; last first.
-          - exact: ARR'.
-          - by rewrite /job_of_task.
-          - by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
-    Qed.
-
-  End PriorityInversionIsBounded.
-
   (** ** Response-Time Bound *)
   (** In this section, we prove that the maximum among the solutions of the response-time
       bound recurrence is a response-time bound for [tsk]. *)
@@ -278,7 +233,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Proof.
       apply: uniprocessor_response_time_bound_edf; eauto 4 with basic_rt_facts.
       { apply: priority_inversion_is_bounded => //.
-        apply: priority_inversion_is_bounded_by_blocking. }
+        by move=> *; apply: nonpreemptive_segments_bounded_by_blocking. }
       - move=> A BPI_SP.
         by apply H_R_is_maximum, search_space_inclusion.
     Qed.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 1ca4ae122dfc7a70e44991b2d669ae2acfe9eee0..fd4ae79c9fdc2c242e96d325fc925b880c891bae 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -3,7 +3,7 @@ Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
 Require Import prosa.model.priority.edf.
-Require Export prosa.analysis.definitions.blocking_bound_edf.
+Require Export prosa.analysis.definitions.blocking_bound.edf.
 
 (** * RTA for EDF with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 2b1560bc7b3d7b21b29328c38eb0439a7c0987d6..91dd7788cf5b7531c11f722ca403aac36a9ef3a3 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -129,8 +129,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Proof.
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L:=L) => //.
     move => A /andP [LT CHANGE].
-    have BLOCK: forall A', blocking_bound_edf.blocking_bound ts tsk A' = blocking_bound A'.
-    { by move=> A'; rewrite /blocking_bound_edf.blocking_bound /parameters.task_max_nonpreemptive_segment
+    have BLOCK: forall A', edf.blocking_bound ts tsk A' = blocking_bound A'.
+    { by move=> A'; rewrite /edf.blocking_bound /parameters.task_max_nonpreemptive_segment
          /fully_preemptive_task_model subnn big1_eq. }
     specialize (H_R_is_maximum A); feed H_R_is_maximum; first by apply/andP; split; done.
     move: H_R_is_maximum => [F [FIX BOUND]].
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index ae47221d5f340f5cdae73deed4937516ff448c07..26819293c2648f2ae17e5cac716142857f7e246e 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -4,7 +4,7 @@ Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.basic.
 Require Export prosa.model.task.preemption.limited_preemptive.
 Require Export prosa.model.priority.edf.
-Require Export prosa.analysis.definitions.blocking_bound_edf.
+Require Export prosa.analysis.definitions.blocking_bound.edf.
 
 (** * RTA for EDF with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 9d319066c203ff1024fb0979d1daaf3efba4c78b..2f67d52b2733ea81d85129a6d1205240bc1d4d37 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -2,7 +2,7 @@ Require Export prosa.analysis.facts.busy_interval.pi_bound.
 Require Export prosa.results.fixed_priority.rta.bounded_pi.
 Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.definitions.busy_interval.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
 
 (** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
 
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 189642013de05442cbc0cea294324e1e23d2427a..c0c19d376cac7648efba0d438dc7f2b9d527a7b5 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,7 +1,7 @@
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
 
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 240853fd182be074e9fd5f0e01aa16d700640b2c..81b0c74aaada454a52c9a991609746d946abdb2a 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -2,7 +2,7 @@ Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.sequential.
 Require Export prosa.model.task.preemption.limited_preemptive.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
 
 (** * RTA for FP-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with
diff --git a/results/rs/fp/fully_preemptive.v b/results/rs/fp/fully_preemptive.v
index 731efe96eef58ef4777a38b83a6a6d50e7df0566..6c5b9deba1b88ac892790f3a2d3be665af67c2d4 100644
--- a/results/rs/fp/fully_preemptive.v
+++ b/results/rs/fp/fully_preemptive.v
@@ -205,7 +205,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
     - 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.
-        by unshelve rewrite (leqRW (priority_inversion_is_bounded_by_blocking _ _ _ _ _ _ _ _ _)) => //.
+        by unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) => //.
     - move => A SP; move: (H_R_is_maximum A) => [].
       + apply: search_space_sub => //; apply: search_space_switch_IBF; last by exact: SP.
         by move=> A1 Δ1; rewrite //= BLOCK.