diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index 1bd61dbd6b8b9137256c8760a8f4210a4da692aa..e3e91e0cf575c52a8fe0bb5831ca27c959a1a1fa 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -7,7 +7,6 @@ Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.floating.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 0535ccf6acd1566084f502e909e9494df6529587..cebdf4816d86985b492ab62dff9975600a156629 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -9,7 +9,6 @@ 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.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index aa42896dabe167ab7174e82e344f38dd1ed3d0d9..b90c5e803e8806c95285b93a3f5659cae3ad7311 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -9,7 +9,6 @@ Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 59ffdcbb0654e88c421ab76ce44a8982d048b68b..4c2d58e6092efe5d7b7c9fd5246442fe40781bcd 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -5,7 +5,6 @@ Require Import rt.restructuring.model.task.concept.
 
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 
 (** * Task's Run to Completion Threshold *)
diff --git a/restructuring/model/preemption/floating.v b/restructuring/model/preemption/floating.v
index a44335562f95deaaabc1c29574e346683831436c..4f8f8b04c27e06ed19ab8a427eab260a0aecda7c 100644
--- a/restructuring/model/preemption/floating.v
+++ b/restructuring/model/preemption/floating.v
@@ -1,4 +1,3 @@
 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.
-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 fad9bf13e26fa7ea353f2fb4f09b57e75c6a4d7c..a1f943c35ebc2cbd22fc34acb1f3f0c91346851b 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.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 b213f96366346c34ec74d2e7e11624b108f65a6d..e3b6368e74306422f43fa50db898b2ba20167963 100644
--- a/restructuring/model/preemption/nonpreemptive.v
+++ b/restructuring/model/preemption/nonpreemptive.v
@@ -3,4 +3,3 @@ 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.
-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 4a081def8377252074f6300364d7d7caaf003ca6..3f5028e7e3e89d08b88f3b7de6eb69bee68aa4ed 100644
--- a/restructuring/model/preemption/preemptive.v
+++ b/restructuring/model/preemption/preemptive.v
@@ -1,4 +1,3 @@
 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/rtc_threshold/instance/floating.v b/restructuring/model/preemption/rtc_threshold/instance/floating.v
deleted file mode 100644
index 4b87a208c04035e13e06dc14e245b23f9c82f873..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/floating.v
+++ /dev/null
@@ -1,21 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
-    threshold] for the model with floating non-preemptive regions. *)
-Section TaskRTCThresholdFloatingNonPreemptiveRegions.
-
-  (** Consider any type of tasks.*)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-  
-  (** In the model with floating non-preemptive regions, task has to
-      static information about the placement of preemption
-      points. Thus, the only safe task's run to completion threshold
-      is [task cost]. *)
-  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
-    { 
-      task_run_to_completion_threshold (tsk : Task) := task_cost tsk
-    }.
-
-End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/limited.v b/restructuring/model/preemption/rtc_threshold/instance/limited.v
deleted file mode 100644
index 14efa28707e6b94e6978682dc3b66389fe9bd0dc..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/limited.v
+++ /dev/null
@@ -1,24 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
-    threshold] for the limited preemptions model. *)
-Section TaskRTCThresholdLimitedPreemptions.
-  
-  (** Consider any type of tasks. *)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-  Context `{TaskPreemptionPoints Task}.
-    
-  (** In the model with limited preemptions, no job can be preempted after
-      a job reaches its last non-preemptive segment. Thus, we can
-      set task's run to completion threshold to [task_cost tsk -
-      (task_last_nonpr_seg tsk - ε)] which is always greater than
-      [job_cost j - (job_last_nonpr_seg j - ε)]. *)
-  Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
-    { 
-      task_run_to_completion_threshold (tsk : Task) :=
-        task_cost tsk - (task_last_nonpr_segment tsk - ε)
-    }.
-  
-End TaskRTCThresholdLimitedPreemptions.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
deleted file mode 100644
index 271f11b4a0ed65f422ca38898634a53d512874ed..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
-    threshold] for the fully non-preemptive model. *)
-Section TaskRTCThresholdFullyNonPreemptive.
-
-  (** Consider any type of tasks. *)
-  Context {Task : TaskType}. 
-  Context `{TaskCost Task}.
-    
-  (** In fully non-preemptive model no job can be preempted until its
-      completion. Thus, we can set task's run to completion threshold
-      to ε. *)
-  Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
-    { 
-      task_run_to_completion_threshold (tsk : Task) := ε
-    }.
-
-End TaskRTCThresholdFullyNonPreemptive.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
deleted file mode 100644
index 30459d065514b25314e78921d5873baade82ef03..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
-   threshold] for the fully preemptive model. *)
-Section TaskRTCThresholdFullyPreemptiveModel.
-
-  (** Consider any type of tasks. *)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-
-  (** In the fully preemptive model any job can be preempted at any time. Thus, 
-       the only safe task's run to completion threshold is [task cost]. *)
-  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
-    { 
-      task_run_to_completion_threshold (tsk : Task) := task_cost tsk
-    }.
-    
-End TaskRTCThresholdFullyPreemptiveModel.
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 6b3837b8dfdf1162475aac75db65ac2857e3ecf7..61eff9396e2ce295085e0af72e954f6bd2fd243f 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -39,3 +39,23 @@ Section ModelWithFloatingNonpreemptiveRegions.
     job_max_np_segment_le_task_max_np_segment.
 
 End ModelWithFloatingNonpreemptiveRegions.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+    threshold] for the model with floating non-preemptive regions. *)
+Section TaskRTCThresholdFloatingNonPreemptiveRegions.
+
+  (** Consider any type of tasks.*)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  
+  (** In the model with floating non-preemptive regions, task has to
+      static information about the placement of preemption
+      points. Thus, the only safe task's run to completion threshold
+      is [task cost]. *)
+  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) := task_cost tsk
+    }.
+
+End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/restructuring/model/task/preemption/fully_nonpreemptive.v
index ced8e61bea1cb714288caf9ac194cdb3fba6f176..c470b16c520febafcf357c8abf70bfbe81ec4fab 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/task/preemption/fully_nonpreemptive.v
@@ -21,3 +21,25 @@ Section FullyNonPreemptiveModel.
     }.
                                                      
 End FullyNonPreemptiveModel.
+
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+    threshold] for the fully non-preemptive model. *)
+Section TaskRTCThresholdFullyNonPreemptive.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}. 
+  Context `{TaskCost Task}.
+    
+  (** In fully non-preemptive model no job can be preempted until its
+      completion. Thus, we can set task's run to completion threshold
+      to ε. *)
+  Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) := ε
+    }.
+
+End TaskRTCThresholdFullyNonPreemptive.
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/restructuring/model/task/preemption/fully_preemptive.v
index fba328695fb1cd6cdc564eaf093755df08bc3ab7..a8f0f210cde6712f1db8f86a4447d5e87cfdedc6 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/restructuring/model/task/preemption/fully_preemptive.v
@@ -16,3 +16,23 @@ Section FullyPreemptiveModel.
     }.
   
 End FullyPreemptiveModel.
+
+Require Export rt.restructuring.model.task.preemption.parameters.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+   threshold] for the fully preemptive model. *)
+Section TaskRTCThresholdFullyPreemptiveModel.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** In the fully preemptive model any job can be preempted at any time. Thus, 
+       the only safe task's run to completion threshold is [task cost]. *)
+  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) := task_cost tsk
+    }.
+    
+End TaskRTCThresholdFullyPreemptiveModel.
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 380996b0e19915fe4d4819b6b6a5c67a96737228..194ceb278d48297aa18566d2688c3cfb6716d54c 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -84,3 +84,27 @@ Section ModelWithFixedPreemptionPoints.
     valid_fixed_preemption_points_task_model.
   
 End ModelWithFixedPreemptionPoints.
+
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+    threshold] for the limited preemptions model. *)
+Section TaskRTCThresholdLimitedPreemptions.
+  
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskPreemptionPoints Task}.
+    
+  (** In the model with limited preemptions, no job can be preempted after
+      a job reaches its last non-preemptive segment. Thus, we can
+      set task's run to completion threshold to [task_cost tsk -
+      (task_last_nonpr_seg tsk - ε)] which is always greater than
+      [job_cost j - (job_last_nonpr_seg j - ε)]. *)
+  Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) :=
+        task_cost tsk - (task_last_nonpr_segment tsk - ε)
+    }.
+  
+End TaskRTCThresholdLimitedPreemptions.