diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 41f1276cfa62e8bc18bc7d957241c2129a399007..4a4e11d947ce546aec12618cbb97f2778ebc7bcb 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.valid_schedule.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 548a8b37559a3d972ac726dcb980b5829f07a745..4a4f9f54aead398294041a7a5c6fbc44d5a6f6f7 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.behavior.schedule.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
-Require Import rt.restructuring.model.preemption.valid_schedule.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 32cb214d30c39ed13e174d95dbd6684d044bab91..9a918e50acfdaf25ee0c0a0f6a6af39546760aef 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
-Require Import rt.restructuring.model.preemption.valid_schedule.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 58c4e7fc0a7013350e90702c4b35da2c86e8a362..e51e4269d0ef4e4714d488d2fb2661f22a85b9b2 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.valid_schedule.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
diff --git a/restructuring/model/preemption/floating.v b/restructuring/model/preemption/floating.v
index a1e3a8fe936738aa3733b9fef2507c0f8d0c78b0..a44335562f95deaaabc1c29574e346683831436c 100644
--- a/restructuring/model/preemption/floating.v
+++ b/restructuring/model/preemption/floating.v
@@ -1,4 +1,4 @@
 Require Export rt.restructuring.model.preemption.valid_model.
-Require Export rt.restructuring.model.preemption.valid_schedule.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
diff --git a/restructuring/model/preemption/limited.v b/restructuring/model/preemption/limited.v
index ba3d31790db7e4f03d8a268e312196e92ad9c949..fad9bf13e26fa7ea353f2fb4f09b57e75c6a4d7c 100644
--- a/restructuring/model/preemption/limited.v
+++ b/restructuring/model/preemption/limited.v
@@ -1,4 +1,4 @@
 Require Export rt.restructuring.model.preemption.valid_model.
-Require Export rt.restructuring.model.preemption.valid_schedule.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.limited_preemptive.
 Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
diff --git a/restructuring/model/preemption/nonpreemptive.v b/restructuring/model/preemption/nonpreemptive.v
index 026c58041a11a4224c9d6e1232e5b1689894326f..b213f96366346c34ec74d2e7e11624b108f65a6d 100644
--- a/restructuring/model/preemption/nonpreemptive.v
+++ b/restructuring/model/preemption/nonpreemptive.v
@@ -1,6 +1,6 @@
 Require Export rt.restructuring.model.schedule.nonpreemptive.
 
-Require Export rt.restructuring.model.preemption.valid_schedule.
+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.
 Require Export rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
diff --git a/restructuring/model/preemption/preemptive.v b/restructuring/model/preemption/preemptive.v
index 872abdd1833a96a6a212f9e28deda848bc10158a..4a081def8377252074f6300364d7d7caaf003ca6 100644
--- a/restructuring/model/preemption/preemptive.v
+++ b/restructuring/model/preemption/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.valid_schedule.
+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.
 Require Export rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
diff --git a/restructuring/model/preemption/valid_schedule.v b/restructuring/model/schedule/limited_preemptive.v
similarity index 100%
rename from restructuring/model/preemption/valid_schedule.v
rename to restructuring/model/schedule/limited_preemptive.v