diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 03df8f5ac881df063f69e3310051cc2be06d0b3f..3283abbd552cba08397e104a517cfe4afa5a54ab 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -2,8 +2,8 @@ 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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 350c71c37d24aedd165b5dab142bcc6799a426e5..6f07e82972fb387b5ba2afe7e9e21f6a74053972 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -3,8 +3,8 @@ 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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.arrival.arrival_curves.
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index 00a4644ac5751900647e2ab984c2222fbe4dda48..95e11dde69566d2bedf6e8295da1054fd58ae120 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -3,8 +3,8 @@ Require Export rt.restructuring.behavior.all.
 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.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.abstract.core.definitions.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 255cd93ca6fc6c32e07a4c323ddc8cb05b8c574b..8a9eef37be6a8dc80c19cf58542b9291a1089a6e 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -3,9 +3,9 @@ Require Import rt.restructuring.behavior.all.
 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.parameter.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
-Require Import rt.restructuring.model.preemption.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.limited.
@@ -164,36 +164,36 @@ Section ModelWithLimitedPreemptions.
 
     (** Recall that file [job.parameters] also defines notion of
         preemption poins.  And note that
-        [job.parameters.job_preemption_points] cannot have a
+        [job.parameter.job_preemption_points] cannot have a
         duplicating preemption points. Therefore, we need additional
-        lemmas to relate [job.parameters.job_preemption_points] and
+        lemmas to relate [job.parameter.job_preemption_points] and
         [limited.job_preemption_points]]. *)
 
     (** First we show that the length of the last non-preemptive
-        segment of [job.parameters.job_preemption_points] is equal to
+        segment of [job.parameter.job_preemption_points] is equal to
         the length of the last non-empty non-preemptive segment of
         [limited.job_preemption_points]. *)
     Lemma job_parameters_last_np_to_job_limited:
-        last0 (distances (parameters.job_preemption_points j)) =
+        last0 (distances (parameter.job_preemption_points j)) =
         last0 (filter (fun x => 0 < x) (distances (job_preemption_points j))).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
+      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
       intros; rewrite distances_iota_filtered; eauto.
       rewrite -A2 //.
         by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
     Qed.
 
     (** Next we show that the length of the max non-preemptive
-        segment of [job.parameters.job_preemption_points] is equal to
+        segment of [job.parameter.job_preemption_points] is equal to
         the length of the max non-preemptive segment of
         [limited.job_preemption_points]. *)
     Lemma job_parameters_max_np_to_job_limited:
-      max0 (distances (parameters.job_preemption_points j)) =
+      max0 (distances (parameter.job_preemption_points j)) =
       max0 (distances (job_preemption_points j)).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
+      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
       intros; rewrite distances_iota_filtered; eauto 2.
       rewrite max0_rem0 //.
       rewrite -A2 //.
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index efaaf78a228cfbcb87de382012def67fb87f3ec6..42fa25ea3630a8b0d0827dda0086313b33cff12c 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -4,8 +4,8 @@ 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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index 1392a0cfb06a5865c168e9a37a0e30e3c655853f..e09ef19d5dc5fa57908d1b3cc85ae8b09617fce0 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index e3e91e0cf575c52a8fe0bb5831ca27c959a1a1fa..f9c02c1303bcf6774a26d4dc7101ba1f9b37b82b 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.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.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 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/rtc_threshold/job_preemptable.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
index f446e860d78ca896bb7e2ce37ec956b3ed49cf1b..099296ceb41bd60df0d09982926c4f66e30c004d 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -2,8 +2,8 @@ Require Import rt.util.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index cebdf4816d86985b492ab62dff9975600a156629..9a7f2c99c8b16056203b973163080410f43ce86b 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 
 Require Import rt.restructuring.model.schedule.limited_preemptive.
-Require Import rt.restructuring.model.preemption.job.parameters.
+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.task.preemption.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index b90c5e803e8806c95285b93a3f5659cae3ad7311..2f1f3584ac45f2c3e93dba078c4829d8d597c68a 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -3,8 +3,8 @@ 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.schedule.nonpreemptive.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index fd6ad2ea1a365b6ab3f1b3a682cab40ae5ccbb43..2fca1a499b3afde7a706165b2aafc1993e34c0cb 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -3,8 +3,8 @@ Require Import rt.util.nondecreasing.
 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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.limited.
@@ -68,7 +68,7 @@ Section FloatingNonPremptiveRegionsModel.
     case: (posnP (job_cost j)) => [ZERO|POS].
     - split.
       rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
-              /lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
+              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
       rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
       + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
         exists 0; rewrite LE; split; first by apply/andP; split.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index e51e4269d0ef4e4714d488d2fb2661f22a85b9b2..20b7e7395f93b40adc530ba561cedb5dd4f48480 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -3,8 +3,8 @@ Require Import rt.util.nondecreasing.
 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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+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.
@@ -66,7 +66,7 @@ Section LimitedPreemptionsModel.
     case: (posnP (job_cost j)) => [ZERO|POS].
     - split.
       rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
-              /lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
+              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
       rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
       + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
         exists 0; rewrite LE; split; first by apply/andP; split.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index c9ea62b6699854e37115b1e2e0617234b136bd98..a32ac7b2add605e4120a1af8722adbfe8f150931 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/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.valid_model.
+
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
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 961efe2fb52dcc888f712a18f714a01fb7bec102..bbcc0919607d4bbdef36c8c40a3e462548ef1a3a 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -7,8 +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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 3f5bec3e2be62c162aadbe674ea852a7d8e21376..481eba5330ba3d1f744360d8559b2f830e2ed74c 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -8,8 +8,8 @@ Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.aggregate.task_arrivals.
 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.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index ad9688c9f2e696d03dc527933376793c4f781400..c0b7ad091ab2e6e504a13f99d4870e61ca07c53d 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.model.preemption.valid_model.
+
 Require Import rt.restructuring.model.schedule.preemption_time.
-Require Import rt.restructuring.model.preemption.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
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 48361205fef154044f44cf48250ad3e38f990bb7..0797d23a7459e8acfc91111d846c434cafd1f80b 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
@@ -7,8 +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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 7d97db5a07d76793e2316b503440f4026988b210..3ca80c5bfdaf1d55a02a8a2083fe1631ed6b9a30 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -7,8 +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.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/model/preemption/job/instance/limited.v b/restructuring/model/preemption/job/instance/limited.v
index 8b631a17f69a9ec6c277c0636e0b4dcfe5a083b2..d4345918c966c593b041f9b017c133a413985773 100644
--- a/restructuring/model/preemption/job/instance/limited.v
+++ b/restructuring/model/preemption/job/instance/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
 Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** Definition of a parameter relating a job
diff --git a/restructuring/model/preemption/job/instance/nonpreemptive.v b/restructuring/model/preemption/job/instance/nonpreemptive.v
index 804d5e3fc9b446f6ae440a5557f20f153367dd74..95f900017c6b894ec368e9c30d56ace65dc6eae3 100644
--- a/restructuring/model/preemption/job/instance/nonpreemptive.v
+++ b/restructuring/model/preemption/job/instance/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
 
 (** * Platform for Fully Non-Preemptive Model *)
 (** In this section, we instantiate [job_preemptable] for the fully
diff --git a/restructuring/model/preemption/job/instance/preemptive.v b/restructuring/model/preemption/job/instance/preemptive.v
index 6febcfda714c88333f75241e19c8d27197c54d89..9f8e026d86600c8de0dacef824469fe9629ab0a9 100644
--- a/restructuring/model/preemption/job/instance/preemptive.v
+++ b/restructuring/model/preemption/job/instance/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
 
 (** * Platform for Fully Premptive Model *)
 (** In this section, we instantiate [job_preemptable] for the fully
diff --git a/restructuring/model/preemption/job/parameters.v b/restructuring/model/preemption/parameter.v
similarity index 55%
rename from restructuring/model/preemption/job/parameters.v
rename to restructuring/model/preemption/parameter.v
index 9ce2edafa637fdea87d2a07032f2c94b5d15a680..20a26f083232dbbde09f8629578532e2c21443a2 100644
--- a/restructuring/model/preemption/job/parameters.v
+++ b/restructuring/model/preemption/parameter.v
@@ -74,3 +74,69 @@ Section MaxAndLastNonpreemptiveSegment.
     job_cost j - (job_last_nonpreemptive_segment j - ε).
   
 End MaxAndLastNonpreemptiveSegment. 
+
+(** * Platform with limited preemptions *)
+(** In the follwoing, we define properties that any reasonable job preemption
+    model must satisfy. *)
+Section PreemptionModel.
+
+  (**  Consider any type of jobs... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** ... and the existence of a predicate mapping a job and
+      its progress to a boolean value saying whether this job is
+      preemptable at its current point of execution. *)
+  Context `{JobPreemptable Job}.
+
+  (** 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.
+
+  (** In this section, we define the notion of a valid preemption model. *)
+  Section ValidPreemptionModel.
+
+    (** We require that a job has to be executed at least one time
+        instant in order to reach a nonpreemptive segment. In other
+        words, a job must start execution to become non-preemptive. *)
+    Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
+      job_preemptable j 0.
+
+    (** And vice versa, a job cannot remain non-preemptive after its completion. *)
+    Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
+      job_preemptable j (job_cost j).
+
+    (** Next, if a job j is not preemptive at some time instant t,
+        then j must be scheduled at time t. *)
+    Definition not_preemptive_implies_scheduled (j : Job) :=
+      forall t,
+        ~~ job_preemptable j (service sched j t) ->
+        scheduled_at sched j t.
+
+    (** A job can start its execution only from a preemption point. *)
+    Definition execution_starts_with_preemption_point (j : Job) :=
+      forall prt,
+        ~~ scheduled_at sched j prt ->
+        scheduled_at sched j prt.+1 ->
+        job_preemptable j (service sched j prt.+1).
+
+    (** We say that a preemption model is a valid preemption model if
+       all the assumptions given above are satisfied for any job. *)
+    Definition valid_preemption_model :=
+      forall j,
+        arrives_in arr_seq j ->
+        job_cannot_become_nonpreemptive_before_execution j
+        /\ job_cannot_be_nonpreemptive_after_completion j
+        /\ not_preemptive_implies_scheduled j
+        /\ execution_starts_with_preemption_point j.
+
+  End ValidPreemptionModel.
+
+End PreemptionModel.
diff --git a/restructuring/model/preemption/valid_model.v b/restructuring/model/preemption/valid_model.v
deleted file mode 100644
index 38ae8fb60c803323719811fed22e430de1434817..0000000000000000000000000000000000000000
--- a/restructuring/model/preemption/valid_model.v
+++ /dev/null
@@ -1,67 +0,0 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
-
-(** * Platform with limited preemptions *)
-(** In the follwoing, we define properties that any reasonable job preemption
-    model must satisfy. *)
-Section PreemptionModel.
-
-  (**  Consider any type of jobs... *)
-  Context {Job : JobType}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
-
-  (** ... and the existence of a predicate mapping a job and
-      its progress to a boolean value saying whether this job is
-      preemptable at its current point of execution. *)
-  Context `{JobPreemptable Job}.
-
-  (** 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.
-
-  (** In this section, we define the notion of a valid preemption model. *)
-  Section ValidPreemptionModel.
-
-    (** We require that a job has to be executed at least one time
-        instant in order to reach a nonpreemptive segment. In other
-        words, a job must start execution to become non-preemptive. *)
-    Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
-      job_preemptable j 0.
-
-    (** And vice versa, a job cannot remain non-preemptive after its completion. *)
-    Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
-      job_preemptable j (job_cost j).
-
-    (** Next, if a job j is not preemptive at some time instant t,
-        then j must be scheduled at time t. *)
-    Definition not_preemptive_implies_scheduled (j : Job) :=
-      forall t,
-        ~~ job_preemptable j (service sched j t) ->
-        scheduled_at sched j t.
-
-    (** A job can start its execution only from a preemption point. *)
-    Definition execution_starts_with_preemption_point (j : Job) :=
-      forall prt,
-        ~~ scheduled_at sched j prt ->
-        scheduled_at sched j prt.+1 ->
-        job_preemptable j (service sched j prt.+1).
-
-    (** We say that a preemption model is a valid preemption model if
-       all the assumptions given above are satisfied for any job. *)
-    Definition valid_preemption_model :=
-      forall j,
-        arrives_in arr_seq j ->
-        job_cannot_become_nonpreemptive_before_execution j
-        /\ job_cannot_be_nonpreemptive_after_completion j
-        /\ not_preemptive_implies_scheduled j
-        /\ execution_starts_with_preemption_point j.
-
-  End ValidPreemptionModel.
-
-End PreemptionModel.
diff --git a/restructuring/model/schedule/limited_preemptive.v b/restructuring/model/schedule/limited_preemptive.v
index 1a96bfbbb97f74112182d0685ae8170db8c69009..2cc39396f778f9c3346ddeb7b2f78085ee3da2b6 100644
--- a/restructuring/model/schedule/limited_preemptive.v
+++ b/restructuring/model/schedule/limited_preemptive.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
  
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/schedule/preemption_time.v b/restructuring/model/schedule/preemption_time.v
index e355941a7998b2224a03f65f80c268e0be43108b..790fd66f77cf0f939b868ae41bd079b6b1b8421e 100644
--- a/restructuring/model/schedule/preemption_time.v
+++ b/restructuring/model/schedule/preemption_time.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.preemption.valid_model.
+Require Export rt.restructuring.model.preemption.parameter.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Preemption Time in Ideal Uni-Processor Model *)
diff --git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index 686f863e2ef680a7b7e41c38f698165ce01842e3..78ce4904486fe7543fba966ff84399f4b0fe74ac 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ -1,6 +1,5 @@
 Require Export rt.util.all.
-Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.valid_model.
+Require Export rt.restructuring.model.preemption.parameter.
 Require Export rt.restructuring.model.task.concept.
 (** * Static information about preemption points *)