diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index cad93d2d939ef9a318d91b0bedbfa486f6fabd63..73f0c97ec7c05e87da86f0e3805aaf30c25c0cd2 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -357,7 +357,7 @@ Section JLFPInstantiation.
       (** We consider an arbitrary time interval <<[t1, t)>> that
           starts with a quiet time. *)
       Variable t1 t : instant.
-      Hypothesis H_quiet_time : busy_interval.quiet_time arr_seq sched j t1.
+      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
@@ -389,15 +389,15 @@ Section JLFPInstantiation.
           time in the _classical_ sense as [quiet_time_cl], and the
           notion of quiet time in the _abstract_ sense as
           [quiet_time_ab]. *)
-      Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.
+      Let quiet_time_cl := classical.quiet_time arr_seq sched.
       Let quiet_time_ab := definitions.quiet_time sched.
 
       (** Same for the two notions of a busy interval prefix ... *)
-      Let busy_interval_prefix_cl := busy_interval.busy_interval_prefix arr_seq sched.
+      Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
       Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
 
       (** ... and the two notions of a busy interval. *)
-      Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.
+      Let busy_interval_cl := classical.busy_interval arr_seq sched.
       Let busy_interval_ab := definitions.busy_interval sched.
 
       (** Consider any job j of [tsk]. *)
diff --git a/analysis/abstract/restricted_supply/iw_instantiation.v b/analysis/abstract/restricted_supply/iw_instantiation.v
index 615646024f2b243052d338f865e09c014c05cf21..be5e088391248ff163d8c1c8ed32522bd3d09a59 100644
--- a/analysis/abstract/restricted_supply/iw_instantiation.v
+++ b/analysis/abstract/restricted_supply/iw_instantiation.v
@@ -241,7 +241,7 @@ Section JLFPInstantiation.
       (** We consider an arbitrary time interval <<[t1, t)>> that
           starts with a (classic) quiet time. *)
       Variable t1 t : instant.
-      Hypothesis H_quiet_time : busy_interval.quiet_time arr_seq sched j t1.
+      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
@@ -281,15 +281,15 @@ Section JLFPInstantiation.
           time in the _classical_ sense as [quiet_time_cl], and the
           notion of quiet time in the _abstract_ sense as
           [quiet_time_ab]. *)
-      Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.
+      Let quiet_time_cl := classical.quiet_time arr_seq sched.
       Let quiet_time_ab := definitions.quiet_time sched.
 
       (** Same for the two notions of a busy interval prefix ... *)
-      Let busy_interval_prefix_cl := busy_interval.busy_interval_prefix arr_seq sched.
+      Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
       Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
 
       (** ... and the two notions of a busy interval. *)
-      Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.
+      Let busy_interval_cl := classical.busy_interval arr_seq sched.
       Let busy_interval_ab := definitions.busy_interval sched.
 
       (** Consider any job [j] of [tsk]. *)
@@ -454,7 +454,7 @@ Section JLFPInstantiation.
 
     (** ... as well as notions of busy interval prefix. *)
     Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
-    Let busy_interval_prefix_cl := busy_interval.busy_interval_prefix arr_seq sched.
+    Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
 
     (** We assume that the schedule is a work-conserving schedule in
         the _classical_ sense, and later prove that the hypothesis
diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval/classical.v
similarity index 100%
rename from analysis/definitions/busy_interval.v
rename to analysis/definitions/busy_interval/classical.v
diff --git a/analysis/definitions/priority_inversion.v b/analysis/definitions/priority_inversion.v
index e4c0914a014b3159c3f711903ef9a633ab73795b..1a3acda306b537a9a4224cf0fb93f996beee7294 100644
--- a/analysis/definitions/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 Require Export prosa.analysis.facts.model.scheduled.
 
 (** * Priority Inversion *)
diff --git a/analysis/definitions/sbf/busy.v b/analysis/definitions/sbf/busy.v
index dde4ed2e31c93bb9656466bd1baccad68eb1d8b3..afede54d41f00f7303053ec451e4c1b70d638d70 100644
--- a/analysis/definitions/sbf/busy.v
+++ b/analysis/definitions/sbf/busy.v
@@ -1,6 +1,6 @@
 Require Export prosa.util.all.
 Require Export prosa.analysis.definitions.sbf.pred.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 
 (** * SBF within Busy Interval *)
 
diff --git a/analysis/definitions/service_inversion/busy_prefix.v b/analysis/definitions/service_inversion/busy_prefix.v
index 424e1f997972721d8f467172584e20ca0fe6cc06..21af507635eac1d7429e9513838cf02df6bd1f1e 100644
--- a/analysis/definitions/service_inversion/busy_prefix.v
+++ b/analysis/definitions/service_inversion/busy_prefix.v
@@ -2,7 +2,7 @@ Require Export prosa.model.priority.classes.
 Require Export prosa.analysis.facts.behavior.completion.
 Require Export prosa.analysis.definitions.service.
 Require Export prosa.analysis.definitions.service_inversion.pred.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 
 (** * Service Inversion Bounded *)
 (** In this section, we define the notion of bounded cumulative
diff --git a/analysis/definitions/workload/bounded.v b/analysis/definitions/workload/bounded.v
index 2ca86d5e8e2ee5d986b50e8af5c9971a3f20b98d..b8120624d489a1bf036138b76982064ab4ff70ca 100644
--- a/analysis/definitions/workload/bounded.v
+++ b/analysis/definitions/workload/bounded.v
@@ -1,5 +1,5 @@
 Require Export prosa.model.aggregate.workload.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 
 (** * Workload Bound in an Interval Starting with Quiet Time *)
 (** In this section, we define the notion of a bound on the total
diff --git a/analysis/facts/busy_interval/arrival.v b/analysis/facts/busy_interval/arrival.v
index 5214ede3ae3ddf85fdb58167125e323f9f38f4d8..8b7f466eed1654ee9e59469de0d6207c91132f2f 100644
--- a/analysis/facts/busy_interval/arrival.v
+++ b/analysis/facts/busy_interval/arrival.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 
 (** In this module we collect some basic facts about arrival times in busy
     windows. These are primarily useful for proof automation. *)
diff --git a/analysis/facts/busy_interval/quiet_time.v b/analysis/facts/busy_interval/quiet_time.v
index e0ae7fc0aa5d75d66ecfeb395f950c077ebcf150..0b3953d0c7b2ef91df7c4b9ebf95fdb4b71189c2 100644
--- a/analysis/facts/busy_interval/quiet_time.v
+++ b/analysis/facts/busy_interval/quiet_time.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 Require Export prosa.analysis.definitions.carry_in.
 
 (** In this module we collect some basic facts about quiet times. *)
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 15ac234bb9af835b8e383e3d9c0533d287bb396f..1c2f83691bf5f22d251b760e84487d2f635bfeba 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -4,7 +4,7 @@ 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 prosa.model.schedule.work_conserving.
-Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.classical.
 Require Export prosa.analysis.facts.blocking_bound.edf.
 
 (** * RTA for EDF  with Bounded Non-Preemptive Segments *)
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 2f67d52b2733ea81d85129a6d1205240bc1d4d37..5daa8659fd6a0e8d0ac978d90839f60a628b12aa 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,7 +1,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.busy_interval.classical.
 Require Export prosa.analysis.definitions.blocking_bound.fp.
 
 (** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)