diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 68a2ebaa5b091484f730cb372e412ddcf8a5a241..03df8f5ac881df063f69e3310051cc2be06d0b3f 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -5,7 +5,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.rtc_threshold.valid_rtct.
+
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.analysis.schedulability.
Require Import rt.restructuring.analysis.basic_facts.all.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 98c0f7ba978ce39ca7855499106b85b3360df7ca..350c71c37d24aedd165b5dab142bcc6799a426e5 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
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.rtc_threshold.valid_rtct.
+
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.task.preemption.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 4a4e11d947ce546aec12618cbb97f2778ebc7bcb..255cd93ca6fc6c32e07a4c323ddc8cb05b8c574b 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.preemption.valid_model.
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.
+
Require Import rt.restructuring.model.preemption.job.instance.limited.
(** * Platform for Models with Limited Preemptions *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index 727b6a712ecd18246db200cd653a939ced01f190..efaaf78a228cfbcb87de382012def67fb87f3ec6 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index e02f731464eed908df7595a88299911c75daf029..1bd61dbd6b8b9137256c8760a8f4210a4da692aa 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
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.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.floating.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 4a4f9f54aead398294041a7a5c6fbc44d5a6f6f7..0535ccf6acd1566084f502e909e9494df6529587 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.job.
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.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.task.preemption.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index b3b14df8e84a5b41fa2bba213220cc80b6dd59fa..aa42896dabe167ab7174e82e344f38dd1ed3d0d9 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
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.rtc_threshold.valid_rtct.
+
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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 33e41a46f2ee55dcb50ceb18cf9b2e633df4b2df..59ffdcbb0654e88c421ab76ce44a8982d048b68b 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
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.rtc_threshold.valid_rtct.
+
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.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 9a918e50acfdaf25ee0c0a0f6a6af39546760aef..fd6ad2ea1a365b6ab3f1b3a682cab40ae5ccbb43 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.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.rtc_threshold.valid_rtct.
+
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index d24bcd4edb956d3dbd5a3f37d0802cad23a64961..961efe2fb52dcc888f712a18f714a01fb7bec102 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
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.rtc_threshold.valid_rtct.
+
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 23f6787d0687fad6efbc08d7200e433705f29e84..3f5bec3e2be62c162aadbe674ea852a7d8e21376 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -11,7 +11,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
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.rtc_threshold.valid_rtct.
+
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index 54e45fcc7da41d2c26b3581d8a27c5d500614ce8..48361205fef154044f44cf48250ad3e38f990bb7 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
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.rtc_threshold.valid_rtct.
+
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/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index b80e1ae55ba2ac699bc79b05c007f87181c8e085..7d97db5a07d76793e2316b503440f4026988b210 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
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.rtc_threshold.valid_rtct.
+
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/model/preemption/rtc_threshold/valid_rtct.v b/restructuring/model/preemption/rtc_threshold/valid_rtct.v
deleted file mode 100644
index d3d4e82776a5e235f98f9183303b7059b2f7be01..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/rtc_threshold/valid_rtct.v
+++ /dev/null
@@ -1,64 +0,0 @@
-Require Export rt.restructuring.model.preemption.valid_model.
-
-(** * Task's Run-to-Completion Threshold *)
-(** Since a task model may not provide exact information about
- preemption point of a task, task's run-to-completion threshold
- cannot be defined in terms of preemption points of a task (unlike
- job's run-to-completion threshold). Therefore, we can assume the
- existence of a function that maps a task to its run-to-completion
- threshold. In this section we define the notion of a valid
- run-to-completion threshold of a task. *)
-Section ValidTaskRunToCompletionThreshold.
-
- (** Consider any type of tasks ... *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType}.
- Context `{JobTask Job Task}.
- Context `{JobCost Job}.
-
- (** In addition, we assume existence of a function
- maping jobs to theirs preemption points ... *)
- Context `{JobPreemptable Job}.
-
- (** ...and a function mapping tasks to theirs
- run-to-completion threshold. *)
- Context `{TaskRunToCompletionThreshold Task}.
-
- (** Consider any kind of processor state model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
-
- (** ... any job arrival sequence, ... *)
- Variable arr_seq: arrival_sequence Job.
-
- (** ... and any given schedule. *)
- Variable sched: schedule PState.
-
- (** A task's run-to-completion threshold should be at most the cost of the task. *)
- Definition task_run_to_completion_threshold_le_task_cost tsk :=
- task_run_to_completion_threshold tsk <= task_cost tsk.
-
- (** We say that the run-to-completion threshold of a task tsk bounds
- the job run-to-completionthreshold iff for any job j of task tsk
- the job run-to-completion threshold is less than or equal to the
- task run-to-completion threshold. *)
- Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
- forall j,
- arrives_in arr_seq j ->
- job_task j = tsk ->
- job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
-
- (** We say that task_run_to_completion_threshold is a valid task
- run-to-completion threshold for a task tsk iff
- [task_run_to_completion_threshold tsk] is (1) no bigger than
- tsk's cost, (2) for any job of task tsk
- job_run_to_completion_threshold is bounded by
- task_run_to_completion_threshold. *)
- Definition valid_task_run_to_completion_threshold tsk :=
- task_run_to_completion_threshold_le_task_cost tsk /\
- task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
-
-End ValidTaskRunToCompletionThreshold.
\ No newline at end of file
diff --git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index d4307eacdd03ece89c4aeb692e26b1271b4c72e7..7d3efc635d0b96b8d0315bdbc390f87b8ab30ef1 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ -1,4 +1,5 @@
Require Export rt.util.all.
+Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
@@ -48,3 +49,67 @@ Section MaxAndLastNonpreemptiveSegment.
last0 (distances (task_preemption_points tsk)).
End MaxAndLastNonpreemptiveSegment.
+
+
+(** * Task's Run-to-Completion Threshold *)
+(** Since a task model may not provide exact information about
+ preemption point of a task, task's run-to-completion threshold
+ cannot be defined in terms of preemption points of a task (unlike
+ job's run-to-completion threshold). Therefore, we can assume the
+ existence of a function that maps a task to its run-to-completion
+ threshold. In this section we define the notion of a valid
+ run-to-completion threshold of a task. *)
+Section ValidTaskRunToCompletionThreshold.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+
+ (** In addition, we assume existence of a function
+ maping jobs to theirs preemption points ... *)
+ Context `{JobPreemptable Job}.
+
+ (** ...and a function mapping tasks to theirs
+ run-to-completion threshold. *)
+ Context `{TaskRunToCompletionThreshold Task}.
+
+ (** Consider any kind of processor state model, ... *)
+ Context {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (** ... any job arrival sequence, ... *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (** ... and any given schedule. *)
+ Variable sched: schedule PState.
+
+ (** A task's run-to-completion threshold should be at most the cost of the task. *)
+ Definition task_run_to_completion_threshold_le_task_cost tsk :=
+ task_run_to_completion_threshold tsk <= task_cost tsk.
+
+ (** We say that the run-to-completion threshold of a task tsk bounds
+ the job run-to-completionthreshold iff for any job j of task tsk
+ the job run-to-completion threshold is less than or equal to the
+ task run-to-completion threshold. *)
+ Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_task j = tsk ->
+ job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
+
+ (** We say that task_run_to_completion_threshold is a valid task
+ run-to-completion threshold for a task tsk iff
+ [task_run_to_completion_threshold tsk] is (1) no bigger than
+ tsk's cost, (2) for any job of task tsk
+ job_run_to_completion_threshold is bounded by
+ task_run_to_completion_threshold. *)
+ Definition valid_task_run_to_completion_threshold tsk :=
+ task_run_to_completion_threshold_le_task_cost tsk /\
+ task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
+
+End ValidTaskRunToCompletionThreshold.