diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 8a9eef37be6a8dc80c19cf58542b9291a1089a6e..bde0d0fc0976418af8057ce2e023af2d5c74a59c 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
-Require Import rt.restructuring.model.preemption.job.instance.limited.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index 42fa25ea3630a8b0d0827dda0086313b33cff12c..06493bcc510ce0bbcccbd34a5c53e6dd4dd91fda 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 
 Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
+Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index e09ef19d5dc5fa57908d1b3cc85ae8b09617fce0..53852d2d8a662bcfd98d714604d9e0045f59d8e0 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
 
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.job.instance.preemptive.
+Require Import rt.restructuring.model.preemption.fully_preemptive.
 
 (** * Preemptions in Fully Premptive Model *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index f9c02c1303bcf6774a26d4dc7101ba1f9b37b82b..afae13c18218d730afbba142a8622d9f012091c3 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
-Require Import rt.restructuring.model.preemption.job.instance.limited.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 9a7f2c99c8b16056203b973163080410f43ce86b..72e2dd08881698ca9763558bcb6730dcc02ed826 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.job.instance.limited.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 2f1f3584ac45f2c3e93dba078c4829d8d597c68a..6f7f0d2659a06b061f1882c51a8fc28bf5c8f3d1 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
-Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
+Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 4c2d58e6092efe5d7b7c9fd5246442fe40781bcd..3bbbd6e6256b14660f9a02557974bee43df32451 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 
-Require Import rt.restructuring.model.preemption.job.instance.preemptive.
+Require Import rt.restructuring.model.preemption.fully_preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 2fca1a499b3afde7a706165b2aafc1993e34c0cb..d00940655e0ab559081f1d8dbb6a4b5089b122ba 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
-Require Import rt.restructuring.model.preemption.job.instance.limited.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 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 20b7e7395f93b40adc530ba561cedb5dd4f48480..17f9ba3d275329077a5c52b2c0cbe5bc8b746766 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
-Require Import rt.restructuring.model.preemption.job.instance.limited.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
index 7646eed4ca39c516ecc2522ddd73a1501c9fcbe8..d9d3235e4d2065d8fdfe9b330b917b14ea398b1a 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
@@ -5,7 +5,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.schedule.nonpreemptive.
-Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
+Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index a32ac7b2add605e4120a1af8722adbfe8f150931..7fbbc1952311316316d17320540c69a9ee5a1544 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 
-Require Import rt.restructuring.model.preemption.job.instance.preemptive.
+Require Import rt.restructuring.model.preemption.fully_preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
 
diff --git a/restructuring/model/preemption/job/instance/nonpreemptive.v b/restructuring/model/preemption/fully_nonpreemptive.v
similarity index 100%
rename from restructuring/model/preemption/job/instance/nonpreemptive.v
rename to restructuring/model/preemption/fully_nonpreemptive.v
diff --git a/restructuring/model/preemption/job/instance/preemptive.v b/restructuring/model/preemption/fully_preemptive.v
similarity index 100%
rename from restructuring/model/preemption/job/instance/preemptive.v
rename to restructuring/model/preemption/fully_preemptive.v
diff --git a/restructuring/model/preemption/job/instance/limited.v b/restructuring/model/preemption/limited_preemptive.v
similarity index 100%
rename from restructuring/model/preemption/job/instance/limited.v
rename to restructuring/model/preemption/limited_preemptive.v
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 61eff9396e2ce295085e0af72e954f6bd2fd243f..d0e75b0ac27f5734022b05d7938790db909b8545 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.instance.limited.
+Require Export rt.restructuring.model.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 194ceb278d48297aa18566d2688c3cfb6716d54c..343a6db764f32b60d2d7bebf77987f1900587e41 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.instance.limited.
+Require Export rt.restructuring.model.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.