diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 3283abbd552cba08397e104a517cfe4afa5a54ab..467bf8b6c6fefe143531f25804aa46292e0f7f08 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -1,17 +1,6 @@
-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.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.analysis.schedulability.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.reduction_of_search_space.
-Require Import rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
+Require Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.abstract.core.reduction_of_search_space.
+Require Export rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 6f07e82972fb387b5ba2afe7e9e21f6a74053972..5cef8756827286d0975c9b09aba60e9054799082 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -1,28 +1,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.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.
-
-Require Import rt.restructuring.model.task.sequentiality.
-Require Import rt.restructuring.analysis.schedulability.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Import rt.restructuring.analysis.basic_facts.workload.
-Require Import rt.restructuring.analysis.task_schedule.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.analysis.basic_facts.task_arrivals.
-
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.reduction_of_search_space.
-Require Import rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
-Require Import rt.restructuring.analysis.abstract.core.abstract_rta.
+Require Export rt.restructuring.analysis.task_schedule.
+Require Export rt.restructuring.analysis.arrival.rbf.
+Require Export rt.restructuring.analysis.basic_facts.task_arrivals.
+Require Export rt.restructuring.analysis.abstract.core.abstract_rta.
   
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 22116f1dd728685b7215adafc59f1446995d361d..e0341070e4ddea954b1fc7216407a895ca02203b 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,6 +1,6 @@
-Require Import rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.task.concept.
+Require Export rt.restructuring.model.task.concept.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
   
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 95e11dde69566d2bedf6e8295da1054fd58ae120..faf66a2b10e0dcdd90205246b46b5a0437979942 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
@@ -1,12 +1,5 @@
-Require Import rt.util.all.
-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.parameter.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.abstract.core.definitions.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/instantiations/ideal_processor.v
index 6e2a74c4989098491bcc81a9b00846f61e0ff297..f8bb0094128a93e8bbb2eb4926239a0ba2b95e16 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/instantiations/ideal_processor.v
@@ -1,13 +1,5 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.aggregate.workload.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.task.sequentiality.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.definitions.busy_interval.
-Require Import rt.restructuring.analysis.definitions.priority_inversion.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
+Require Export rt.restructuring.analysis.definitions.priority_inversion.
+Require Export rt.restructuring.analysis.abstract.core.abstract_seq_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** In this file we consider an ideal uni-processor ... *)
@@ -16,7 +8,6 @@ Require Import rt.restructuring.model.processor.ideal.
 (** ... and classic model of readiness without jitter and no
     self-suspensions, where pending jobs are always ready. *)
 Require Import rt.restructuring.model.readiness.basic.
- 
 
 (** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
 (** In this module we instantiate functions Interference and Interfering Workload 
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index bde7b2ae1bb3aa828e6675e7a01f32582ecba6ee..e9c18f44565063ee8952ce59d4232593ecde5d18 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,10 +1,5 @@
-Require Import rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.aggregate.task_arrivals.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.arrival.workload_bound.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 07be1832e592b0fd8e790a0c905b06e19299f34c..98471fce2d2ec76c77e051e42b8ecc53bca7ea49 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,12 +1,6 @@
-Require Import rt.util.sum.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.aggregate.task_arrivals.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.analysis.basic_facts.workload.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Import rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.basic_facts.workload.
+Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.model.arrival.arrival_curves.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index d57646ad175a9609ec730b111409767ff5a3cd90..35d507ff8947f1e91182c0ce72b3ad8f64e258cf 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,9 +1,6 @@
-Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.service.
 Require Export rt.restructuring.analysis.basic_facts.arrivals.
 
-Require Export rt.util.nat.
-
 (** In this file, we establish basic facts about job completions. *)
 
 Section CompletionFacts.
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
index 47163b68c4b879559cb1d3e46b4af9b3283fe689..fb80bdae30201642d29c4f6c01efc4420ac31dd4 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -1,5 +1,3 @@
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.service.
 Require Export rt.restructuring.analysis.basic_facts.completion.
 
 (** In this file, we observe basic properties of the behavioral job
diff --git a/restructuring/analysis/basic_facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
index 707b53a2b94dbedd31b9210dcfecd1aff8f26f84..4759a455b0015159e26ff37accbe96401318711f 100644
--- a/restructuring/analysis/basic_facts/ideal_schedule.v
+++ b/restructuring/analysis/basic_facts/ideal_schedule.v
@@ -1,6 +1,9 @@
 From mathcomp Require Import all_ssreflect.
+Require Export rt.restructuring.model.processor.platform_properties.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.processor.platform_properties.
+
 (** Note: we do not re-export the basic definitions to avoid littering the global
    namespace with type class instances. *)
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index bde0d0fc0976418af8057ce2e023af2d5c74a59c..81e57d5753e230ac56cf15a39ab2b50f16c06098 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -1,14 +1,8 @@
-Require Import rt.util.all.
-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.parameter.
-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.limited_preemptive.
+Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
+
+Require Export 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 06493bcc510ce0bbcccbd34a5c53e6dd4dd91fda..efa8ad2f52566c4295efe03a29a690b49895bc82 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -1,14 +1,9 @@
-Require Import rt.util.all.
-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.schedule.nonpreemptive.
+Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.model.schedule.nonpreemptive.
 
-Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 
-
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Platform for Fully Non-Preemptive model *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index 53852d2d8a662bcfd98d714604d9e0045f59d8e0..f5f56bdef2dc9fcc15651e854c2b28a6a04556a0 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -1,8 +1,4 @@
-Require Import rt.util.all.
-Require Import rt.restructuring.behavior.all.
-
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.fully_preemptive.
 
 (** * Preemptions in Fully Premptive Model *)
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index afae13c18218d730afbba142a8622d9f012091c3..4a2d046f7f65fae448de76fbc07e192545501b67 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -1,15 +1,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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
-
 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.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
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 099296ceb41bd60df0d09982926c4f66e30c004d..8ea77ec19d16d33b6b2ae0ce9fd92e6f35b6cee1 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,10 +1,6 @@
-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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
 (** In this section, we provide a few basic properties 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 72e2dd08881698ca9763558bcb6730dcc02ed826..f515e6358616c052713f1d6c625c67af04287f96 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -1,17 +1,8 @@
-Require Import rt.util.all.
-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 Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 
-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.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.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 6f7f0d2659a06b061f1882c51a8fc28bf5c8f3d1..8875e0e6feac0c3174ad3d3245ce308263c6bd01 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,15 +1,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.schedule.nonpreemptive.
-
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.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.
 
 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 3bbbd6e6256b14660f9a02557974bee43df32451..25f5ab7fe14ec75a1c43a138a49dd1ac28f5f2fe 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -1,8 +1,3 @@
-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.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 d00940655e0ab559081f1d8dbb6a4b5089b122ba..286e8d2e23f6070fd974956b3dff2e189db435b5 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -1,16 +1,7 @@
-Require Import rt.util.all.
-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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.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.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 17f9ba3d275329077a5c52b2c0cbe5bc8b746766..fb3661327163aed67e27734101b6b5afb65b2077 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -1,15 +1,7 @@
-Require Import rt.util.all.
-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 Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
 
-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.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
index d9d3235e4d2065d8fdfe9b330b917b14ea398b1a..717d7cdde85b9a6bb3f686c7d84bb70841b24013 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
@@ -1,13 +1,7 @@
-Require Import rt.util.all.
-Require Import rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
 
-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.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_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/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index 7fbbc1952311316316d17320540c69a9ee5a1544..1a33d34bbc01692bc0cce0d9ea131945701af2b6 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
@@ -1,11 +1,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 Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.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.
 
 (** * Platform for Fully Premptive Model *)
 (** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index a845717736296dee04a1710a28230600f22ba95b..543fcdf4b93df4768a3280e0a06901167559aaef 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -1,11 +1,7 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
-
-Require Export rt.restructuring.behavior.all.
+Require Export rt.util.all.
 Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Export rt.restructuring.model.processor.platform_properties.
-Require Import rt.util.tactics.
-Require Import rt.util.step_function.
-Require Import rt.util.sum.
+
+From mathcomp Require Import ssrnat ssrbool fintype.
 
 (** In this file, we establish basic facts about the service received by
     jobs. *)
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 698a63177683e4aacb7361980f3e6fce26a307ea..2d10fa54b2a3d6ea80b7b34303a29e8433c98d5d 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -1,17 +1,8 @@
-Require Import rt.util.all.
-
-Require Import rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.aggregate.workload.
 Require Export rt.restructuring.model.aggregate.service_of_jobs.
-Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.processor.platform_properties.
-Require Import rt.restructuring.model.priority.classes.
-
-Require Import rt.restructuring.analysis.basic_facts.arrivals.
-Require Import rt.restructuring.analysis.basic_facts.service.
-Require Import rt.restructuring.analysis.basic_facts.completion.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.analysis.basic_facts.completion.
+
+Require Import rt.restructuring.model.processor.ideal.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/basic_facts/workload.v b/restructuring/analysis/basic_facts/workload.v
index 67c71814b7cfc8f3edbbda7b804e82deb2ded405..942bd65826d11848c034177461812fa27a86476e 100644
--- a/restructuring/analysis/basic_facts/workload.v
+++ b/restructuring/analysis/basic_facts/workload.v
@@ -1,7 +1,5 @@
-Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.basic_facts.arrivals.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/definitions/busy_interval.v
index 0857ebc79f1d523b1fff9f404b442651063d50bf..5a2edb38fd9a8e7731f6a75c827836fea65da315 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/definitions/busy_interval.v
@@ -1,9 +1,8 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
+Require Export rt.restructuring.model.priority.classes.
+Require Export rt.restructuring.analysis.basic_facts.completion.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/no_carry_in.v
index 2118f1c9ff870365e5d462965a8f97a72d3aab89..f30d12ba15eec51560986479b284e7fc86c35b5e 100644
--- a/restructuring/analysis/definitions/no_carry_in.v
+++ b/restructuring/analysis/definitions/no_carry_in.v
@@ -1,8 +1,8 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.restructuring.model.priority.classes.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** * No Carry-In *)
@@ -34,4 +34,4 @@ Section NoCarryIn.
       arrived_before j_o t ->
       completed_by sched j_o t.
 
-End NoCarryIn.
+End NoCarryIn. 
\ No newline at end of file
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/definitions/priority_inversion.v
index 559b0a207be062afa14971f9fb69842c2209ea9b..a868dba5cf986fe8fd5b01483bdb668321c2ee7c 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/definitions/priority_inversion.v
@@ -1,10 +1,3 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index e111ffeb1ec43a8ab9b000e742deb3a0595083b9..1d05d354e041149a613dfad6da830bb2f4509939 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -1,26 +1,9 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+
 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.schedule.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
-
-Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 08df29bc1a6e09c042c5ad93a531f096a50721e6..5f3aafd5227e4fa0a45fd6a259e8465db6c3bd22 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -1,24 +1,9 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+
 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.schedule.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 5449e5c8e16e58c6203e13338d93ee890d9e358d..503ea76a0fecb947266d67966adfc6463b7ddc84 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -1,25 +1,11 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+
+Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 
 (** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index c8d0f915754de3b1a53e726daf4364d7b47b7e3f..338deb12070711cebd62d9f6d8372d59b2e6df56 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -1,20 +1,7 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
+
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.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 bbcc0919607d4bbdef36c8c40a3e462548ef1a3a..de5919d6490f2e30f64607221fc8e8c0d4c57c7a 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -1,25 +1,9 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
+Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
+Require Export rt.restructuring.analysis.arrival.rbf.
+
 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.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.analysis.facts.priority_inversion_is_bounded.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 481eba5330ba3d1f744360d8559b2f830e2ed74c..5d71602be938e18d289cc95877d4b8c75fe1bc82 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -1,32 +1,10 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.facts.edf.
+Require Export rt.restructuring.model.schedule.priority_driven.
+Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
+Require Export rt.restructuring.analysis.schedulability.
+
 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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.schedulability.
-Require Export rt.restructuring.analysis.definitions.no_carry_in.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
 Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index d5600eb1dfc8d29f2d698f26ecd0c39ebd57089e..3e08644788e015e9e3fec68c294c16856f982b3a 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -1,16 +1,12 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
+Require Export rt.restructuring.analysis.basic_facts.all.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
 
-(** Throughout the file we assume for the classic Liu & Layland model
-   of readiness without jitter and no self-suspensions, where prending
-   jobs are always ready. *)
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 196b6376c1b10e6436a30da88ae5fe3a3525e83c..1e9b85e351606b76463bd27d495a4e6364719454 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -1,18 +1,10 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
 Require Export rt.restructuring.analysis.facts.busy_interval_exists.
 
-(** Throughout the file we assume for the classic Liu & Layland model
-   of readiness without jitter and no self-suspensions, where prending
-   jobs are always ready. *)
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index c0b7ad091ab2e6e504a13f99d4870e61ca07c53d..33fa5cd7a4a3668e17668c45a198f3ddb0f6e22b 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -1,15 +1,5 @@
-Require Import rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
-
-Require Import rt.restructuring.model.schedule.preemption_time.
-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.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
+Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index c84d38c4ecace597151659d7adbf252a2dce52aa..988413f76256ab7e6ed358081038846d8bc55bb3 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -1,24 +1,13 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.schedule.limited_preemptive.
+
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
-Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index fcc437b33f5e8da7978c61c83dbc1b681b7553c9..214f3969633db03c24ebc1bf4ce42f3130357762 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -1,23 +1,13 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.schedule.limited_preemptive.
+
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index ec552eb4628fb931a01fa732b75775949d168b86..f78d709f25139362cbb012c8bb3c9e21f9d6d01f 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -1,26 +1,14 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 
-(** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.schedule.nonpreemptive.
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
 
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
+Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index f5ec02a06607af04b5b616d01b44524100dc5dab..c411242a27515dbe47b516096b592ca6362c353f 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -1,23 +1,10 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
 
 (** Assume we have a fully preemptive model. *)
+Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 0797d23a7459e8acfc91111d846c434cafd1f80b..88825b64be14fc0bbc89fc2da5b439953183a2f1 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
@@ -1,23 +1,13 @@
-Require Import rt.util.all.
-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.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 Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.arrival.workload_bound.
+Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
+Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
 
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
-Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 3ca80c5bfdaf1d55a02a8a2083fe1631ed6b9a30..8662ed9f271d9e3018439ab73bfb8945ddde079b 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -1,29 +1,13 @@
-Require Import rt.util.all.
-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.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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
-
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.schedulability.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
+Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
 Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/transform/facts/swaps.v
index 016ad4d5ff1ed570eb440736ba4aa4ba12b76629..d59d6035c3d84be426919ecdb21cd1965b2b3d92 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/transform/facts/swaps.v
@@ -1,7 +1,4 @@
-Require Export rt.restructuring.analysis.transform.swap.
 Require Export rt.restructuring.analysis.transform.facts.replace_at.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.util.nat.
 
 (** In this file, we establish invariants about schedules in which two
     allocations have been swapped, as for instance it is done in the
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 0d6af127644e2f67c687a634b0abf8b472b6a2b1..d22cedb042519d03e520511be9db2d3f4c161ded 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -1,5 +1,7 @@
 Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
      
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index a66d11cc539fae00f8e3c794b2a39d9ea244a5a5..3c801eabcf14a5554a5f2b57905cf651ac38f51e 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.limited_preemptive.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.parameters.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.