diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0100d960571cc378b46bb4256e5dccb477351a33..717fffe3a69da2599e7f656eda92d0d5940cf4bf 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -143,8 +143,8 @@ proof-state:
   dependencies:
     - 1.9.0-coq-8.10
   script:
-    - find restructuring util -iname *.v | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
-    - scripts/intersperse-proof-state.py `find restructuring util -iname *.v`
+    - find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
+    - scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
     - cd with-proof-state/
     - ln -s ../scripts/
     - ln -s ../_CoqProject
diff --git a/README.md b/README.md
index befa2f077d5984b02038ea7a61fe1965cc08e072..dc7427a9ad8a7fac494e7528ce522a8bdb9716b2 100644
--- a/README.md
+++ b/README.md
@@ -16,12 +16,21 @@ Please see the [list of publications](http://prosa.mpi-sws.org/documentation.htm
 
 ## Directory and Module Structure
 
-The directory and module structure is currently undergoing a fundamental reorganization. 
+The directory and module structure is organized as follows. First, the main parts, of which there are currently four.
+
+- [behavior/](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module. 
+- [model/](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate.
+- [analysis/](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
+- [results/](results/): The `results` namespace contains all **high-level analysis results**. 
+
+
+In future work, there will also (again) be an `implementation` or `examples` namespace in which important high-level results are instantiated (i.e., applied) in an assumption-free environment for concrete job and task types to establish the absence of any contradiction in assumptions.
+
+Furthermore, there are a couple of additional folders and namespaces.
 
 - [classic/](classic/): This module contains the "classic" version of Prosa as first presented at ECRTS'16.  
 All results published prior to 2020 build on this "classic" version of Prosa.
 - [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
-- [restructuring/](restructuring/): The new, refactored version of Prosa. Currently still under heavy development. This part of Prosa will soon move out of the `restructuring` namespace. 
 - [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
 
 ## Dependencies 
diff --git a/restructuring/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/abstract_rta.v
rename to analysis/abstract/abstract_rta.v
index 9351b305610369738498e6edad86070160b92533..446eff6eb9c82e71bbf02a9c470ce53c94f440c5 100644
--- a/restructuring/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Export rt.restructuring.analysis.abstract.search_space.
-Require Export rt.restructuring.analysis.abstract.run_to_completion.
+Require Export rt.analysis.concepts.schedulability.
+Require Export rt.analysis.abstract.search_space.
+Require Export rt.analysis.abstract.run_to_completion.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/abstract_seq_rta.v
rename to analysis/abstract/abstract_seq_rta.v
index 5946e2aca0577719a29077bb00bf9abf3204b681..bb09b5d2c8d88fbb655a8f38b89bd7a818ca11ac 100644
--- a/restructuring/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.definitions.task_schedule.
-Require Export rt.restructuring.analysis.facts.rbf.
-Require Export rt.restructuring.analysis.facts.behavior.task_arrivals.
-Require Export rt.restructuring.analysis.abstract.abstract_rta.
+Require Export rt.analysis.definitions.task_schedule.
+Require Export rt.analysis.facts.rbf.
+Require Export rt.analysis.facts.behavior.task_arrivals.
+Require Export rt.analysis.abstract.abstract_rta.
   
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
similarity index 99%
rename from restructuring/analysis/abstract/definitions.v
rename to analysis/abstract/definitions.v
index 3d3d5c05e1473b65a3f5abb0df284aa68b78d017..5bbb12e05a3e9b2fbc5eaeb1dc1188ace3ef1911 100644
--- a/restructuring/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.  
+Require Import rt.model.processor.ideal.  
 
 (** * Definitions for Abstract Response-Time Analysis *)
 (** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA) 
diff --git a/restructuring/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/ideal_jlfp_rta.v
rename to analysis/abstract/ideal_jlfp_rta.v
index 8b1d173e87e4bf01977d1bb0d8c57b7f4be7f2a4..153df7665eb84402a1b82732c5961d9ba803f740 100644
--- a/restructuring/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -1,13 +1,13 @@
-Require Export rt.restructuring.analysis.concepts.priority_inversion.
-Require Export rt.restructuring.analysis.abstract.abstract_seq_rta.
+Require Export rt.analysis.concepts.priority_inversion.
+Require Export rt.analysis.abstract.abstract_seq_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** In this file we consider an ideal uni-processor ... *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** ... and classic model of readiness without jitter and no
     self-suspensions, where pending jobs are always ready. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
 (** In this module we instantiate functions Interference and Interfering Workload 
diff --git a/restructuring/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
similarity index 98%
rename from restructuring/analysis/abstract/run_to_completion.v
rename to analysis/abstract/run_to_completion.v
index 53597c8e67bcc2f465afcf5c6b7ac2bb73402e67..e00ebe39bc2c660f00e90b27a936614c6b4400c6 100644
--- a/restructuring/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Export rt.restructuring.analysis.abstract.definitions.
+Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.analysis.abstract.definitions.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
similarity index 99%
rename from restructuring/analysis/abstract/search_space.v
rename to analysis/abstract/search_space.v
index f40ecc21a4f455a2eddf07768494574255d7d49f..8bc34c281eaeb8c4655fad5a787f530785b45911 100644
--- a/restructuring/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -1,6 +1,6 @@
 Require Import rt.util.epsilon.
 Require Import rt.util.tactics.
-Require Import rt.restructuring.model.task.concept.
+Require Import rt.model.task.concept.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Reduction of the search space for Abstract RTA *)
diff --git a/restructuring/analysis/concepts/busy_interval.v b/analysis/concepts/busy_interval.v
similarity index 95%
rename from restructuring/analysis/concepts/busy_interval.v
rename to analysis/concepts/busy_interval.v
index 84620629c520e0c470ab2c16ecea82a6b3387e79..5e613bdaf933b8a866285c4a6eaed0edbcfae124 100644
--- a/restructuring/analysis/concepts/busy_interval.v
+++ b/analysis/concepts/busy_interval.v
@@ -1,9 +1,9 @@
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.model.priority.classes.
+Require Export rt.analysis.facts.behavior.completion.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** * Busy Interval for JLFP-models *)
 (** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
diff --git a/restructuring/analysis/concepts/priority_inversion.v b/analysis/concepts/priority_inversion.v
similarity index 97%
rename from restructuring/analysis/concepts/priority_inversion.v
rename to analysis/concepts/priority_inversion.v
index a90e9f672bf17d38e4639974f89843c5171e5459..6278e97301b1d3c5db3a3ba1f98738827b5c8d27 100644
--- a/restructuring/analysis/concepts/priority_inversion.v
+++ b/analysis/concepts/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.concepts.busy_interval.
+Require Export rt.analysis.concepts.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/concepts/request_bound_function.v b/analysis/concepts/request_bound_function.v
similarity index 94%
rename from restructuring/analysis/concepts/request_bound_function.v
rename to analysis/concepts/request_bound_function.v
index 13aab3c1e015473a2ef22000b3c23ba8f3eadbe0..f531fa0fa221c6d61432edd36312e4d0cc20305b 100644
--- a/restructuring/analysis/concepts/request_bound_function.v
+++ b/analysis/concepts/request_bound_function.v
@@ -1,10 +1,10 @@
-Require Export rt.restructuring.model.task.arrival.curves.
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.task.arrival.curves.
+Require Export rt.model.priority.classes.
 
 (** The following definitions assume ideal uni-processor schedules.  This
     restriction exists for historic reasons; the defined concepts could be
     generalized in future work. *)
-Require Import rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Import rt.analysis.facts.behavior.ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/concepts/schedulability.v b/analysis/concepts/schedulability.v
similarity index 97%
rename from restructuring/analysis/concepts/schedulability.v
rename to analysis/concepts/schedulability.v
index 8ecedc8d006518ae90fd9304c8b2a963c8df0a24..4cffcb4f82d7924a66330e8c3697c3a9e915d89f 100644
--- a/restructuring/analysis/concepts/schedulability.v
+++ b/analysis/concepts/schedulability.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.behavior.completion.
-Require Import rt.restructuring.model.task.absolute_deadline.
+Require Export rt.analysis.facts.behavior.completion.
+Require Import rt.model.task.absolute_deadline.
 
 Section Task.
   Context {Task : TaskType}.
diff --git a/restructuring/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
similarity index 91%
rename from restructuring/analysis/definitions/carry_in.v
rename to analysis/definitions/carry_in.v
index ac0eee1afe00ebdbd149de9403d732fdde794284..55a3453c5ff0353b9d7f398fe9b243ea6b2d398f 100644
--- a/restructuring/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** * No Carry-In *)
 (** In this module we define the notion of no carry-in time for uni-processor schedulers. *)
diff --git a/restructuring/analysis/definitions/job_properties.v b/analysis/definitions/job_properties.v
similarity index 89%
rename from restructuring/analysis/definitions/job_properties.v
rename to analysis/definitions/job_properties.v
index 543f91039dc8e3e7aa67e4136b6dee5b5b9639ae..707ebee085f8944d254331c82df67a3882f5883b 100644
--- a/restructuring/analysis/definitions/job_properties.v
+++ b/analysis/definitions/job_properties.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 From mathcomp Require Export eqtype ssrnat.
 
 (** In this section, we introduce properties of a job. *)
diff --git a/restructuring/analysis/definitions/progress.v b/analysis/definitions/progress.v
similarity index 97%
rename from restructuring/analysis/definitions/progress.v
rename to analysis/definitions/progress.v
index de794d26c762f30ae767ce3a367654a4e4e6b9de..f36e412c266a24c88b613c3eeeb24488034a524c 100644
--- a/restructuring/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.analysis.facts.behavior.service.
 
 (** * Job Progress (or Lack Thereof) *)
 
diff --git a/restructuring/analysis/definitions/task_schedule.v b/analysis/definitions/task_schedule.v
similarity index 93%
rename from restructuring/analysis/definitions/task_schedule.v
rename to analysis/definitions/task_schedule.v
index a5ee28f9793dd8eafa7cf40a1bce419293a17802..19d851306b7a558c14a2632b429020688b1c521a 100644
--- a/restructuring/analysis/definitions/task_schedule.v
+++ b/analysis/definitions/task_schedule.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Export rt.model.task.concept.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/analysis/facts/behavior/all.v b/analysis/facts/behavior/all.v
new file mode 100644
index 0000000000000000000000000000000000000000..b5904f4ea533b602345870833dcc0027a82c0ff8
--- /dev/null
+++ b/analysis/facts/behavior/all.v
@@ -0,0 +1,8 @@
+Require Export rt.analysis.facts.behavior.service.
+Require Export rt.analysis.facts.behavior.service_of_jobs.
+Require Export rt.analysis.facts.behavior.completion.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
+Require Export rt.analysis.facts.behavior.sequential.
+Require Export rt.analysis.facts.behavior.arrivals.
+Require Export rt.analysis.facts.behavior.deadlines.
+Require Export rt.analysis.facts.behavior.workload.
diff --git a/restructuring/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
similarity index 99%
rename from restructuring/analysis/facts/behavior/arrivals.v
rename to analysis/facts/behavior/arrivals.v
index a9eb167ab5d8a9c5b2e68f5256628861275bc0e9..fbb7bf68f4c5d8707143a430d785d40b83c1778e 100644
--- a/restructuring/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 Require Export rt.util.all.
 
 (** In this section, we relate job readiness to [has_arrived]. *)
diff --git a/restructuring/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
similarity index 98%
rename from restructuring/analysis/facts/behavior/completion.v
rename to analysis/facts/behavior/completion.v
index d32bb55fb100e7eba08aa4ea46cdfedf0e6adc33..f9d9a6ce4a9888f263106070c9c1d45f10798433 100644
--- a/restructuring/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.behavior.service.
-Require Export rt.restructuring.analysis.facts.behavior.arrivals.
+Require Export rt.analysis.facts.behavior.service.
+Require Export rt.analysis.facts.behavior.arrivals.
 
 (** In this file, we establish basic facts about job completions. *)
 
diff --git a/restructuring/analysis/facts/behavior/deadlines.v b/analysis/facts/behavior/deadlines.v
similarity index 97%
rename from restructuring/analysis/facts/behavior/deadlines.v
rename to analysis/facts/behavior/deadlines.v
index 777c92c79cdf3e8de02a1053364b8fd390b0fe62..097c6d6a6c58b96a1cd583395679f2ad478b3574 100644
--- a/restructuring/analysis/facts/behavior/deadlines.v
+++ b/analysis/facts/behavior/deadlines.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.analysis.facts.behavior.completion.
 
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
diff --git a/restructuring/analysis/facts/behavior/ideal_schedule.v b/analysis/facts/behavior/ideal_schedule.v
similarity index 97%
rename from restructuring/analysis/facts/behavior/ideal_schedule.v
rename to analysis/facts/behavior/ideal_schedule.v
index ee7d8f7051eaa911508a19f1a63009e93e8e41b4..b1bdca2a45f55ad66c284fe9d69703cc16aa060f 100644
--- a/restructuring/analysis/facts/behavior/ideal_schedule.v
+++ b/analysis/facts/behavior/ideal_schedule.v
@@ -1,10 +1,10 @@
 From mathcomp Require Import all_ssreflect.
 Require Export rt.util.all.
-Require Export rt.restructuring.model.processor.platform_properties.
-Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.model.processor.platform_properties.
+Require Export rt.analysis.facts.behavior.service.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Note: we do not re-export the basic definitions to avoid littering the global
    namespace with type class instances. *)
diff --git a/restructuring/analysis/facts/behavior/sequential.v b/analysis/facts/behavior/sequential.v
similarity index 95%
rename from restructuring/analysis/facts/behavior/sequential.v
rename to analysis/facts/behavior/sequential.v
index 75efd68ab39c5172e1bdb7a765166456c618686b..7c115ca5648d84b199750b4d6a757257985948c3 100644
--- a/restructuring/analysis/facts/behavior/sequential.v
+++ b/analysis/facts/behavior/sequential.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.sequentiality.
+Require Export rt.model.task.sequentiality.
 
 Section ExecutionOrder.
   (** Consider any type of job associated with any type of tasks... *)
diff --git a/restructuring/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
similarity index 99%
rename from restructuring/analysis/facts/behavior/service.v
rename to analysis/facts/behavior/service.v
index 1d84947bcface00604bfdcb36a1c212b4ee45b59..c0852c0dfccfa05d0c28022de21a64c3a6d5bd45 100644
--- a/restructuring/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -1,6 +1,6 @@
 Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.processor.platform_properties.
+Require Export rt.behavior.all.
+Require Export rt.model.processor.platform_properties.
 
 From mathcomp Require Import ssrnat ssrbool fintype.
 
diff --git a/restructuring/analysis/facts/behavior/service_of_jobs.v b/analysis/facts/behavior/service_of_jobs.v
similarity index 97%
rename from restructuring/analysis/facts/behavior/service_of_jobs.v
rename to analysis/facts/behavior/service_of_jobs.v
index 5e3bfb7ab96ef4114744855d3b2b558eb27ab0d6..627a27770485ab0bf6b0a5c779f02678033671de 100644
--- a/restructuring/analysis/facts/behavior/service_of_jobs.v
+++ b/analysis/facts/behavior/service_of_jobs.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.aggregate.service_of_jobs.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
-Require Import rt.restructuring.model.processor.ideal.
+Require Export rt.model.aggregate.workload.
+Require Export rt.model.aggregate.service_of_jobs.
+Require Export rt.analysis.facts.behavior.completion.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
+Require Import rt.model.processor.ideal.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/behavior/task_arrivals.v b/analysis/facts/behavior/task_arrivals.v
similarity index 94%
rename from restructuring/analysis/facts/behavior/task_arrivals.v
rename to analysis/facts/behavior/task_arrivals.v
index 539c0c4de1f3c10c4cd41057a3a60d4dc27c96d1..96e695dc03d0c6b2920f70b3cf3b7781e5fa4a50 100644
--- a/restructuring/analysis/facts/behavior/task_arrivals.v
+++ b/analysis/facts/behavior/task_arrivals.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.arrivals.
+Require Export rt.model.task.arrivals.
 
 (** In this file we provide basic properties related to tasks on arrival sequences. *)
 Section TaskArrivals.
diff --git a/restructuring/analysis/facts/behavior/workload.v b/analysis/facts/behavior/workload.v
similarity index 90%
rename from restructuring/analysis/facts/behavior/workload.v
rename to analysis/facts/behavior/workload.v
index f8286ab2bdbd927eb7f4ff6271e68ccc96e76231..c7a352543952b161b799cb58c5aea7063eb3db52 100644
--- a/restructuring/analysis/facts/behavior/workload.v
+++ b/analysis/facts/behavior/workload.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.analysis.facts.behavior.arrivals.
+Require Export rt.model.aggregate.workload.
+Require Export rt.analysis.facts.behavior.arrivals.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/busy_interval.v b/analysis/facts/busy_interval.v
similarity index 98%
rename from restructuring/analysis/facts/busy_interval.v
rename to analysis/facts/busy_interval.v
index 9275bab698d5c2e4347340c44484a8169d0c7469..aeb1e61c5b303929d56bd9c4058db05a95d9a4f1 100644
--- a/restructuring/analysis/facts/busy_interval.v
+++ b/analysis/facts/busy_interval.v
@@ -1,14 +1,14 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.analysis.concepts.priority_inversion.
-Require Export rt.restructuring.analysis.facts.behavior.all.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.model.schedule.work_conserving.
+Require Export rt.analysis.concepts.priority_inversion.
+Require Export rt.analysis.facts.behavior.all.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** * Existence of Busy Interval for JLFP-models *)
 (** In this module we derive a sufficient condition for existence of
diff --git a/restructuring/analysis/facts/carry_in.v b/analysis/facts/carry_in.v
similarity index 98%
rename from restructuring/analysis/facts/carry_in.v
rename to analysis/facts/carry_in.v
index 35b0cb56c05136cab6a42edf5838efd1a738014b..e4832432f3f54f22c6d1932ff8b0303619d8a6a5 100644
--- a/restructuring/analysis/facts/carry_in.v
+++ b/analysis/facts/carry_in.v
@@ -1,12 +1,12 @@
-Require Export rt.restructuring.analysis.definitions.carry_in.
-Require Export rt.restructuring.analysis.facts.busy_interval.
+Require Export rt.analysis.definitions.carry_in.
+Require Export rt.analysis.facts.busy_interval.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** * Existence of No Carry-In Instant *)
 
diff --git a/restructuring/analysis/facts/edf.v b/analysis/facts/edf.v
similarity index 89%
rename from restructuring/analysis/facts/edf.v
rename to analysis/facts/edf.v
index 10cd3dc4c16d716afe190685a0a8283de2bcce8e..f85bd1a19bde485c9f20e7bb83659b3282164472 100644
--- a/restructuring/analysis/facts/edf.v
+++ b/analysis/facts/edf.v
@@ -1,5 +1,5 @@
-Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.task.absolute_deadline.
+Require Import rt.model.priority.edf.
+Require Import rt.model.task.absolute_deadline.
 
 (** In this section, we prove a few properties about EDF policy. *)
 Section PropertiesOfEDF.
diff --git a/restructuring/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
similarity index 97%
rename from restructuring/analysis/facts/preemption/job/limited.v
rename to analysis/facts/preemption/job/limited.v
index 4241860f010523c613cfebaefa37bb225eaa4df6..76cb3846ae85266827a8ddc2fa57b0d7b2eed67b 100644
--- a/restructuring/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.analysis.facts.behavior.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.schedule.limited_preemptive.
+Require Export rt.analysis.facts.behavior.all.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.model.schedule.limited_preemptive.
 
-Require Import rt.restructuring.model.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
similarity index 95%
rename from restructuring/analysis/facts/preemption/job/nonpreemptive.v
rename to analysis/facts/preemption/job/nonpreemptive.v
index 029b0a24d1bd082b36ed70e8003235f2000fe52a..2154889ffc95cb1ba5202d0481f04aa7b7d5d56e 100644
--- a/restructuring/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.analysis.facts.behavior.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.schedule.nonpreemptive.
+Require Export rt.analysis.facts.behavior.all.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.model.schedule.nonpreemptive.
 
-Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
+Require Import rt.model.preemption.fully_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
similarity index 93%
rename from restructuring/analysis/facts/preemption/job/preemptive.v
rename to analysis/facts/preemption/job/preemptive.v
index f2af28e1f4eff982ec6b35dd379be17c5d92f0ef..3d06928e6da8c1eeadc58d2d289aa9470b74df7a 100644
--- a/restructuring/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.fully_preemptive.
+Require Export rt.model.task.preemption.parameters.
+Require Import rt.model.preemption.fully_preemptive.
 
 (** * Preemptions in Fully Preemptive Model *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
similarity index 81%
rename from restructuring/analysis/facts/preemption/rtc_threshold/floating.v
rename to analysis/facts/preemption/rtc_threshold/floating.v
index e5be78e16c203c2bf2f10044af5f7e05ba9a2f28..e376c23e12514d2afa9bd0697e8648f0a6f65714 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -1,7 +1,7 @@
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Export rt.restructuring.analysis.facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
+Require Export rt.analysis.facts.preemption.task.floating.
+Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
similarity index 98%
rename from restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
rename to analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 03dd0428bb31662eeeef19a764a13d849b91ce42..9a4f1c349d91b5309bae9b742d13a8da2fb112da 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.facts.behavior.all.
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.facts.behavior.all.
+Require Export rt.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
 (** In this section, we provide a few basic properties 
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
similarity index 95%
rename from restructuring/analysis/facts/preemption/rtc_threshold/limited.v
rename to analysis/facts/preemption/rtc_threshold/limited.v
index 7819489405f2156db4d6da2a891eec46541e93c1..bab0d88aa96c9f4a5908da3cbed7a0294815b570 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.analysis.facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.analysis.facts.preemption.task.limited.
+Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
 
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
similarity index 92%
rename from restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
rename to analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index f1dcc2704b0d90fbdd7ece843cac31df915d8508..70aa48a161f428745462b84044ba1e4936447ccc 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
+Require Export rt.analysis.facts.preemption.job.nonpreemptive.
 
-Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
  
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
similarity index 85%
rename from restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
rename to analysis/facts/preemption/rtc_threshold/preemptive.v
index e2e9b6a0aa504603592f7db4295862d5f23d3c93..e92b555605297d10c99938160327c21d70290789 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -1,6 +1,6 @@
-Require Import rt.restructuring.model.preemption.fully_preemptive.
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
-Require Import rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Import rt.model.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
+Require Import rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
similarity index 96%
rename from restructuring/analysis/facts/preemption/task/floating.v
rename to analysis/facts/preemption/task/floating.v
index e76c730488f018fd7c48e6efe9a2827f28fd4879..28fa124791c789465c62c84fd325a43444aa15af 100644
--- a/restructuring/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.limited.
+Require Export rt.analysis.facts.preemption.job.limited.
 
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
similarity index 96%
rename from restructuring/analysis/facts/preemption/task/limited.v
rename to analysis/facts/preemption/task/limited.v
index 88ba4d0de81a9c1b8fa6d6e323e0f573e61c273c..a62f17823a886a3f041a039176239edc9f7fd701 100644
--- a/restructuring/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.limited.
+Require Export rt.analysis.facts.preemption.job.limited.
 
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
similarity index 94%
rename from restructuring/analysis/facts/preemption/task/nonpreemptive.v
rename to analysis/facts/preemption/task/nonpreemptive.v
index 62786996dda7b744e447da67533b31b48c25a88e..8e3d584c4d9ea62e56eb731b56657a1a7b0625fb 100644
--- a/restructuring/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
+Require Export rt.analysis.facts.preemption.job.nonpreemptive.
 
-Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
similarity index 91%
rename from restructuring/analysis/facts/preemption/task/preemptive.v
rename to analysis/facts/preemption/task/preemptive.v
index 8b17d3c66c94259de20e4c60b2d369de7781890a..4c95a45a741d3894655c17331591421ddb8b6364 100644
--- a/restructuring/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.facts.preemption.job.preemptive.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.facts.preemption.job.preemptive.
 
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
 
 (** * Platform for Fully Preemptive Model *)
 (** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/facts/priority_inversion.v b/analysis/facts/priority_inversion.v
similarity index 98%
rename from restructuring/analysis/facts/priority_inversion.v
rename to analysis/facts/priority_inversion.v
index 1e1eb9c93069dd1ca474157c5b2dfbdbab3b9acf..ca247335f8cae94bf719b47247a98e8a31f2090e 100644
--- a/restructuring/analysis/facts/priority_inversion.v
+++ b/analysis/facts/priority_inversion.v
@@ -1,19 +1,19 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.concepts.busy_interval.
-Require Export rt.restructuring.analysis.facts.busy_interval.
+Require Export rt.model.task.preemption.parameters.
+Require Export rt.model.schedule.priority_driven.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
+Require Export rt.model.schedule.work_conserving.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.concepts.busy_interval.
+Require Export rt.analysis.facts.busy_interval.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout the file we assume for the classic Liu & Layland model
     of readiness without jitter and no self-suspensions, where
     pending jobs are always ready. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** In preparation of the derivation of the priority inversion bound, we
     establish two basic facts on preemption times. *)
diff --git a/restructuring/analysis/facts/rbf.v b/analysis/facts/rbf.v
similarity index 98%
rename from restructuring/analysis/facts/rbf.v
rename to analysis/facts/rbf.v
index 5cdc4ffbcd564b64c82c6ad55feca86c01e6561f..af0888348edd41467dc8d62b67f3e01512fed4aa 100644
--- a/restructuring/analysis/facts/rbf.v
+++ b/analysis/facts/rbf.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.facts.behavior.workload.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.concepts.request_bound_function.
+Require Export rt.analysis.facts.behavior.workload.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.concepts.request_bound_function.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
similarity index 90%
rename from restructuring/analysis/facts/readiness/basic.v
rename to analysis/facts/readiness/basic.v
index a58055a1853de74d40930747a37f9a4480f1d717..df77d613dfd58232a7d2956bc29cbe2ce0063bd5 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -1,7 +1,7 @@
-Require Import rt.restructuring.analysis.facts.behavior.completion.
+Require Import rt.analysis.facts.behavior.completion.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 Section LiuAndLaylandReadiness.
   (** Consider any kind of jobs... *)
diff --git a/restructuring/analysis/facts/tdma.v b/analysis/facts/tdma.v
similarity index 99%
rename from restructuring/analysis/facts/tdma.v
rename to analysis/facts/tdma.v
index c951933016d74a9111b69c72985de77e91f46de4..830e1258e134427b21d593e1bfef2b0560bf69f4 100644
--- a/restructuring/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.tdma.
+Require Export rt.model.schedule.tdma.
 Require Import rt.util.all.
 From mathcomp Require Import div.
 
diff --git a/restructuring/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
similarity index 98%
rename from restructuring/analysis/facts/transform/edf_opt.v
rename to analysis/facts/transform/edf_opt.v
index 993ac77899724362fc09b4cd7e88d867c38d470a..11f79849800514e240d4dfeb69298d71d5dd58e7 100644
--- a/restructuring/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -1,9 +1,9 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.model.schedule.edf.
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Export rt.restructuring.analysis.transform.edf_trans.
-Require Export rt.restructuring.analysis.facts.transform.swaps.
-Require Export rt.restructuring.analysis.facts.readiness.basic.
+Require Export rt.model.schedule.edf.
+Require Export rt.analysis.concepts.schedulability.
+Require Export rt.analysis.transform.edf_trans.
+Require Export rt.analysis.facts.transform.swaps.
+Require Export rt.analysis.facts.readiness.basic.
 
 (** This file contains the main argument of the EDF optimality proof,
     starting with an analysis of the individual functions that drive
@@ -12,9 +12,9 @@ Require Export rt.restructuring.analysis.facts.readiness.basic.
     the obtained EDF schedule. *)
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** We start by analyzing the helper function [find_swap_candidate],
     which is a problem-specific wrapper around [search_arg]. *)
diff --git a/restructuring/analysis/facts/transform/replace_at.v b/analysis/facts/transform/replace_at.v
similarity index 96%
rename from restructuring/analysis/facts/transform/replace_at.v
rename to analysis/facts/transform/replace_at.v
index 29a4d88050ebb0be804c9559e4505cfb33c0d915..a1cc634a68c50cfaa4c10984e85da6fb5975161b 100644
--- a/restructuring/analysis/facts/transform/replace_at.v
+++ b/analysis/facts/transform/replace_at.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.transform.swap.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.analysis.transform.swap.
+Require Export rt.analysis.facts.behavior.completion.
 
 (** In this file, we make a few simple observations about schedules with
     replacements. *)
diff --git a/restructuring/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
similarity index 99%
rename from restructuring/analysis/facts/transform/swaps.v
rename to analysis/facts/transform/swaps.v
index 1b27adf6be892fa49e3e36f5a6f9a9a35c21d71e..8ed2b4160ab03751c2f11c777a80fdaf12eebc1b 100644
--- a/restructuring/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.transform.replace_at.
-Require Export rt.restructuring.analysis.facts.behavior.deadlines.
+Require Export rt.analysis.facts.transform.replace_at.
+Require Export rt.analysis.facts.behavior.deadlines.
 
 (** In this file, we establish invariants about schedules in which two
     allocations have been swapped, as for instance it is done in the
diff --git a/restructuring/analysis/transform/edf_trans.v b/analysis/transform/edf_trans.v
similarity index 96%
rename from restructuring/analysis/transform/edf_trans.v
rename to analysis/transform/edf_trans.v
index 1fd663234a6ba0ca211e11f772be2624f942fe4b..cf96a65066b95f06003aaf9965f46b7943e4295c 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/analysis/transform/edf_trans.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.transform.prefix.
-Require Export rt.restructuring.analysis.transform.swap.
+Require Export rt.analysis.transform.prefix.
+Require Export rt.analysis.transform.swap.
 
 (** In this file we define the EDF transformation of a schedule, which turns a
     (finite prefix of a) schedule into an EDF schedule. This operation is at
diff --git a/restructuring/analysis/transform/prefix.v b/analysis/transform/prefix.v
similarity index 98%
rename from restructuring/analysis/transform/prefix.v
rename to analysis/transform/prefix.v
index 90e5ee75d71704bed5db777a99bc0b3bc3f52c2c..feb1602893774867c8d019de1968602512decadd 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.analysis.facts.behavior.all.
+Require Export rt.analysis.facts.behavior.all.
 
 (** This file provides an operation that transforms a finite prefix of
     a given schedule by applying a point-wise transformation to each
diff --git a/restructuring/analysis/transform/swap.v b/analysis/transform/swap.v
similarity index 97%
rename from restructuring/analysis/transform/swap.v
rename to analysis/transform/swap.v
index 443aa3987a10bb41c3f1b2942449be7278ca86b1..eec37bca12a7bafdaa57d54319cd12e275f647bb 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/analysis/transform/swap.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** This file defines simple allocation substitutions and a swapping operation
     as used for instance in the classic EDF optimality proof. *)
diff --git a/restructuring/behavior/README.md b/behavior/README.md
similarity index 100%
rename from restructuring/behavior/README.md
rename to behavior/README.md
diff --git a/behavior/all.v b/behavior/all.v
new file mode 100644
index 0000000000000000000000000000000000000000..a2c66f74bc5809ab98913416415040f2acb66046
--- /dev/null
+++ b/behavior/all.v
@@ -0,0 +1,6 @@
+Require Export rt.behavior.time.
+Require Export rt.behavior.job.
+Require Export rt.behavior.arrival_sequence.
+Require Export rt.behavior.schedule.
+Require Export rt.behavior.service.
+Require Export rt.behavior.ready.
diff --git a/restructuring/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
similarity index 98%
rename from restructuring/behavior/arrival_sequence.v
rename to behavior/arrival_sequence.v
index 564c6f4e1832757e6cb8881e3177363a572efe78..bcc8dfa50b0ba83e83b4beec738293b2110063a2 100644
--- a/restructuring/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
-Require Export rt.restructuring.behavior.job.
+Require Export rt.behavior.job.
 Require Export rt.util.notation.
 
 (** This module contains basic definitions and properties of job arrival
diff --git a/restructuring/behavior/job.v b/behavior/job.v
similarity index 94%
rename from restructuring/behavior/job.v
rename to behavior/job.v
index df1d078512666d3b05fb9330f609dc5d2b11100d..6d10d08d9b26f86988edf2558d0d9c9a15497fb9 100644
--- a/restructuring/behavior/job.v
+++ b/behavior/job.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.time.
+Require Export rt.behavior.time.
 From mathcomp Require Export eqtype ssrnat.
 
 (** * Notion of a Job Type *)
diff --git a/restructuring/behavior/ready.v b/behavior/ready.v
similarity index 98%
rename from restructuring/behavior/ready.v
rename to behavior/ready.v
index 90361a6626fe85a9740682d2b6b30d7a7510fc87..fac5542f6009c58bc88714d38fc2bdfaa3220538 100644
--- a/restructuring/behavior/ready.v
+++ b/behavior/ready.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.service.
+Require Export rt.behavior.service.
 
 (** * Readiness of a Job *)
 
diff --git a/restructuring/behavior/schedule.v b/behavior/schedule.v
similarity index 98%
rename from restructuring/behavior/schedule.v
rename to behavior/schedule.v
index cba3f33ebff15997f2cbd2a1e61f39b1f104ca13..25009b4189c087553661a7bac23277ed43bb4de7 100644
--- a/restructuring/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.arrival_sequence.
+Require Export rt.behavior.arrival_sequence.
 
 (** * Generic Processor State *)
 
diff --git a/restructuring/behavior/service.v b/behavior/service.v
similarity index 98%
rename from restructuring/behavior/service.v
rename to behavior/service.v
index 6223722de9b7fa04a5599bf4b6299cde9018d5ec..0cbb438a5f8fd8df42f0d419e18a3329ad157e08 100644
--- a/restructuring/behavior/service.v
+++ b/behavior/service.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.schedule.
+Require Export rt.behavior.schedule.
 
 Section Service.
 
diff --git a/restructuring/behavior/time.v b/behavior/time.v
similarity index 100%
rename from restructuring/behavior/time.v
rename to behavior/time.v
diff --git a/create_makefile.sh b/create_makefile.sh
index 8a7176c66651a95e7d3d3c238a62ba187b28c35f..973076b38f4b2b6fa04a8e6bd393c89b7ba328f0 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -10,7 +10,7 @@ do
             FIND_OPTS+=( ! -path './classic/*' )
             ;;
         --only-classic)
-            FIND_OPTS+=( ! -path './restructuring/*' )
+            FIND_OPTS+=( ! -path './analysis/*' ! -path './behavior/*' ! -path './model/*'  ! -path './results/*')
             ;;
         *)
             echo "Unrecognized option: $1"
diff --git a/restructuring/model/README.md b/model/README.md
similarity index 100%
rename from restructuring/model/README.md
rename to model/README.md
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/model/aggregate/service_of_jobs.v
similarity index 98%
rename from restructuring/model/aggregate/service_of_jobs.v
rename to model/aggregate/service_of_jobs.v
index e6ed0146fb2bd28e9be41a125c887cf49cdcf440..908d2de04a8138152413fea3ce40cb4c36dd3dae 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/model/aggregate/service_of_jobs.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 
 (** * Service Received by Sets of Jobs *)
 
diff --git a/restructuring/model/aggregate/workload.v b/model/aggregate/workload.v
similarity index 97%
rename from restructuring/model/aggregate/workload.v
rename to model/aggregate/workload.v
index 8394feac8d95a5e2aa89bfbfd393bf7b7798495a..8054e7911f947ad05ff0bf8a096e3a8ca3074fb2 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/model/aggregate/workload.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 
 (** * Cumulative Workload of Sets of Jobs *)
 
diff --git a/restructuring/model/preemption/fully_nonpreemptive.v b/model/preemption/fully_nonpreemptive.v
similarity index 91%
rename from restructuring/model/preemption/fully_nonpreemptive.v
rename to model/preemption/fully_nonpreemptive.v
index 6915071ab9e6007f20f8f02276844132d46f5351..d70545dcb4cc50f488ac686ebbc80a4fdc4e466e 100644
--- a/restructuring/model/preemption/fully_nonpreemptive.v
+++ b/model/preemption/fully_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
 
 (** * Preemption Model: Fully Non-Preemptive Jobs *)
 (** In this section, we instantiate [job_preemptable] for the fully
diff --git a/restructuring/model/preemption/fully_preemptive.v b/model/preemption/fully_preemptive.v
similarity index 90%
rename from restructuring/model/preemption/fully_preemptive.v
rename to model/preemption/fully_preemptive.v
index d982b2dfa4861dcd20ceb149810f7b097f9ea28c..a02d2ae2458a8062bf9e3f60dd9cf7e49de89bea 100644
--- a/restructuring/model/preemption/fully_preemptive.v
+++ b/model/preemption/fully_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
 
 (** * Preemption Model: Fully Preemptive Jobs *)
 (** In this section, we instantiate [job_preemptable] for the fully preemptive
diff --git a/restructuring/model/preemption/limited_preemptive.v b/model/preemption/limited_preemptive.v
similarity index 97%
rename from restructuring/model/preemption/limited_preemptive.v
rename to model/preemption/limited_preemptive.v
index 98fdca850e35e9143a38205cec0095a1724dd0e7..105401d199e18a29a5346dfc25f377a1e7fb0c6a 100644
--- a/restructuring/model/preemption/limited_preemptive.v
+++ b/model/preemption/limited_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
 
 (** * Job Model Parameter for Preemption Points *)
 
diff --git a/restructuring/model/preemption/parameter.v b/model/preemption/parameter.v
similarity index 99%
rename from restructuring/model/preemption/parameter.v
rename to model/preemption/parameter.v
index 970d59dd088fdf3e6ac7fe565da234c42d68b045..ce601d51153da4573230c084e6b3d28e96edee55 100644
--- a/restructuring/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -1,5 +1,5 @@
 Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Job-Level Preemption Model *)
 (** There are many equivalent ways to represent at which points in time a job
diff --git a/restructuring/model/priority/classes.v b/model/priority/classes.v
similarity index 99%
rename from restructuring/model/priority/classes.v
rename to model/priority/classes.v
index ca8a406a343139f58539deac10f88cf1310a7c57..06fe6efad0e44c056ce9be62301af331788dd6bb 100644
--- a/restructuring/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 Require Export rt.util.rel.
 Require Export rt.util.list.
 
diff --git a/restructuring/model/priority/deadline_monotonic.v b/model/priority/deadline_monotonic.v
similarity index 95%
rename from restructuring/model/priority/deadline_monotonic.v
rename to model/priority/deadline_monotonic.v
index 6236df71720370b662ff52ca1bc9d2ef622eea58..0a25f5699ef5f9e00f10aeedd0a51fda84df6800 100644
--- a/restructuring/model/priority/deadline_monotonic.v
+++ b/model/priority/deadline_monotonic.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 
 (** * Deadline-Monotonic Fixed-Priority Policy *)
 
diff --git a/restructuring/model/priority/edf.v b/model/priority/edf.v
similarity index 95%
rename from restructuring/model/priority/edf.v
rename to model/priority/edf.v
index 6aaa625cdca54961e43167c23c48238a42836845..e0bfe8f3ca5294256fd3cad3eda0b6218fab795f 100644
--- a/restructuring/model/priority/edf.v
+++ b/model/priority/edf.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 
 (** * EDF Priority Policy *)
 
diff --git a/restructuring/model/priority/fifo.v b/model/priority/fifo.v
similarity index 95%
rename from restructuring/model/priority/fifo.v
rename to model/priority/fifo.v
index 67dfb099cee079b27b219254f928249ea70714e8..1c0a365681d324844e6840e363d51f733ee4fcfc 100644
--- a/restructuring/model/priority/fifo.v
+++ b/model/priority/fifo.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 
 (** * FIFO Priority Policy *)
 
diff --git a/restructuring/model/priority/numeric_fixed_priority.v b/model/priority/numeric_fixed_priority.v
similarity index 97%
rename from restructuring/model/priority/numeric_fixed_priority.v
rename to model/priority/numeric_fixed_priority.v
index c86717b6ff8094ba76fe7b82ea4d811ae33da585..bc5a698b356a9598c9f17d5a01c6f310996ef3e8 100644
--- a/restructuring/model/priority/numeric_fixed_priority.v
+++ b/model/priority/numeric_fixed_priority.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
 
 (** * Numeric Fixed Task Priorities *)
 
diff --git a/restructuring/model/priority/rate_monotonic.v b/model/priority/rate_monotonic.v
similarity index 92%
rename from restructuring/model/priority/rate_monotonic.v
rename to model/priority/rate_monotonic.v
index 7d17f266faad950f96e26cdf495b4124fdd225ca..bc38330462e5d023da18f2412e6a031ee8ad53c9 100644
--- a/restructuring/model/priority/rate_monotonic.v
+++ b/model/priority/rate_monotonic.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.task.arrival.sporadic.
+Require Export rt.model.priority.classes.
+Require Export rt.model.task.arrival.sporadic.
 
 
 (** * Rate-Monotonic Fixed-Priority Policy *)
diff --git a/restructuring/model/processor/ideal.v b/model/processor/ideal.v
similarity index 98%
rename from restructuring/model/processor/ideal.v
rename to model/processor/ideal.v
index 70ceea83cff06baf6cebeb18b5a39e8e7aa1c7cd..5f5b83bc5d6ffd1065bf7ab603dd74c8b334bc33 100644
--- a/restructuring/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * The Ideal Uniprocessor Model *)
 
diff --git a/restructuring/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
similarity index 98%
rename from restructuring/model/processor/multiprocessor.v
rename to model/processor/multiprocessor.v
index 9c13ebcaf1ddb59a2ab57a08a3e63de53d8ff3ba..ca02b538d034fbe98ffb6d4e8cfd76720f1de2e6 100644
--- a/restructuring/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export fintype.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Multiprocessor State *)
 
diff --git a/restructuring/model/processor/platform_properties.v b/model/processor/platform_properties.v
similarity index 96%
rename from restructuring/model/processor/platform_properties.v
rename to model/processor/platform_properties.v
index bf5e4825cf82f0c75e41b57781500b6adb17e149..cd2ad22738620659270ec55e44d13d45af761c09 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/model/processor/platform_properties.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** To reason about classes of schedule types / processor models, we define the
     following properties that group processor models into classes of similar
diff --git a/restructuring/model/processor/spin.v b/model/processor/spin.v
similarity index 97%
rename from restructuring/model/processor/spin.v
rename to model/processor/spin.v
index 42d23623a0d8621d9717ff94b92a2abe58a70596..5c1b708ed7fdf1fec2111607655e70c0cd8b0774 100644
--- a/restructuring/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** In the following, we define a processor state that includes the possibility
     of spinning, where spinning jobs do not progress (= don't get any service).
diff --git a/restructuring/model/processor/varspeed.v b/model/processor/varspeed.v
similarity index 97%
rename from restructuring/model/processor/varspeed.v
rename to model/processor/varspeed.v
index 4e9967b82b0a7ef0fee706f994871625222f69ed..e452f69f7255fcff2bf6beeef32f2dc9ab5bd481 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** In the following, we define a model of processors with variable execution
     speeds.
diff --git a/restructuring/model/readiness/basic.v b/model/readiness/basic.v
similarity index 94%
rename from restructuring/model/readiness/basic.v
rename to model/readiness/basic.v
index 5c94fd67f41174f98a870117fe5ac855a17e3e1e..271e6499c9663d64f8a70a0a3f5e3a787e1ed3f5 100644
--- a/restructuring/model/readiness/basic.v
+++ b/model/readiness/basic.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Liu & Layland Readiness Model *)
 
diff --git a/restructuring/model/readiness/jitter.v b/model/readiness/jitter.v
similarity index 97%
rename from restructuring/model/readiness/jitter.v
rename to model/readiness/jitter.v
index d7579df1e47fa0a8ff3c9f646bcde9c7e0bdede8..ab0b8b3b2593e8bbcb7d6728f3786ce7eefe4991 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 Require Import rt.util.nat.
 
diff --git a/restructuring/model/readiness/suspension.v b/model/readiness/suspension.v
similarity index 96%
rename from restructuring/model/readiness/suspension.v
rename to model/readiness/suspension.v
index b6c2e5214b01e830fa8727eb122a734c40bec8ca..5c9c5f2bc647cbd9f220e1a66fc9e3e83d8611f1 100644
--- a/restructuring/model/readiness/suspension.v
+++ b/model/readiness/suspension.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.definitions.progress.
+Require Export rt.behavior.all.
+Require Export rt.analysis.definitions.progress.
 Require Export rt.util.nat.
 
 (** * Job Model Parameter for Jobs Exhibiting Self-Suspensions *)
diff --git a/restructuring/model/schedule/edf.v b/model/schedule/edf.v
similarity index 98%
rename from restructuring/model/schedule/edf.v
rename to model/schedule/edf.v
index 4d05ba0b242208707f4183d64fb7c7996a3ff0df..cfe08f00734fa3ee1bf6ead3e00a75e4e3d71663 100644
--- a/restructuring/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Fully-Preemptive EDF Schedules *)
 
diff --git a/restructuring/model/schedule/limited_preemptive.v b/model/schedule/limited_preemptive.v
similarity index 94%
rename from restructuring/model/schedule/limited_preemptive.v
rename to model/schedule/limited_preemptive.v
index 3bf94581f6128f8641abb10f7c6e0fcd91796602..a9849974a482e6c9919bfd4a6740b58add0ba296 100644
--- a/restructuring/model/schedule/limited_preemptive.v
+++ b/model/schedule/limited_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter. 
+Require Export rt.model.preemption.parameter. 
 
 (** * Preemption Model Compliance *)
 
diff --git a/restructuring/model/schedule/nonpreemptive.v b/model/schedule/nonpreemptive.v
similarity index 95%
rename from restructuring/model/schedule/nonpreemptive.v
rename to model/schedule/nonpreemptive.v
index 05e1852f37e68a46e7315227512f504d1ec76bca..6bff4dd09c707e92ce69cea4e152dfcd3315241e 100644
--- a/restructuring/model/schedule/nonpreemptive.v
+++ b/model/schedule/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Nonpreemptive Schedules  *)
 
diff --git a/restructuring/model/schedule/preemption_time.v b/model/schedule/preemption_time.v
similarity index 93%
rename from restructuring/model/schedule/preemption_time.v
rename to model/schedule/preemption_time.v
index 8fb17776e73b0939b3c2bf957dec9359f168d0e7..97508bc0800dd13ab518f0c1b784b85c96dce19c 100644
--- a/restructuring/model/schedule/preemption_time.v
+++ b/model/schedule/preemption_time.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
 
 (** * Preemption Times *)
 
@@ -14,7 +14,7 @@ Require Export rt.restructuring.model.preemption.parameter.
     ideal uniprocessor schedules. Lifting this assumption is future work. *)
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
 
 Section PreemptionTime.
 
diff --git a/restructuring/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
similarity index 91%
rename from restructuring/model/schedule/priority_driven.v
rename to model/schedule/priority_driven.v
index 49845a6532385fa37140ffc6eadbaec4fd0ae7a0..b66607e4c8fbdb70ab00c4878b801b62b71fda26 100644
--- a/restructuring/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.schedule.preemption_time.
+Require Export rt.model.priority.classes.
+Require Export rt.model.schedule.preemption_time.
 
 (** * Priority-Driven Schedules *)
 
@@ -13,7 +13,7 @@ Require Export rt.restructuring.model.schedule.preemption_time.
         uniprocessor schedules. Removal of this limitation is future work. *)
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
 
 Section Priority.
 
diff --git a/restructuring/model/schedule/tdma.v b/model/schedule/tdma.v
similarity index 98%
rename from restructuring/model/schedule/tdma.v
rename to model/schedule/tdma.v
index 24ee5d5290ee851a7adb8ad85867489205e67d46..c86e0425dffce7445c1fd5ba6088b02caada672a 100644
--- a/restructuring/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -1,10 +1,10 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 Require Export rt.util.seqset.
 Require Export rt.util.rel.
 From mathcomp Require Import div.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
 
 (** * TDMA Scheduling *)
 
diff --git a/restructuring/model/schedule/work_conserving.v b/model/schedule/work_conserving.v
similarity index 97%
rename from restructuring/model/schedule/work_conserving.v
rename to model/schedule/work_conserving.v
index 6d72faff1acd80608593c8c93fa52c2d6bb71739..335dff6146243167758b92b225a4894a3ff163bf 100644
--- a/restructuring/model/schedule/work_conserving.v
+++ b/model/schedule/work_conserving.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Definition of Work Conservation *)
 
diff --git a/restructuring/model/task/absolute_deadline.v b/model/task/absolute_deadline.v
similarity index 89%
rename from restructuring/model/task/absolute_deadline.v
rename to model/task/absolute_deadline.v
index 86cc56f1026a49d776d069fb0479817956391c6d..f9be6873c190fa3c6f2ac920204821b40ddab7a5 100644
--- a/restructuring/model/task/absolute_deadline.v
+++ b/model/task/absolute_deadline.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 
 (** Given relative task deadlines and a mapping from jobs to tasks, we provide
     the canonical definition of each job's absolute deadline, i.e.,
diff --git a/restructuring/model/task/arrival/curves.v b/model/task/arrival/curves.v
similarity index 99%
rename from restructuring/model/task/arrival/curves.v
rename to model/task/arrival/curves.v
index 649d3a62a251e9b1763ac8b14598af84a240d6bf..20f196236f8f4dc4c5cd8defbe40332797c79b2f 100644
--- a/restructuring/model/task/arrival/curves.v
+++ b/model/task/arrival/curves.v
@@ -1,5 +1,5 @@
 Require Export rt.util.rel.
-Require Export rt.restructuring.model.task.arrivals.
+Require Export rt.model.task.arrivals.
 
 (** * The Arbitrary Arrival Curves Model *)
 
diff --git a/restructuring/model/task/arrival/sporadic.v b/model/task/arrival/sporadic.v
similarity index 98%
rename from restructuring/model/task/arrival/sporadic.v
rename to model/task/arrival/sporadic.v
index f2e7f53bcf3fd2297eee6bbf5a7e3b8a8a434c12..b154736e2a3b3ec033829ef24b9b2209d6da2fa8 100644
--- a/restructuring/model/task/arrival/sporadic.v
+++ b/model/task/arrival/sporadic.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 
 (** * The Sporadic Task Model *)
 
diff --git a/restructuring/model/task/arrivals.v b/model/task/arrivals.v
similarity index 95%
rename from restructuring/model/task/arrivals.v
rename to model/task/arrivals.v
index 540571a58a708b7a8087eff493d095051f327f39..5ba7bc383e6e40c1c8b2780fcc136e6730dff844 100644
--- a/restructuring/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 
 (** In this module, we provide basic definitions concerning the job
     arrivals of a given task. *)
diff --git a/restructuring/model/task/concept.v b/model/task/concept.v
similarity index 98%
rename from restructuring/model/task/concept.v
rename to model/task/concept.v
index db9044e79b4c16f4057bfe024a8f34443ffde411..c9cf3696017d19cdab69ef37d58f50d7e3a0316d 100644
--- a/restructuring/model/task/concept.v
+++ b/model/task/concept.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssrbool.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
 
 (** * Task Type *)
 
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/model/task/preemption/floating_nonpreemptive.v
similarity index 95%
rename from restructuring/model/task/preemption/floating_nonpreemptive.v
rename to model/task/preemption/floating_nonpreemptive.v
index bd65347eef097ab68cc70bd7f0df366f81b46e75..62d93a0d36ac8f093c1354354973a9780f045922 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/model/task/preemption/floating_nonpreemptive.v
@@ -1,5 +1,5 @@
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Import rt.model.preemption.limited_preemptive.
+Require Export rt.model.task.preemption.parameters.
 
 (** * Task Model with Floating Non-Preemptive Regions *)
 
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/model/task/preemption/fully_nonpreemptive.v
similarity index 95%
rename from restructuring/model/task/preemption/fully_nonpreemptive.v
rename to model/task/preemption/fully_nonpreemptive.v
index 707c2e990406349d0016a24c96ebf9b1d91169b3..9da4626ebc921c6b854c656e471883c93b47808e 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/model/task/preemption/fully_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.model.task.preemption.parameters.
 
 (** * Fully Non-Preemptive Task Model *)
 
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v
similarity index 95%
rename from restructuring/model/task/preemption/fully_preemptive.v
rename to model/task/preemption/fully_preemptive.v
index 6a4faa33a0156400d9ce04dc89bac1086fb34d50..7cff6fbba814f9e21b21da4c487367d6673648d7 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/model/task/preemption/fully_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.model.task.preemption.parameters.
 
 (** * Fully Preemptive Task Model *)
 
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/model/task/preemption/limited_preemptive.v
similarity index 97%
rename from restructuring/model/task/preemption/limited_preemptive.v
rename to model/task/preemption/limited_preemptive.v
index c91d4f2169863e85551024b5fc2a696dc643b6c6..685d09357520c71387d54f0f8deed1532201b138 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/model/task/preemption/limited_preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.limited_preemptive.
+Require Export rt.model.task.preemption.parameters.
+Require Import rt.model.preemption.limited_preemptive.
 
 (** * Limited-Preemptive Task Model *)
 
diff --git a/restructuring/model/task/preemption/parameters.v b/model/task/preemption/parameters.v
similarity index 98%
rename from restructuring/model/task/preemption/parameters.v
rename to model/task/preemption/parameters.v
index 151a838734118487ac896ce96a789127bca3f4a4..e5092055f7289e7ce6dcf28b6d8470becc1ca744 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/model/task/preemption/parameters.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.preemption.parameter.
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.preemption.parameter.
+Require Export rt.model.task.concept.
 
 (** * Task Preemption Model *)
 
diff --git a/restructuring/model/task/sequentiality.v b/model/task/sequentiality.v
similarity index 95%
rename from restructuring/model/task/sequentiality.v
rename to model/task/sequentiality.v
index 8afbffb46f3c4171adedc280cc2ee8ba8eadfdc2..b6819e4345e302cb9cd2641583714d3f921a6f3e 100644
--- a/restructuring/model/task/sequentiality.v
+++ b/model/task/sequentiality.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
 
 (** In this module, we give a precise definition of the common notion of
     "sequential tasks", which is commonly understood to mean that the jobs of a
diff --git a/restructuring/model/task/suspension/dynamic.v b/model/task/suspension/dynamic.v
similarity index 91%
rename from restructuring/model/task/suspension/dynamic.v
rename to model/task/suspension/dynamic.v
index 44d6c5a587963e506510950ab6426cec93cddc00..31e1dbfdae729ae0fcf71d5c9bf58b508cf3be19 100644
--- a/restructuring/model/task/suspension/dynamic.v
+++ b/model/task/suspension/dynamic.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.readiness.suspension.
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.readiness.suspension.
+Require Export rt.model.task.concept.
 
 (** * Task Parameter for the Dynamic Self-Suspension Model *)
 
diff --git a/restructuring/README.md b/restructuring/README.md
deleted file mode 100644
index 0d89a0d0f1664d5d20fb6270246330aec0ed8cd9..0000000000000000000000000000000000000000
--- a/restructuring/README.md
+++ /dev/null
@@ -1,17 +0,0 @@
-# Restructed Prosa
-
-This is a work-in-progress directory and part of the larger Prosa restructuring effort. As parts in Prosa are changed to comply with the “new style”, they are placed here. 
-
-The following discussion is going to move to the top-level README file when the `restructuring` prefix is dropped.
-
-## Structure 
-
-There are four main parts of Prosa. 
-
-The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module. 
-
-The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module may contain multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.) and higher-level results can pick-and-choose whatever definitions are appropriate.
-
-The `analysis` namespace collects all definitions and proofs of **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Most importantly, all high-level analysis results and virtually all proofs are located here. 
-
-In future work, there will also (again) be an `implementation` namespace in which important high-level results are instantiated (i.e., applied) in an assumption-free environment for concrete job and task types to establish the absence of any contradiction in assumptions.
diff --git a/restructuring/analysis/facts/behavior/all.v b/restructuring/analysis/facts/behavior/all.v
deleted file mode 100644
index dbd7016f99146b49c88cfe95ce6e9da2f92b37a7..0000000000000000000000000000000000000000
--- a/restructuring/analysis/facts/behavior/all.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Export rt.restructuring.analysis.facts.behavior.service.
-Require Export rt.restructuring.analysis.facts.behavior.service_of_jobs.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
-Require Export rt.restructuring.analysis.facts.behavior.sequential.
-Require Export rt.restructuring.analysis.facts.behavior.arrivals.
-Require Export rt.restructuring.analysis.facts.behavior.deadlines.
-Require Export rt.restructuring.analysis.facts.behavior.workload.
diff --git a/restructuring/behavior/all.v b/restructuring/behavior/all.v
deleted file mode 100644
index f12642cbe3dadf6371e8d36be6bcae1112fd7d7d..0000000000000000000000000000000000000000
--- a/restructuring/behavior/all.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Require Export rt.restructuring.behavior.time.
-Require Export rt.restructuring.behavior.job.
-Require Export rt.restructuring.behavior.arrival_sequence.
-Require Export rt.restructuring.behavior.schedule.
-Require Export rt.restructuring.behavior.service.
-Require Export rt.restructuring.behavior.ready.
diff --git a/restructuring/results/edf/optimality.v b/results/edf/optimality.v
similarity index 95%
rename from restructuring/results/edf/optimality.v
rename to results/edf/optimality.v
index 44e7f6836c5680ab6a315f6a1c0e4aee987c0b1a..8158da0725deb4cac30d50146139aac28551506e 100644
--- a/restructuring/results/edf/optimality.v
+++ b/results/edf/optimality.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.facts.transform.edf_opt.
+Require Export rt.analysis.facts.transform.edf_opt.
 
 (** This file contains the theorem that states the famous EDF
     optimality result: if there is any way to meet all deadlines
@@ -6,10 +6,10 @@ Require Export rt.restructuring.analysis.facts.transform.edf_opt.
     schedule in which all deadlines are met. *)
 
 (** The following results assume ideal uniprocessor schedules... *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
 (** ... and the basic (i.e., Liu & Layland) readiness model under which any
     pending job is ready. *)
-Require rt.restructuring.model.readiness.basic.
+Require rt.model.readiness.basic.
 
 Section Optimality.
   (** For any given type of jobs... *)
diff --git a/restructuring/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
similarity index 97%
rename from restructuring/results/edf/rta/bounded_nps.v
rename to results/edf/rta/bounded_nps.v
index 96e0dd951c8223172ab1dbb02d5bcca07c43918e..85cf2103e744280a22a466adf535c348d42fe80e 100644
--- a/restructuring/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -1,14 +1,14 @@
-Require Export rt.restructuring.analysis.facts.priority_inversion.
-Require Export rt.restructuring.results.edf.rta.bounded_pi.
-Require Export rt.restructuring.analysis.facts.rbf.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.analysis.facts.priority_inversion.
+Require Export rt.results.edf.rta.bounded_pi.
+Require Export rt.analysis.facts.rbf.
+Require Import rt.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** * RTA for EDF-schedulers with Bounded Non-Preemptive Segments *)
 
diff --git a/restructuring/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
similarity index 98%
rename from restructuring/results/edf/rta/bounded_pi.v
rename to results/edf/rta/bounded_pi.v
index f8cbcdcaeb2aec64893bf942f6d2ed9f75633823..dc900393d2d4fad092b48e6cac5e7ac77c86e533 100644
--- a/restructuring/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,18 +1,18 @@
-Require Export rt.restructuring.analysis.facts.edf.
-Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.priority_inversion.
-Require Export rt.restructuring.analysis.facts.carry_in.
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.task.absolute_deadline.
-Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
+Require Export rt.analysis.facts.edf.
+Require Export rt.model.schedule.priority_driven.
+Require Export rt.analysis.facts.priority_inversion.
+Require Export rt.analysis.facts.carry_in.
+Require Export rt.analysis.concepts.schedulability.
+Require Import rt.model.priority.edf.
+Require Import rt.model.task.absolute_deadline.
+Require Import rt.analysis.abstract.ideal_jlfp_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 
 (** * Abstract RTA for EDF-schedulers with Bounded Priority Inversion *)
diff --git a/restructuring/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
similarity index 93%
rename from restructuring/results/edf/rta/floating_nonpreemptive.v
rename to results/edf/rta/floating_nonpreemptive.v
index a7f1ebd9468b4bff56f5b52ad2bc8cce994d8a14..51949915ce9042d15a0036ab2fdee669b486a842 100644
--- a/restructuring/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -1,17 +1,17 @@
-Require Export rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.floating.
+Require Import rt.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the task model with floating non-preemptive regions. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
 
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
diff --git a/restructuring/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
similarity index 93%
rename from restructuring/results/edf/rta/fully_nonpreemptive.v
rename to results/edf/rta/fully_nonpreemptive.v
index bd170fec07bcf72c5763a72208c1636dae08599a..4d83117649e35a368115f5ed7f0e0a9dd2b3c091 100644
--- a/restructuring/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -1,17 +1,17 @@
-Require Export rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.nonpreemptive.
+Require Import rt.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the fully non-preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
 
 (** * RTA for Fully Non-Preemptive FP Model *)
 (** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
diff --git a/restructuring/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
similarity index 93%
rename from restructuring/results/edf/rta/fully_preemptive.v
rename to results/edf/rta/fully_preemptive.v
index ad7f4121a085882e4609513d9dacf25d41f2de33..2a875b431d8c6abfeb97b39aeed7b45d92593d88 100644
--- a/restructuring/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -1,17 +1,17 @@
-Require Import rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
-Require Import rt.restructuring.model.priority.edf.
+Require Import rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.preemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.preemptive.
+Require Import rt.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the fully preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
 
 (** * RTA for Fully Preemptive EDF Model *)
 (** In this section we prove the RTA theorem for the fully preemptive EDF model *)
diff --git a/restructuring/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
similarity index 94%
rename from restructuring/results/edf/rta/limited_preemptive.v
rename to results/edf/rta/limited_preemptive.v
index 133b828e2d2bc9ff2cb6b9283b41b92f3dcc58c3..eccb3e98c0b9cf9e46a701bf2a42e7e291a6f246 100644
--- a/restructuring/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -1,17 +1,17 @@
-Require Export rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.limited.
+Require Import rt.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the task model with fixed preemption points. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
 
 (** * RTA for EDF-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points. *)
diff --git a/restructuring/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
similarity index 96%
rename from restructuring/results/fixed_priority/rta/bounded_nps.v
rename to results/fixed_priority/rta/bounded_nps.v
index 58e4da3ee2b6de0c03ea3b97c9362d9df6665494..418d5f35c0621696fee5599c2ea1d9544925211f 100644
--- a/restructuring/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,14 +1,14 @@
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Export rt.restructuring.analysis.concepts.request_bound_function.
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_pi.
-Require Export rt.restructuring.analysis.facts.priority_inversion.
+Require Export rt.analysis.concepts.schedulability.
+Require Export rt.analysis.concepts.request_bound_function.
+Require Export rt.results.fixed_priority.rta.bounded_pi.
+Require Export rt.analysis.facts.priority_inversion.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
 
diff --git a/restructuring/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
similarity index 98%
rename from restructuring/results/fixed_priority/rta/bounded_pi.v
rename to results/fixed_priority/rta/bounded_pi.v
index 184a7948633eb7834a061b6154fca14445f56161..5546a98a658455fa4bc76766327ae0467813bb14 100644
--- a/restructuring/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -1,13 +1,13 @@
-Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.busy_interval.
-Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
+Require Export rt.model.schedule.priority_driven.
+Require Export rt.analysis.facts.busy_interval.
+Require Import rt.analysis.abstract.ideal_jlfp_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
 (** In this module we instantiate the Abstract Response-Time analysis
diff --git a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
similarity index 93%
rename from restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
rename to results/fixed_priority/rta/floating_nonpreemptive.v
index 4bb73c0f0900e1fe1b0f6ae5ad2d8a4cb8cd9653..1094dbe7887d0cd085c72619ba667c995f1c7bb9 100644
--- a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.floating.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the task model with floating non-preemptive regions. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
 
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating
diff --git a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
similarity index 93%
rename from restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
rename to results/fixed_priority/rta/fully_nonpreemptive.v
index 0cf5969b488f0dca2f585fedbd38b8930ca61d3f..e1eb3fcd3f70c7105188393d5a0bb32365771bf3 100644
--- a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the fully non-preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
 
 (** * RTA for Fully Non-Preemptive FP Model *)
 (** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
diff --git a/restructuring/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
similarity index 92%
rename from restructuring/results/fixed_priority/rta/fully_preemptive.v
rename to results/fixed_priority/rta/fully_preemptive.v
index 9195c46eeaf81cf274c634039219e607d74e7341..c216f3d5699de9f3ba873abcc24f8a8dd8082749 100644
--- a/restructuring/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.preemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.preemptive.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the fully preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
 
 (** * RTA for Fully Preemptive FP Model *)
 (** In this module we prove the RTA theorem for fully preemptive FP model. *)
diff --git a/restructuring/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
similarity index 94%
rename from restructuring/results/fixed_priority/rta/limited_preemptive.v
rename to results/fixed_priority/rta/limited_preemptive.v
index 19fa54b29cbf2cdccfa223a3294b6be1d92cfa87..360c097b5d19ec8f2af2f088b307fc7ff7fd0ab9 100644
--- a/restructuring/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.limited.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
 
 (** Throughout this file, we assume the task model with fixed preemption points. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
 
 
 (** * RTA for FP-schedulers with Fixed Preemption Points *)