diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 8eeb79e924ac3b30bcf4b6a7a271db075e2528e9..06c0c2428c916294ccbb1c632c372c19b6bd81c7 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.concepts.schedulability.
+Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.abstract.search_space.
 Require Export prosa.analysis.abstract.run_to_completion.
 
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index 1a4959e1a0041b93c44de4ac93fe1277fb38384d..53b778c382e815fb4af7884917bfeb3a107fe29d 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.concepts.priority_inversion.
+Require Export prosa.analysis.definitions.priority_inversion.
 Require Export prosa.analysis.abstract.abstract_seq_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/analysis/concepts/busy_interval.v b/analysis/definitions/busy_interval.v
similarity index 100%
rename from analysis/concepts/busy_interval.v
rename to analysis/definitions/busy_interval.v
diff --git a/analysis/concepts/priority_inversion.v b/analysis/definitions/priority_inversion.v
similarity index 98%
rename from analysis/concepts/priority_inversion.v
rename to analysis/definitions/priority_inversion.v
index d2397db2085b23c379e24841a7f79778e9a93e59..21d93352591f2d32822b488ff7404b2764fae844 100644
--- a/analysis/concepts/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.concepts.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/analysis/concepts/request_bound_function.v b/analysis/definitions/request_bound_function.v
similarity index 100%
rename from analysis/concepts/request_bound_function.v
rename to analysis/definitions/request_bound_function.v
diff --git a/analysis/concepts/schedulability.v b/analysis/definitions/schedulability.v
similarity index 100%
rename from analysis/concepts/schedulability.v
rename to analysis/definitions/schedulability.v
diff --git a/analysis/facts/busy_interval.v b/analysis/facts/busy_interval.v
index 4dfb29e9a2d24214782e24ae54aea8256a4cf384..ef2bbbd873757b70e586cb34642679f020abef9f 100644
--- a/analysis/facts/busy_interval.v
+++ b/analysis/facts/busy_interval.v
@@ -1,6 +1,6 @@
 Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.model.schedule.work_conserving.
-Require Export prosa.analysis.concepts.priority_inversion.
+Require Export prosa.analysis.definitions.priority_inversion.
 Require Export prosa.analysis.facts.behavior.all.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/analysis/facts/priority_inversion.v b/analysis/facts/priority_inversion.v
index 84820dd4242bf0737312d43f16d7dbf44a89e8bc..fa62b565c74942bf73f6d7914c67a24a728f1527 100644
--- a/analysis/facts/priority_inversion.v
+++ b/analysis/facts/priority_inversion.v
@@ -3,7 +3,7 @@ Require Export prosa.model.schedule.priority_driven.
 Require Export prosa.analysis.facts.behavior.ideal_schedule.
 Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.definitions.job_properties.
-Require Export prosa.analysis.concepts.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.
 Require Export prosa.analysis.facts.busy_interval.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/analysis/facts/rbf.v b/analysis/facts/rbf.v
index 376dcf44b5f583d2a3da90ebd97a1f0a9b3f35a8..27fa1e790cd95055182f07da66a3ff69618f91c1 100644
--- a/analysis/facts/rbf.v
+++ b/analysis/facts/rbf.v
@@ -1,6 +1,6 @@
 Require Export prosa.analysis.facts.behavior.workload.
 Require Export prosa.analysis.definitions.job_properties.
-Require Export prosa.analysis.concepts.request_bound_function.
+Require Export prosa.analysis.definitions.request_bound_function.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index 0ce47a1350ccdd4c6dc0d42cd26f043fa0c1c0a6..56d6e1247ec7362ceb499fb237801f828189bc96 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -1,6 +1,6 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
 Require Export prosa.model.schedule.edf.
-Require Export prosa.analysis.concepts.schedulability.
+Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.transform.edf_trans.
 Require Export prosa.analysis.facts.transform.swaps.
 Require Export prosa.analysis.facts.readiness.basic.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index d7295099c09b49d0bd3a13dd2aacf17e011811b9..55a3ae8db5d61b0e019633e8963298b4c195afce 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -2,7 +2,7 @@ Require Export prosa.analysis.facts.edf.
 Require Export prosa.model.schedule.priority_driven.
 Require Export prosa.analysis.facts.priority_inversion.
 Require Export prosa.analysis.facts.carry_in.
-Require Export prosa.analysis.concepts.schedulability.
+Require Export prosa.analysis.definitions.schedulability.
 Require Import prosa.model.priority.edf.
 Require Import prosa.model.task.absolute_deadline.
 Require Import prosa.analysis.abstract.ideal_jlfp_rta.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index bb195bafe085610db229dd7158a757e0fe8bfb75..51b583a3aec27318bdc7b7ce2010efe1c5755a30 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,5 +1,5 @@
-Require Export prosa.analysis.concepts.schedulability.
-Require Export prosa.analysis.concepts.request_bound_function.
+Require Export prosa.analysis.definitions.schedulability.
+Require Export prosa.analysis.definitions.request_bound_function.
 Require Export prosa.results.fixed_priority.rta.bounded_pi.
 Require Export prosa.analysis.facts.priority_inversion.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.