diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 71e1e4c665d19f55f4a72f2c6d573bcf7cb23d11..e111ffeb1ec43a8ab9b000e742deb3a0595083b9 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.floating.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
+Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.facts.edf.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index b8e4da568d2fc3b6a8ebeee070a7ab63d0a414e1..08df29bc1a6e09c042c5ad93a531f096a50721e6 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.limited.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
+Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.facts.edf.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 65b36f528c46da306090b85ee2b9693914930c61..5449e5c8e16e58c6203e13338d93ee890d9e358d 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -19,7 +19,8 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreempti
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 
 (** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.preemption.nonpreemptive.
+Require Import rt.restructuring.model.schedule.nonpreemptive.
+Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index 1a398a87b08c7ada149c3a450bc2e678dbdc8929..c8d0f915754de3b1a53e726daf4364d7b47b7e3f 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -19,7 +19,7 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
 
 (** Assume we have a fully preemptive model. *)
-Require Import rt.restructuring.model.preemption.preemptive.
+Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index e48ce1209992ec2d030dface138e430db13d66a9..c84d38c4ecace597151659d7adbf252a2dce52aa 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.floating.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
+Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_driven.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index f93f2e8f2bb3806a96bc65290cf0cd4bd436f3bc..fcc437b33f5e8da7978c61c83dbc1b681b7553c9 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.limited.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
+Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_driven.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index e2387d28ef594e4d5422ff95a2741f13cbdb3c19..ec552eb4628fb931a01fa732b75775949d168b86 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -18,7 +18,9 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreempti
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 
 (** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.preemption.nonpreemptive.
+Require Import rt.restructuring.model.schedule.nonpreemptive.
+Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 607cf2a00c0479ec2b7577881ca52d95028e1ddc..f5ec02a06607af04b5b616d01b44524100dc5dab 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -18,7 +18,7 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
 
 (** Assume we have a fully preemptive model. *)
-Require Import rt.restructuring.model.preemption.preemptive.
+Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/model/preemption/floating.v b/restructuring/model/preemption/floating.v
deleted file mode 100644
index 4f8f8b04c27e06ed19ab8a427eab260a0aecda7c..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/floating.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Export rt.restructuring.model.preemption.valid_model.
-Require Export rt.restructuring.model.schedule.limited_preemptive.
-Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
diff --git a/restructuring/model/preemption/limited.v b/restructuring/model/preemption/limited.v
deleted file mode 100644
index a1f943c35ebc2cbd22fc34acb1f3f0c91346851b..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/limited.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Export rt.restructuring.model.preemption.valid_model.
-Require Export rt.restructuring.model.schedule.limited_preemptive.
-Require Export rt.restructuring.model.task.preemption.limited_preemptive.
-
diff --git a/restructuring/model/preemption/nonpreemptive.v b/restructuring/model/preemption/nonpreemptive.v
deleted file mode 100644
index e3b6368e74306422f43fa50db898b2ba20167963..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/nonpreemptive.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Require Export rt.restructuring.model.schedule.nonpreemptive.
-
-Require Export rt.restructuring.model.schedule.limited_preemptive.
-Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
-Require Export rt.restructuring.model.task.preemption.fully_nonpreemptive.
diff --git a/restructuring/model/preemption/preemptive.v b/restructuring/model/preemption/preemptive.v
deleted file mode 100644
index 3f5028e7e3e89d08b88f3b7de6eb69bee68aa4ed..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/preemptive.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Export rt.restructuring.model.schedule.limited_preemptive.
-Require Export rt.restructuring.model.preemption.job.instance.preemptive.
-Require Export rt.restructuring.model.task.preemption.fully_preemptive.