From 064a1c759d82b31116829fcaf14f83b84767366d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 25 Nov 2019 16:42:30 +0100
Subject: [PATCH] re-organization of the analysis module, part 1

This is not yet the final organization, but already an improvement.

Move main high-level results to separate top-level `results` module.
Rationale: Let's make it very clear where to find the main, high-level
results in Prosa, and at the same time let's declutter the analysis
namespace.

Other notable change, apart from moving files around:

- move two key analysis definitions to analysis.definitions
- split RBF definition and facts into separate files
- move facts about ideal schedule to ideal_schedule.v
---
 .../abstract/{core => }/abstract_rta.v        |   6 +-
 .../abstract/{core => }/abstract_seq_rta.v    |   8 +-
 .../core/run_to_completion_threshold.v        |   0
 .../abstract/{core => }/definitions.v         |   0
 .../ideal_processor.v => ideal_jlfp_rta.v}    |   4 +-
 ...letion_threshold.v => run_to_completion.v} |   4 +-
 ...ction_of_search_space.v => search_space.v} |   0
 restructuring/analysis/arrival/rbf.v          |  92 -----
 .../analysis/arrival/workload_bound.v         | 291 ----------------
 restructuring/analysis/basic_facts/all.v      |   8 -
 .../analysis/basic_facts/ideal_schedule.v     | 113 ------
 .../{definitions => concepts}/busy_interval.v |   2 +-
 .../priority_inversion.v                      |   2 +-
 .../concepts/request_bound_function.v         |  94 +++++
 .../analysis/{ => concepts}/schedulability.v  |   2 +-
 .../definitions/{no_carry_in.v => carry_in.v} |   0
 .../{ => definitions}/task_schedule.v         |   2 +-
 restructuring/analysis/facts/behavior/all.v   |   8 +
 .../behavior}/arrivals.v                      |   0
 .../behavior}/completion.v                    |   4 +-
 .../behavior}/deadlines.v                     |   2 +-
 .../analysis/facts/behavior/ideal_schedule.v  | 222 ++++++++++++
 .../behavior}/sequential.v                    |   0
 .../{basic_facts => facts/behavior}/service.v | 111 +-----
 .../behavior}/service_of_jobs.v               |   6 +-
 .../behavior}/task_arrivals.v                 |   0
 .../behavior}/workload.v                      |   2 +-
 ...busy_interval_exists.v => busy_interval.v} |   4 +-
 .../{no_carry_in_exists.v => carry_in.v}      |   4 +-
 .../preemption/job/limited.v                  |   2 +-
 .../preemption/job/nonpreemptive.v            |   2 +-
 .../preemption/job/preemptive.v               |   0
 .../preemption/rtc_threshold/floating.v       |   4 +-
 .../rtc_threshold/job_preemptable.v           |   2 +-
 .../preemption/rtc_threshold/limited.v        |   4 +-
 .../preemption/rtc_threshold/nonpreemptive.v  |   2 +-
 .../preemption/rtc_threshold/preemptive.v     |   2 +-
 .../preemption/task/floating.v                |   2 +-
 .../preemption/task/limited.v                 |   2 +-
 .../preemption/task/nonpreemptive.v           |   2 +-
 .../preemption/task/preemptive.v              |   2 +-
 ...sion_is_bounded.v => priority_inversion.v} |   6 +-
 restructuring/analysis/facts/rbf.v            | 323 ++++++++++++++++++
 .../analysis/facts/readiness/basic.v          |   2 +-
 .../facts => facts/transform}/edf_opt.v       |   4 +-
 .../facts => facts/transform}/replace_at.v    |   1 +
 .../facts => facts/transform}/swaps.v         |   3 +-
 restructuring/analysis/transform/prefix.v     |   2 +-
 restructuring/analysis/transform/swap.v       |   2 +-
 .../{analysis => results}/edf/optimality.v    |   2 +-
 .../edf/rta/bounded_nps.v}                    |   6 +-
 .../edf/rta/bounded_pi.v}                     |  15 +-
 .../edf/rta/floating_nonpreemptive.v}         |   4 +-
 .../edf/rta/fully_nonpreemptive.v}            |   6 +-
 .../edf/rta/fully_preemptive.v}               |   6 +-
 .../edf/rta/limited_preemptive.v}             |   4 +-
 .../fixed_priority/rta/bounded_nps.v}         |  10 +-
 .../fixed_priority/rta/bounded_pi.v}          |  12 +-
 .../rta/floating_nonpreemptive.v}             |   4 +-
 .../fixed_priority/rta/fully_nonpreemptive.v} |   6 +-
 .../fixed_priority/rta/fully_preemptive.v}    |   6 +-
 .../fixed_priority/rta/limited_preemptive.v}  |   4 +-
 62 files changed, 744 insertions(+), 701 deletions(-)
 rename restructuring/analysis/abstract/{core => }/abstract_rta.v (99%)
 rename restructuring/analysis/abstract/{core => }/abstract_seq_rta.v (99%)
 delete mode 100644 restructuring/analysis/abstract/core/run_to_completion_threshold.v
 rename restructuring/analysis/abstract/{core => }/definitions.v (100%)
 rename restructuring/analysis/abstract/{instantiations/ideal_processor.v => ideal_jlfp_rta.v} (99%)
 rename restructuring/analysis/abstract/{core/sufficient_condition_for_run_to_completion_threshold.v => run_to_completion.v} (98%)
 rename restructuring/analysis/abstract/{core/reduction_of_search_space.v => search_space.v} (100%)
 delete mode 100644 restructuring/analysis/arrival/rbf.v
 delete mode 100644 restructuring/analysis/arrival/workload_bound.v
 delete mode 100644 restructuring/analysis/basic_facts/all.v
 delete mode 100644 restructuring/analysis/basic_facts/ideal_schedule.v
 rename restructuring/analysis/{definitions => concepts}/busy_interval.v (98%)
 rename restructuring/analysis/{definitions => concepts}/priority_inversion.v (97%)
 create mode 100644 restructuring/analysis/concepts/request_bound_function.v
 rename restructuring/analysis/{ => concepts}/schedulability.v (98%)
 rename restructuring/analysis/definitions/{no_carry_in.v => carry_in.v} (100%)
 rename restructuring/analysis/{ => definitions}/task_schedule.v (96%)
 create mode 100644 restructuring/analysis/facts/behavior/all.v
 rename restructuring/analysis/{basic_facts => facts/behavior}/arrivals.v (100%)
 rename restructuring/analysis/{basic_facts => facts/behavior}/completion.v (98%)
 rename restructuring/analysis/{basic_facts => facts/behavior}/deadlines.v (97%)
 create mode 100644 restructuring/analysis/facts/behavior/ideal_schedule.v
 rename restructuring/analysis/{basic_facts => facts/behavior}/sequential.v (100%)
 rename restructuring/analysis/{basic_facts => facts/behavior}/service.v (79%)
 rename restructuring/analysis/{basic_facts => facts/behavior}/service_of_jobs.v (98%)
 rename restructuring/analysis/{basic_facts => facts/behavior}/task_arrivals.v (100%)
 rename restructuring/analysis/{basic_facts => facts/behavior}/workload.v (94%)
 rename restructuring/analysis/facts/{busy_interval_exists.v => busy_interval.v} (99%)
 rename restructuring/analysis/facts/{no_carry_in_exists.v => carry_in.v} (99%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/job/limited.v (99%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/job/nonpreemptive.v (98%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/job/preemptive.v (100%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/rtc_threshold/floating.v (90%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/rtc_threshold/job_preemptable.v (99%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/rtc_threshold/limited.v (97%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/rtc_threshold/nonpreemptive.v (97%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/rtc_threshold/preemptive.v (94%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/task/floating.v (98%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/task/limited.v (98%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/task/nonpreemptive.v (97%)
 rename restructuring/analysis/{basic_facts => facts}/preemption/task/preemptive.v (96%)
 rename restructuring/analysis/facts/{priority_inversion_is_bounded.v => priority_inversion.v} (99%)
 create mode 100644 restructuring/analysis/facts/rbf.v
 rename restructuring/analysis/{transform/facts => facts/transform}/edf_opt.v (99%)
 rename restructuring/analysis/{transform/facts => facts/transform}/replace_at.v (98%)
 rename restructuring/analysis/{transform/facts => facts/transform}/swaps.v (99%)
 rename restructuring/{analysis => results}/edf/optimality.v (98%)
 rename restructuring/{analysis/edf/rta/nonpr_reg/response_time_bound.v => results/edf/rta/bounded_nps.v} (99%)
 rename restructuring/{analysis/edf/rta/response_time_bound.v => results/edf/rta/bounded_pi.v} (98%)
 rename restructuring/{analysis/edf/rta/nonpr_reg/concrete_models/floating.v => results/edf/rta/floating_nonpreemptive.v} (97%)
 rename restructuring/{analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v => results/edf/rta/fully_nonpreemptive.v} (96%)
 rename restructuring/{analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v => results/edf/rta/fully_preemptive.v} (96%)
 rename restructuring/{analysis/edf/rta/nonpr_reg/concrete_models/limited.v => results/edf/rta/limited_preemptive.v} (98%)
 rename restructuring/{analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v => results/fixed_priority/rta/bounded_nps.v} (97%)
 rename restructuring/{analysis/fixed_priority/rta/response_time_bound.v => results/fixed_priority/rta/bounded_pi.v} (97%)
 rename restructuring/{analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v => results/fixed_priority/rta/floating_nonpreemptive.v} (97%)
 rename restructuring/{analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v => results/fixed_priority/rta/fully_nonpreemptive.v} (95%)
 rename restructuring/{analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v => results/fixed_priority/rta/fully_preemptive.v} (95%)
 rename restructuring/{analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v => results/fixed_priority/rta/limited_preemptive.v} (97%)

diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/abstract_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/core/abstract_rta.v
rename to restructuring/analysis/abstract/abstract_rta.v
index 467bf8b6c..088b34a7f 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/abstract_rta.v
@@ -1,6 +1,6 @@
-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.
+Require Export rt.restructuring.analysis.concepts.schedulability.
+Require Export rt.restructuring.analysis.abstract.search_space.
+Require Export rt.restructuring.analysis.abstract.run_to_completion.
 
 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/abstract_seq_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/core/abstract_seq_rta.v
rename to restructuring/analysis/abstract/abstract_seq_rta.v
index 5cef87568..41c01f681 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/abstract_seq_rta.v
@@ -1,7 +1,7 @@
-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.
+Require Export rt.restructuring.analysis.definitions.task_schedule.
+Require Export rt.restructuring.analysis.facts.rbf.
+Require Export rt.restructuring.analysis.facts.behavior.task_arrivals.
+Require Export rt.restructuring.analysis.abstract.abstract_rta.
   
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/core/run_to_completion_threshold.v b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
deleted file mode 100644
index e69de29bb..000000000
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/definitions.v
similarity index 100%
rename from restructuring/analysis/abstract/core/definitions.v
rename to restructuring/analysis/abstract/definitions.v
diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/ideal_jlfp_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/instantiations/ideal_processor.v
rename to restructuring/analysis/abstract/ideal_jlfp_rta.v
index f8bb00941..535e0b06c 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/ideal_jlfp_rta.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.abstract.core.abstract_seq_rta.
+Require Export rt.restructuring.analysis.concepts.priority_inversion.
+Require Export rt.restructuring.analysis.abstract.abstract_seq_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** In this file we consider an ideal uni-processor ... *)
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/run_to_completion.v
similarity index 98%
rename from restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
rename to restructuring/analysis/abstract/run_to_completion.v
index faf66a2b1..63f0ef08d 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/run_to_completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
-Require Export rt.restructuring.analysis.abstract.core.definitions.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.abstract.definitions.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/restructuring/analysis/abstract/core/reduction_of_search_space.v b/restructuring/analysis/abstract/search_space.v
similarity index 100%
rename from restructuring/analysis/abstract/core/reduction_of_search_space.v
rename to restructuring/analysis/abstract/search_space.v
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
deleted file mode 100644
index e9c18f445..000000000
--- a/restructuring/analysis/arrival/rbf.v
+++ /dev/null
@@ -1,92 +0,0 @@
-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.
-
-(** * Request Bound Functions (RBF) *)
-(** In this section, we prove some properties of Request Bound Functions (RBF). *)
-Section RequestBoundFunctions.
-  
-  (** Consider any type of tasks ... *)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-
-  (** ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  
-  (** Consider any arrival sequence. *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_arrival_times_are_consistent:
-    consistent_arrival_times arr_seq.
-
-  (** Let tsk be any task. *)
-  Variable tsk : Task.
-
-  (** Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts 
-     [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function 
-     that equals 0 for the empty interval delta = 0. *)
-  Context `{MaxArrivals Task}.
-  Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
-  Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
-  
-  (** Let's define some local names for clarity. *)
-  Let task_rbf := task_request_bound_function tsk.
-
-  (** We prove that [task_rbf 0] is equal to 0. *)
-  Lemma task_rbf_0_zero:
-    task_rbf 0 = 0.
-  Proof.
-    rewrite /task_rbf /task_request_bound_function.
-    apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
-      by move: H_valid_arrival_curve => [T1 T2].
-  Qed.
-  
-  (** We prove that task_rbf is monotone. *)
-  Lemma task_rbf_monotone:
-    monotone task_rbf leq.
-  Proof.
-    rewrite /monotone; intros ? ? LE.
-    rewrite /task_rbf /task_request_bound_function leq_mul2l.
-    apply/orP; right.
-      by move: H_valid_arrival_curve => [_ T]; apply T.
-  Qed.      
-  
-  (** Consider any job j of tsk. This guarantees that 
-     there exists at least one job of task tsk. *)
-  Variable j : Job.
-  Hypothesis H_j_arrives : arrives_in arr_seq j.
-  Hypothesis H_job_of_tsk : job_task j = tsk.
-  
-  (** Then we prove that task_rbf 1 is greater than or equal to task cost. *)
-  Lemma task_rbf_1_ge_task_cost:
-    task_rbf 1 >= task_cost tsk.
-  Proof.
-    have ALT: forall n, n = 0 \/ n > 0.
-    { by clear; intros n; destruct n; [left | right]. }
-    specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z. 
-    rewrite leqNgt; apply/negP; intros CONTR.
-    move: H_is_arrival_curve => ARRB.
-    specialize (ARRB (job_arrival j) (job_arrival j + 1)).
-    feed ARRB; first by rewrite leq_addr.
-    rewrite addKn in ARRB.
-    move: CONTR; rewrite /task_rbf /task_request_bound_function; move => CONTR.
-    move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move => /andP [_ CONTR].
-    move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move => /eqP CONTR.
-    move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move => /negP T; apply: T.
-    rewrite /number_of_task_arrivals -has_predT. 
-    rewrite /task_arrivals_between.
-    apply/hasP; exists j; last by done.
-    rewrite /arrivals_between addn1 big_nat_recl; last by done. 
-    rewrite big_geq ?cats0; last by done.
-    rewrite mem_filter.
-    apply/andP; split.
-    - by apply/eqP.
-    - move: H_j_arrives => [t ARR].
-      move: (ARR) => CONS.
-      apply H_arrival_times_are_consistent in CONS.
-        by rewrite CONS.
-  Qed.
-  
-End RequestBoundFunctions.
\ No newline at end of file
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
deleted file mode 100644
index 98471fce2..000000000
--- a/restructuring/analysis/arrival/workload_bound.v
+++ /dev/null
@@ -1,291 +0,0 @@
-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.
-
-(** * Task Workload Bounded by Arrival Curves *)
-Section TaskWorkloadBoundedByArrivalCurves.
-
-  (** Consider any type of tasks ... *)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-
-  (**  ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
-  
-  (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-
-  (** ... and any ideal uniprocessor schedule of this arrival sequence.*)
-  Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
-
-  (** Consider an FP policy that indicates a higher-or-equal priority relation. *)
-  Variable higher_eq_priority : FP_policy Task.
-  Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
-
-  (** For simplicity, let's define some local names. *)
-  Let arrivals_between := arrivals_between arr_seq.
-  
-  (** We define the notion of request bound function. *)
-  Section RequestBoundFunction.
-    
-    (** Let MaxArrivals denote any function that takes a task and an interval length
-       and returns the associated number of job arrivals of the task. *) 
-    Context `{MaxArrivals Task}.
-    
-    (** In this section, we define a bound for the workload of a single task
-       under uniprocessor FP scheduling. *)
-    Section SingleTask.
-
-      (** Consider any task tsk that is to be scheduled in an interval of length delta. *)
-      Variable tsk : Task.
-      Variable delta : duration.
-
-      (** We define the following workload bound for the task. *)
-      Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
-
-    End SingleTask.
-
-    (** In this section, we define a bound for the workload of multiple tasks. *)
-    Section AllTasks.
-
-      (** Consider a task set ts... *)
-      Variable ts : list Task.
-
-      (** ...and let tsk be any task in task set. *)
-      Variable tsk : Task.
-      
-      (** Let delta be the length of the interval of interest. *)
-      Variable delta : duration.
-      
-      (** Recall the definition of higher-or-equal-priority task and
-         the per-task workload bound for FP scheduling. *)
-      Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
-      Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
-
-      (** Using the sum of individual workload bounds, we define the following bound
-         for the total workload of tasks in any interval of length delta. *)
-      Definition total_request_bound_function :=
-        \sum_(tsk <- ts) task_request_bound_function tsk delta.
-      
-      (** Similarly, we define the following bound for the total workload of tasks of 
-         higher-or-equal priority (with respect to tsk) in any interval of length delta. *)
-      Definition total_hep_request_bound_function_FP :=
-        \sum_(tsk_other <- ts | is_hep_task tsk_other)
-         task_request_bound_function tsk_other delta.
-      
-      (** We also define a bound for the total workload of higher-or-equal 
-         priority tasks other than tsk in any interval of length delta. *)
-      Definition total_ohep_request_bound_function_FP :=
-        \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
-         task_request_bound_function tsk_other delta.
-      
-    End AllTasks.
-
-  End RequestBoundFunction.
-
-  (** In this section we prove some lemmas about request bound functions. *)
-  Section ProofWorkloadBound.
-
-    (** Consider a task set ts... *)
-    Variable ts : list Task.
-
-    (** ...and let tsk be any task in ts. *)
-    Variable tsk : Task.
-    Hypothesis H_tsk_in_ts : tsk \in ts.
-
-    (** Assume that the job costs are no larger than the task costs. *)
-    Hypothesis H_job_cost_le_task_cost :
-      cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
-
-    (** Next, we assume that all jobs come from the task set. *)
-    Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
-      
-    (** Let max_arrivals be any arrival bound for taskset ts. *)
-    Context `{MaxArrivals Task}.
-    Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts. 
-    
-    (** Let's define some local names for clarity. *)
-    Let task_rbf := task_request_bound_function tsk.
-    Let total_rbf := total_request_bound_function ts.
-    Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
-    Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
-
-    (** Next, we consider any job j of tsk. *)
-    Variable j : Job.
-    Hypothesis H_j_arrives : arrives_in arr_seq j.
-    Hypothesis H_job_of_tsk : job_task j = tsk.
-    
-    (** Next, we say that two jobs j1 and j2 are in relation other_higher_eq_priority, iff 
-       j1 has higher or equal priority than j2 and is produced by a different task. *)
-    Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
-
-    (** Next, we recall the notions of total workload of jobs... *)
-    Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between t1 t2).
-    
-    (** ...notions of workload of higher or equal priority jobs... *)
-    Let total_hep_workload t1 t2 :=
-      workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between t1 t2).
-    
-    (** ... workload of other higher or equal priority jobs... *)
-    Let total_ohep_workload t1 t2 :=
-      workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between t1 t2).
-
-    (** ... and the workload of jobs of the same task as job j. *)
-    Let task_workload t1 t2 :=
-      workload_of_jobs (job_of_task tsk) (arrivals_between t1 t2).
-    
-    (** In this section we prove that the workload of any jobs is 
-       no larger than the request bound function. *) 
-    Section WorkloadIsBoundedByRBF.
-
-      (** Consider any time t and any interval of length delta. *)
-      Variable t : instant.
-      Variable delta : instant.
-
-      (** First, we show that workload of task tsk is bounded by 
-         the number of arrivals of the task times the cost of the task. *)
-      Lemma task_workload_le_num_of_arrivals_times_cost:
-        task_workload t (t + delta)
-        <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta).
-      Proof.
-        rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.
-        rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.
-        rewrite /same_task -H_job_of_tsk muln1.
-        apply leq_sum_seq; move => j0 IN0 /eqP EQ.
-        rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
-          by apply H_job_cost_le_task_cost.
-      Qed.
-      
-      (** As a corollary, we prove that workload of task is 
-         no larger the than task request bound function. *)
-      Corollary task_workload_le_task_rbf:
-        task_workload t (t + delta) <= task_rbf delta.
-      Proof.    
-        apply leq_trans with
-            (task_cost tsk *  number_of_task_arrivals arr_seq tsk t (t + delta));
-          first by apply task_workload_le_num_of_arrivals_times_cost.
-        rewrite leq_mul2l; apply/orP; right.
-        rewrite -{2}[delta](addKn t).
-          by apply H_is_arrival_bound; last rewrite leq_addr.
-      Qed.
-
-      (** Next, we prove that total workload of other tasks with
-         higher-or-equal priority is no larger than the total
-         request bound function. *)
-      Lemma total_workload_le_total_rbf:
-        total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
-      Proof.        
-        set l := arrivals_between t (t + delta).
-        set hep := higher_eq_priority.        
-        apply leq_trans with
-            (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
-              (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
-        { intros.
-          rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
-          rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk. 
-          have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk && (job_task x != tsk)).
-          rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
-          rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
-          apply leq_sum; move => j0 /andP [IN0 HP0].
-          rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
-            by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
-        }
-        apply leq_sum_seq; intros tsk0 INtsk0 HP0.
-        apply leq_trans with
-            (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
-        { rewrite -sum1_size big_distrr /= big_filter.
-          rewrite /workload_of_jobs.
-          rewrite  muln1 /l /arrivals_between /arrival_sequence.arrivals_between. 
-          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
-            by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0.
-        }
-        { rewrite leq_mul2l; apply/orP; right.
-          rewrite -{2}[delta](addKn t).
-            by apply H_is_arrival_bound; last rewrite leq_addr.
-        }
-      Qed.
-
-      (** Next, we prove that total workload of tasks with higher-or-equal 
-         priority is no larger than the total request bound function. *)
-      Lemma total_workload_le_total_rbf':
-        total_hep_workload t (t + delta) <= total_hep_rbf delta.
-      Proof.
-        set l := arrivals_between t (t + delta).
-        set hep := higher_eq_priority.
-        apply leq_trans with
-            (n := \sum_(tsk' <- ts | hep tsk' tsk)
-                   (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
-        { rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk. 
-          have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk).
-          rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
-          rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
-          apply leq_sum; move => j0 /andP [IN0 HP0].
-          rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
-            by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
-        }
-        apply leq_sum_seq; intros tsk0 INtsk0 HP0.
-        apply leq_trans with
-            (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
-        { rewrite -sum1_size big_distrr /= big_filter.
-          rewrite -/l /workload_of_jobs.
-          rewrite muln1.
-          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
-          rewrite -EQ.
-          apply H_job_cost_le_task_cost.
-            by apply in_arrivals_implies_arrived in IN0.
-        }
-        { rewrite leq_mul2l; apply/orP; right.
-          rewrite -{2}[delta](addKn t).
-            by apply H_is_arrival_bound; last rewrite leq_addr.
-        }
-      Qed.
-      
-      (** Next, we prove that total workload of tasks is 
-         no larger than the total request bound function. *)
-      Lemma total_workload_le_total_rbf'':
-        total_workload t (t + delta) <= total_rbf delta.
-      Proof.
-        set l := arrivals_between t (t + delta).
-        apply leq_trans with
-            (n := \sum_(tsk' <- ts)
-                   (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
-        { rewrite /total_workload.
-          have EXCHANGE := exchange_big_dep predT.
-          rewrite EXCHANGE /=; clear EXCHANGE; last by done. 
-          rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
-          apply leq_sum; move => j0 /andP [IN0 HP0].
-          rewrite big_mkcond (big_rem (job_task j0)) /=.
-          rewrite eq_refl; apply leq_addr.
-            by apply in_arrivals_implies_arrived in IN0;
-              apply H_all_jobs_from_taskset.
-        }
-        apply leq_sum_seq; intros tsk0 INtsk0 HP0.
-        apply leq_trans with
-            (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
-        { rewrite -sum1_size big_distrr /= big_filter.
-          rewrite -/l /workload_of_jobs.
-          rewrite muln1.
-          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
-          rewrite -EQ.
-          apply H_job_cost_le_task_cost.
-            by apply in_arrivals_implies_arrived in IN0.
-        }
-        { rewrite leq_mul2l; apply/orP; right.
-          rewrite -{2}[delta](addKn t).
-            by apply H_is_arrival_bound; last rewrite leq_addr.
-        }
-      Qed.  
-
-    End WorkloadIsBoundedByRBF.
-
-  End ProofWorkloadBound.
-  
-End TaskWorkloadBoundedByArrivalCurves.
\ No newline at end of file
diff --git a/restructuring/analysis/basic_facts/all.v b/restructuring/analysis/basic_facts/all.v
deleted file mode 100644
index 51567b1bf..000000000
--- a/restructuring/analysis/basic_facts/all.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Export rt.restructuring.analysis.basic_facts.service.
-Require Export rt.restructuring.analysis.basic_facts.service_of_jobs.
-Require Export rt.restructuring.analysis.basic_facts.completion.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Export rt.restructuring.analysis.basic_facts.sequential.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
-Require Export rt.restructuring.analysis.basic_facts.deadlines.
-Require Export rt.restructuring.analysis.basic_facts.workload.
diff --git a/restructuring/analysis/basic_facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
deleted file mode 100644
index 4759a455b..000000000
--- a/restructuring/analysis/basic_facts/ideal_schedule.v
+++ /dev/null
@@ -1,113 +0,0 @@
-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.
-
-(** Note: we do not re-export the basic definitions to avoid littering the global
-   namespace with type class instances. *)
-
-(** In this section we estlish the classes to which an ideal schedule belongs. *)
-Section ScheduleClass.
-
-  Local Transparent service_in scheduled_in scheduled_on.
-  (** Consider any job type and the ideal processor model. *)
-  Context {Job: JobType}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.  
-
-  (** We note that the ideal processor model is indeed a uniprocessor
-     model. *)
-  Lemma ideal_proc_model_is_a_uniprocessor_model:
-    uniprocessor_model (processor_state Job).
-  Proof.
-    move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
-    by move: E1 E2=>->[].
-  Qed.
-
-  (** We observe that the ideal processor model falls into the category
-     of ideal-progress models, i.e., a scheduled job always receives
-     service. *)
-  Lemma ideal_proc_model_ensures_ideal_progress:
-    ideal_progress_proc_model (processor_state Job).
-  Proof.
-    move=> j s /existsP[[]/eqP->]/=.
-    by rewrite eqxx.
-  Qed.
-
-  (** The ideal processor model is a unit-service model. *)
-  Lemma ideal_proc_model_provides_unit_service:
-    unit_service_proc_model (processor_state Job).
-  Proof.
-    move=> j s.
-    rewrite /service_in/=/nat_of_bool.
-    by case:ifP.
-  Qed.
-
-  Lemma scheduled_in_def (j : Job) s :
-    scheduled_in j s = (s == Some j).
-  Proof.
-    rewrite /scheduled_in/scheduled_on/=.
-    case: existsP=>[[_->]//|].
-    case: (s == Some j)=>//=[[]].
-      by exists.
-  Qed.
-
-  Lemma scheduled_at_def sched (j : Job) t :
-    scheduled_at sched j t = (sched t == Some j).
-  Proof.
-      by rewrite /scheduled_at scheduled_in_def.
-  Qed.
-
-  Lemma service_in_is_scheduled_in (j : Job) s :
-    service_in j s = scheduled_in j s.
-  Proof.
-    by rewrite /service_in scheduled_in_def/=.
-  Qed.
-
-  Lemma service_at_is_scheduled_at sched (j : Job) t :
-    service_at sched j t = scheduled_at sched j t.
-  Proof.
-      by rewrite /service_at service_in_is_scheduled_in.
-  Qed.
-    
-  (** Next we prove a lemma which helps us to do a case analysis on
-   the state of an ideal schedule. *)
-  Lemma ideal_proc_model_sched_case_analysis:
-    forall (sched : schedule (ideal.processor_state Job)) (t : instant),
-      is_idle sched t \/ exists j, scheduled_at sched j t. 
-  Proof.
-    intros.
-    unfold is_idle; simpl; destruct (sched t) eqn:EQ.
-    - by right; exists s; auto; rewrite scheduled_at_def EQ.
-    - by left; auto.
-  Qed.
-  
-End ScheduleClass.
-
-(** * Automation *)
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq 
-    will be able to apply them automatically. *)
-Hint Resolve ideal_proc_model_is_a_uniprocessor_model
-     ideal_proc_model_ensures_ideal_progress
-     ideal_proc_model_provides_unit_service : basic_facts.
-
-(** We also provide tactics for case analysis on ideal processor state. *)
-
-(** The first tactic generates two subgoals: one with idle processor and 
-    the other with processor executing a job named JobName. *)
-Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
-  let Idle := fresh "Idle" in
-  let Sched := fresh "Sched_" JobName in
-  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
-
-(** The second tactic is similar to the first, but it additionally generates 
-    two equalities: [sched t = None] and [sched t = Some j]. *)
-Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
-  let Idle := fresh "Idle" in
-  let IdleEq := fresh "Eq" Idle in
-  let Sched := fresh "Sched_" JobName in 
-  let SchedEq := fresh "Eq" Sched in
-  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
-  [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
-  | move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/concepts/busy_interval.v
similarity index 98%
rename from restructuring/analysis/definitions/busy_interval.v
rename to restructuring/analysis/concepts/busy_interval.v
index bb1fff380..f2cde4cd5 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/concepts/busy_interval.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/concepts/priority_inversion.v
similarity index 97%
rename from restructuring/analysis/definitions/priority_inversion.v
rename to restructuring/analysis/concepts/priority_inversion.v
index a868dba5c..bc5271e68 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/concepts/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.definitions.busy_interval.
+Require Export rt.restructuring.analysis.concepts.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/concepts/request_bound_function.v b/restructuring/analysis/concepts/request_bound_function.v
new file mode 100644
index 000000000..f4401de56
--- /dev/null
+++ b/restructuring/analysis/concepts/request_bound_function.v
@@ -0,0 +1,94 @@
+Require Export rt.restructuring.model.arrival.arrival_curves.
+Require Export rt.restructuring.model.priority.classes.
+
+(** The following definitions assume ideal uniprocessor schedules.  This
+    restriction exists for historic reasons; the defined concepts could be
+    generalized in future work. *)
+Require Import rt.restructuring.analysis.facts.behavior.ideal_schedule.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Request Bound Function (RBF) *)
+
+(** We define the notion of a task's request-bound function (RBF), as well as
+    the total request bound function of a set of tasks. *)
+
+Section TaskWorkloadBoundedByArrivalCurves.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** ... and any type of jobs associated with these tasks, where each task has
+      a cost. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+
+  (** Consider any ideal uniprocessor schedule of these jobs... *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** ... and an FP policy that indicates a higher-or-equal priority
+      relation. *)
+  Variable higher_eq_priority : FP_policy Task.
+
+  (** Let MaxArrivals denote any function that takes a task and an interval length
+      and returns the associated number of job arrivals of the task. *)
+  Context `{MaxArrivals Task}.
+
+  (** ** RBF of a Single Task *)
+
+  (** In this section, we define a bound for the workload of a single task
+      under uniprocessor FP scheduling. *)
+  Section SingleTask.
+
+    (** Consider any task tsk that is to be scheduled in an interval of length delta. *)
+    Variable tsk : Task.
+    Variable delta : duration.
+
+    (** We define the following workload bound for the task. *)
+    Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
+
+  End SingleTask.
+
+  (** ** Total RBF of Multiple Tasks *)
+
+  (** In this section, we define a bound for the workload of multiple tasks. *)
+  Section AllTasks.
+
+    (** Consider a task set ts... *)
+    Variable ts : list Task.
+
+    (** ...and let tsk be any task in task set. *)
+    Variable tsk : Task.
+
+    (** Let delta be the length of the interval of interest. *)
+    Variable delta : duration.
+
+    (** Recall the definition of higher-or-equal-priority task and the per-task
+        workload bound for FP scheduling. *)
+    Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
+    Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
+
+    (** Using the sum of individual workload bounds, we define the following
+        bound for the total workload of tasks in any interval of length
+        delta. *)
+    Definition total_request_bound_function :=
+      \sum_(tsk <- ts) task_request_bound_function tsk delta.
+
+    (** Similarly, we define the following bound for the total workload of
+        tasks of higher-or-equal priority (with respect to tsk) in any interval
+        of length delta. *)
+    Definition total_hep_request_bound_function_FP :=
+      \sum_(tsk_other <- ts | is_hep_task tsk_other)
+       task_request_bound_function tsk_other delta.
+
+    (** We also define a bound for the total workload of higher-or-equal
+        priority tasks other than tsk in any interval of length delta. *)
+    Definition total_ohep_request_bound_function_FP :=
+      \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
+       task_request_bound_function tsk_other delta.
+
+  End AllTasks.
+
+End TaskWorkloadBoundedByArrivalCurves.
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/concepts/schedulability.v
similarity index 98%
rename from restructuring/analysis/schedulability.v
rename to restructuring/analysis/concepts/schedulability.v
index a3de0ced0..eaa3f136b 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/concepts/schedulability.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
 Require Import rt.restructuring.model.task.absolute_deadline.
 
 Section Task.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/carry_in.v
similarity index 100%
rename from restructuring/analysis/definitions/no_carry_in.v
rename to restructuring/analysis/definitions/carry_in.v
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/definitions/task_schedule.v
similarity index 96%
rename from restructuring/analysis/task_schedule.v
rename to restructuring/analysis/definitions/task_schedule.v
index 2f7eb103e..abd2757e6 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/definitions/task_schedule.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/behavior/all.v b/restructuring/analysis/facts/behavior/all.v
new file mode 100644
index 000000000..dbd7016f9
--- /dev/null
+++ b/restructuring/analysis/facts/behavior/all.v
@@ -0,0 +1,8 @@
+Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.restructuring.analysis.facts.behavior.service_of_jobs.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Export rt.restructuring.analysis.facts.behavior.sequential.
+Require Export rt.restructuring.analysis.facts.behavior.arrivals.
+Require Export rt.restructuring.analysis.facts.behavior.deadlines.
+Require Export rt.restructuring.analysis.facts.behavior.workload.
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/facts/behavior/arrivals.v
similarity index 100%
rename from restructuring/analysis/basic_facts/arrivals.v
rename to restructuring/analysis/facts/behavior/arrivals.v
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/facts/behavior/completion.v
similarity index 98%
rename from restructuring/analysis/basic_facts/completion.v
rename to restructuring/analysis/facts/behavior/completion.v
index 35d507ff8..d32bb55fb 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/facts/behavior/completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.basic_facts.service.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.restructuring.analysis.facts.behavior.arrivals.
 
 (** In this file, we establish basic facts about job completions. *)
 
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/facts/behavior/deadlines.v
similarity index 97%
rename from restructuring/analysis/basic_facts/deadlines.v
rename to restructuring/analysis/facts/behavior/deadlines.v
index fb80bdae3..777c92c79 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/facts/behavior/deadlines.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
 
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
diff --git a/restructuring/analysis/facts/behavior/ideal_schedule.v b/restructuring/analysis/facts/behavior/ideal_schedule.v
new file mode 100644
index 000000000..2435af2fc
--- /dev/null
+++ b/restructuring/analysis/facts/behavior/ideal_schedule.v
@@ -0,0 +1,222 @@
+From mathcomp Require Import all_ssreflect.
+Require Export rt.util.all.
+Require Export rt.restructuring.model.processor.platform_properties.
+Require Export rt.restructuring.analysis.facts.behavior.service.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
+(** Note: we do not re-export the basic definitions to avoid littering the global
+   namespace with type class instances. *)
+
+(** In this section we estlish the classes to which an ideal schedule belongs. *)
+Section ScheduleClass.
+
+  Local Transparent service_in scheduled_in scheduled_on.
+  (** Consider any job type and the ideal processor model. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.  
+
+  (** We note that the ideal processor model is indeed a uniprocessor
+     model. *)
+  Lemma ideal_proc_model_is_a_uniprocessor_model:
+    uniprocessor_model (processor_state Job).
+  Proof.
+    move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
+    by move: E1 E2=>->[].
+  Qed.
+
+  (** We observe that the ideal processor model falls into the category
+     of ideal-progress models, i.e., a scheduled job always receives
+     service. *)
+  Lemma ideal_proc_model_ensures_ideal_progress:
+    ideal_progress_proc_model (processor_state Job).
+  Proof.
+    move=> j s /existsP[[]/eqP->]/=.
+    by rewrite eqxx.
+  Qed.
+
+  (** The ideal processor model is a unit-service model. *)
+  Lemma ideal_proc_model_provides_unit_service:
+    unit_service_proc_model (processor_state Job).
+  Proof.
+    move=> j s.
+    rewrite /service_in/=/nat_of_bool.
+    by case:ifP.
+  Qed.
+
+  Lemma scheduled_in_def (j : Job) s :
+    scheduled_in j s = (s == Some j).
+  Proof.
+    rewrite /scheduled_in/scheduled_on/=.
+    case: existsP=>[[_->]//|].
+    case: (s == Some j)=>//=[[]].
+      by exists.
+  Qed.
+
+  Lemma scheduled_at_def sched (j : Job) t :
+    scheduled_at sched j t = (sched t == Some j).
+  Proof.
+      by rewrite /scheduled_at scheduled_in_def.
+  Qed.
+
+  Lemma service_in_is_scheduled_in (j : Job) s :
+    service_in j s = scheduled_in j s.
+  Proof.
+    by rewrite /service_in scheduled_in_def/=.
+  Qed.
+
+  Lemma service_at_is_scheduled_at sched (j : Job) t :
+    service_at sched j t = scheduled_at sched j t.
+  Proof.
+      by rewrite /service_at service_in_is_scheduled_in.
+  Qed.
+    
+  (** Next we prove a lemma which helps us to do a case analysis on
+   the state of an ideal schedule. *)
+  Lemma ideal_proc_model_sched_case_analysis:
+    forall (sched : schedule (ideal.processor_state Job)) (t : instant),
+      is_idle sched t \/ exists j, scheduled_at sched j t. 
+  Proof.
+    intros.
+    unfold is_idle; simpl; destruct (sched t) eqn:EQ.
+    - by right; exists s; auto; rewrite scheduled_at_def EQ.
+    - by left; auto.
+  Qed.
+  
+End ScheduleClass.
+
+(** * Automation *)
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq 
+    will be able to apply them automatically. *)
+Hint Resolve ideal_proc_model_is_a_uniprocessor_model
+     ideal_proc_model_ensures_ideal_progress
+     ideal_proc_model_provides_unit_service : basic_facts.
+
+(** We also provide tactics for case analysis on ideal processor state. *)
+
+(** The first tactic generates two subgoals: one with idle processor and 
+    the other with processor executing a job named JobName. *)
+Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
+  let Idle := fresh "Idle" in
+  let Sched := fresh "Sched_" JobName in
+  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
+
+(** The second tactic is similar to the first, but it additionally generates 
+    two equalities: [sched t = None] and [sched t = Some j]. *)
+Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
+  let Idle := fresh "Idle" in
+  let IdleEq := fresh "Eq" Idle in
+  let Sched := fresh "Sched_" JobName in 
+  let SchedEq := fresh "Eq" Sched in
+  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
+  [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
+  | move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
+
+(** * Incremental Service in Ideal Schedule *)
+(** In the following section we prove a few facts about service in ideal schedeule. *)
+(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
+Section IncrementalService.
+
+  (** Consider any job type, ... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+  Variable sched : schedule (ideal.processor_state Job).  
+
+  (** As a base case, we prove that if a job j receives service in
+      some time interval [t1,t2), then there exists a time instant t
+      ∈ [t1,t2) such that j is scheduled at time t and t is the first
+      instant where j receives service. *)
+  Lemma positive_service_during:
+    forall j t1 t2,
+      0 < service_during sched j t1 t2 -> 
+      exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.
+  Proof.
+    intros j t1 t2 SERV.
+    have LE: t1 <= t2.
+    { rewrite leqNgt; apply/negP; intros CONTR.
+        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
+    }
+    destruct (scheduled_at sched j t1) eqn:SCHED.
+    { exists t1; repeat split; try done.
+      - apply/andP; split; first by done.
+        rewrite ltnNge; apply/negP; intros CONTR.
+          by move: SERV; rewrite/service_during big_geq.
+      - by rewrite /service_during big_geq.                
+    }  
+    { apply negbT in SCHED.
+      move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]].
+      rewrite lt0b in SCHEDt.
+      rewrite mem_iota subnKC in IN; last by done.
+      move: IN => /andP [IN1 IN2].
+      move: (exists_first_intermediate_point
+               ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A.
+      feed A; first by rewrite scheduled_at_def/=.
+      move: A => [x [/andP [T1 T4] [T2 T3]]].
+      exists x; repeat split; try done.
+      - apply/andP; split; first by apply ltnW.
+          by apply leq_ltn_trans with t. 
+      - apply/eqP; rewrite big_nat_cond big1 //.
+        move => y /andP [T5 _].
+          by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
+    }
+  Qed.
+
+  (** Next, we prove that if in some time interval [t1,t2) a job j
+     receives k units of service, then there exists a time instant t ∈
+     [t1,t2) such that j is scheduled at time t and service of job j
+     within interval [t1,t) is equal to k. *)
+  Lemma incremental_service_during:
+    forall j t1 t2 k,
+      service_during sched j t1 t2 > k ->
+      exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
+  Proof.
+    intros j t1 t2 k SERV.
+    have LE: t1 <= t2.
+    { rewrite leqNgt; apply/negP; intros CONTR.
+        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
+    }
+    induction k; first by apply positive_service_during in SERV.
+    feed IHk; first by apply ltn_trans with k.+1.
+    move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
+    have SERVk1: service_during sched j t1 t.+1 = k.+1.
+    { rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.
+      rewrite  SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.
+        by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.  
+    } 
+    move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.
+    { by apply/andP; split; first apply leq_trans with t. }
+    rewrite SERVk1 -addn1 leq_add2l; move => SERV.
+    destruct (scheduled_at sched j t.+1) eqn:SCHED.
+    - exists t.+1; repeat split; try done. apply/andP; split.
+      + apply leq_trans with t; by done. 
+      + rewrite ltnNge; apply/negP; intros CONTR.
+          by move: SERV; rewrite /service_during big_geq.
+    -  apply negbT in SCHED.
+       move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]].
+       rewrite lt0b in SCHEDx.
+       rewrite mem_iota subnKC in INx; last by done.
+       move: INx => /andP [INx1 INx2].
+       move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.
+       feed A; first by rewrite scheduled_at_def/=.
+       move: A => [y [/andP [T1 T4] [T2 T3]]].
+       exists y; repeat split; try done.
+       + apply/andP; split.
+         apply leq_trans with t; first by done. 
+         apply ltnW, ltn_trans with t.+1; by done.
+           by apply leq_ltn_trans with x. 
+       + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].
+         unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.
+         rewrite -{2}[k.+1]addn0 eqn_add2l.
+         rewrite big_nat_cond big1 //; move => z /andP [H5 _].
+           by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
+  Qed.
+
+End IncrementalService.
diff --git a/restructuring/analysis/basic_facts/sequential.v b/restructuring/analysis/facts/behavior/sequential.v
similarity index 100%
rename from restructuring/analysis/basic_facts/sequential.v
rename to restructuring/analysis/facts/behavior/sequential.v
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/facts/behavior/service.v
similarity index 79%
rename from restructuring/analysis/basic_facts/service.v
rename to restructuring/analysis/facts/behavior/service.v
index 543fcdf4b..77d36351f 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/facts/behavior/service.v
@@ -1,5 +1,6 @@
 Require Export rt.util.all.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.behavior.all.
+Require Export rt.restructuring.model.processor.platform_properties.
 
 From mathcomp Require Import ssrnat ssrbool fintype.
 
@@ -576,111 +577,3 @@ Section RelationToScheduled.
 
 End RelationToScheduled.
 
-Require Import rt.restructuring.model.processor.ideal.
-
-(** * Incremental Service in Ideal Schedule *)
-(** In the following section we prove a few facts about service in ideal schedeule. *)
-(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
-Section IncrementalService.
-
-  (** Consider any job type, ... *)
-  Context {Job : JobType}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
-
-  (** ... any arrival sequence, ... *)
-  Variable arr_seq : arrival_sequence Job.
-
-  (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).  
-
-  (** As a base case, we prove that if a job j receives service in
-      some time interval [t1,t2), then there exists a time instant t
-      ∈ [t1,t2) such that j is scheduled at time t and t is the first
-      instant where j receives service. *)
-  Lemma positive_service_during:
-    forall j t1 t2,
-      0 < service_during sched j t1 t2 -> 
-      exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.
-  Proof.
-    intros j t1 t2 SERV.
-    have LE: t1 <= t2.
-    { rewrite leqNgt; apply/negP; intros CONTR.
-        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
-    }
-    destruct (scheduled_at sched j t1) eqn:SCHED.
-    { exists t1; repeat split; try done.
-      - apply/andP; split; first by done.
-        rewrite ltnNge; apply/negP; intros CONTR.
-          by move: SERV; rewrite/service_during big_geq.
-      - by rewrite /service_during big_geq.                
-    }  
-    { apply negbT in SCHED.
-      move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]].
-      rewrite lt0b in SCHEDt.
-      rewrite mem_iota subnKC in IN; last by done.
-      move: IN => /andP [IN1 IN2].
-      move: (exists_first_intermediate_point
-               ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A.
-      feed A; first by rewrite scheduled_at_def/=.
-      move: A => [x [/andP [T1 T4] [T2 T3]]].
-      exists x; repeat split; try done.
-      - apply/andP; split; first by apply ltnW.
-          by apply leq_ltn_trans with t. 
-      - apply/eqP; rewrite big_nat_cond big1 //.
-        move => y /andP [T5 _].
-          by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
-    }
-  Qed.
-
-  (** Next, we prove that if in some time interval [t1,t2) a job j
-     receives k units of service, then there exists a time instant t ∈
-     [t1,t2) such that j is scheduled at time t and service of job j
-     within interval [t1,t) is equal to k. *)
-  Lemma incremental_service_during:
-    forall j t1 t2 k,
-      service_during sched j t1 t2 > k ->
-      exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
-  Proof.
-    intros j t1 t2 k SERV.
-    have LE: t1 <= t2.
-    { rewrite leqNgt; apply/negP; intros CONTR.
-        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
-    }
-    induction k; first by apply positive_service_during in SERV.
-    feed IHk; first by apply ltn_trans with k.+1.
-    move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
-    have SERVk1: service_during sched j t1 t.+1 = k.+1.
-    { rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.
-      rewrite  SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.
-        by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.  
-    } 
-    move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.
-    { by apply/andP; split; first apply leq_trans with t. }
-    rewrite SERVk1 -addn1 leq_add2l; move => SERV.
-    destruct (scheduled_at sched j t.+1) eqn:SCHED.
-    - exists t.+1; repeat split; try done. apply/andP; split.
-      + apply leq_trans with t; by done. 
-      + rewrite ltnNge; apply/negP; intros CONTR.
-          by move: SERV; rewrite /service_during big_geq.
-    -  apply negbT in SCHED.
-       move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]].
-       rewrite lt0b in SCHEDx.
-       rewrite mem_iota subnKC in INx; last by done.
-       move: INx => /andP [INx1 INx2].
-       move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.
-       feed A; first by rewrite scheduled_at_def/=.
-       move: A => [y [/andP [T1 T4] [T2 T3]]].
-       exists y; repeat split; try done.
-       + apply/andP; split.
-         apply leq_trans with t; first by done. 
-         apply ltnW, ltn_trans with t.+1; by done.
-           by apply leq_ltn_trans with x. 
-       + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].
-         unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.
-         rewrite -{2}[k.+1]addn0 eqn_add2l.
-         rewrite big_nat_cond big1 //; move => z /andP [H5 _].
-           by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
-  Qed.
-
-End IncrementalService.
\ No newline at end of file
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/facts/behavior/service_of_jobs.v
similarity index 98%
rename from restructuring/analysis/basic_facts/service_of_jobs.v
rename to restructuring/analysis/facts/behavior/service_of_jobs.v
index 2d10fa54b..706ff2a14 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/facts/behavior/service_of_jobs.v
@@ -1,7 +1,7 @@
 Require Export rt.restructuring.model.aggregate.workload.
 Require Export rt.restructuring.model.aggregate.service_of_jobs.
-Require Export rt.restructuring.analysis.basic_facts.completion.
-
+Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
 Require Import rt.restructuring.model.processor.ideal.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
@@ -371,4 +371,4 @@ Section IdealModelLemmas.
 
   End WorkloadServiceAndCompletion. 
 
-End IdealModelLemmas.
\ No newline at end of file
+End IdealModelLemmas.
diff --git a/restructuring/analysis/basic_facts/task_arrivals.v b/restructuring/analysis/facts/behavior/task_arrivals.v
similarity index 100%
rename from restructuring/analysis/basic_facts/task_arrivals.v
rename to restructuring/analysis/facts/behavior/task_arrivals.v
diff --git a/restructuring/analysis/basic_facts/workload.v b/restructuring/analysis/facts/behavior/workload.v
similarity index 94%
rename from restructuring/analysis/basic_facts/workload.v
rename to restructuring/analysis/facts/behavior/workload.v
index 942bd6582..f8286ab2b 100644
--- a/restructuring/analysis/basic_facts/workload.v
+++ b/restructuring/analysis/facts/behavior/workload.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.facts.behavior.arrivals.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval.v
similarity index 99%
rename from restructuring/analysis/facts/busy_interval_exists.v
rename to restructuring/analysis/facts/busy_interval.v
index d97ca3841..739f2f492 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval.v
@@ -1,7 +1,7 @@
 Require Export rt.restructuring.analysis.definitions.job_properties.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.concepts.priority_inversion.
+Require Export rt.restructuring.analysis.facts.behavior.all.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/carry_in.v
similarity index 99%
rename from restructuring/analysis/facts/no_carry_in_exists.v
rename to restructuring/analysis/facts/carry_in.v
index 26c4bdaf9..2b036253e 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/carry_in.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.definitions.no_carry_in.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
+Require Export rt.restructuring.analysis.definitions.carry_in.
+Require Export rt.restructuring.analysis.facts.busy_interval.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/facts/preemption/job/limited.v
similarity index 99%
rename from restructuring/analysis/basic_facts/preemption/job/limited.v
rename to restructuring/analysis/facts/preemption/job/limited.v
index 392482c93..909f35c5c 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/facts/preemption/job/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
 Require Export rt.restructuring.model.schedule.limited_preemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/facts/preemption/job/nonpreemptive.v
similarity index 98%
rename from restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
rename to restructuring/analysis/facts/preemption/job/nonpreemptive.v
index efa8ad2f5..8ac8a8278 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/job/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
 Require Export rt.restructuring.model.schedule.nonpreemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/facts/preemption/job/preemptive.v
similarity index 100%
rename from restructuring/analysis/basic_facts/preemption/job/preemptive.v
rename to restructuring/analysis/facts/preemption/job/preemptive.v
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
similarity index 90%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/floating.v
index 4a2d046f7..bba9d8127 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
@@ -1,7 +1,7 @@
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.facts.preemption.task.floating.
+Require Export rt.restructuring.analysis.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/facts/preemption/rtc_threshold/job_preemptable.v
similarity index 99%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 8ea77ec19..ef91d3329 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
 Require Export 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/facts/preemption/rtc_threshold/limited.v
similarity index 97%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/limited.v
index f515e6358..0d1606ed3 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.facts.preemption.task.limited.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
 
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 8875e0e6f..335c6df92 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
 
 Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
similarity index 94%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
index 25f5ab7fe..d8b601ffa 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -1,6 +1,6 @@
 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.
+Require Import rt.restructuring.analysis.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/task/floating.v b/restructuring/analysis/facts/preemption/task/floating.v
similarity index 98%
rename from restructuring/analysis/basic_facts/preemption/task/floating.v
rename to restructuring/analysis/facts/preemption/task/floating.v
index 286e8d2e2..28c39720c 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/facts/preemption/task/floating.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.facts.preemption.job.limited.
 
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/facts/preemption/task/limited.v
similarity index 98%
rename from restructuring/analysis/basic_facts/preemption/task/limited.v
rename to restructuring/analysis/facts/preemption/task/limited.v
index fb3661327..a3d9a6862 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/facts/preemption/task/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.facts.preemption.job.limited.
 
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
rename to restructuring/analysis/facts/preemption/task/nonpreemptive.v
index 717d7cdde..fd3ba3548 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
 
 Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/facts/preemption/task/preemptive.v
similarity index 96%
rename from restructuring/analysis/basic_facts/preemption/task/preemptive.v
rename to restructuring/analysis/facts/preemption/task/preemptive.v
index 1a33d34bb..f04b0de7e 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/facts/preemption/task/preemptive.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
+Require Export rt.restructuring.analysis.facts.preemption.job.preemptive.
 
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion.v
similarity index 99%
rename from restructuring/analysis/facts/priority_inversion_is_bounded.v
rename to restructuring/analysis/facts/priority_inversion.v
index 93c89d784..16e07b07b 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion.v
@@ -1,6 +1,10 @@
 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.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Export rt.restructuring.model.schedule.work_conserving.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.concepts.busy_interval.
+Require Export rt.restructuring.analysis.facts.busy_interval.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/facts/rbf.v b/restructuring/analysis/facts/rbf.v
new file mode 100644
index 000000000..93dad5fd0
--- /dev/null
+++ b/restructuring/analysis/facts/rbf.v
@@ -0,0 +1,323 @@
+Require Export rt.restructuring.analysis.facts.behavior.workload.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.concepts.request_bound_function.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+
+(** * Facts about Request Bound Functions (RBFs) *)
+
+
+(** In this file, we prove some lemmas about request bound functions. *)
+
+
+(** ** RBF is a Bound on Workload *)
+
+(** First, we show that a task's RBF is indeed an upper bound on its
+    workload. *)
+Section ProofWorkloadBound.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** ... and any ideal uniprocessor schedule of this arrival sequence.*)
+  Variable sched : schedule (ideal.processor_state Job).
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority relation. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
+
+  (** Consider a task set ts... *)
+  Variable ts : list Task.
+
+  (** ...and let tsk be any task in ts. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_job_cost_le_task_cost :
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** Next, we assume that all jobs come from the task set. *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** Let max_arrivals be any arrival bound for taskset ts. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_rbf := total_request_bound_function ts.
+  Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
+
+  (** Next, we consider any job j of tsk. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_of_tsk : job_task j = tsk.
+
+  (** Next, we say that two jobs j1 and j2 are in relation
+      other_higher_eq_priority, iff j1 has higher or equal priority than j2 and
+      is produced by a different task. *)
+  Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
+
+  (** Next, we recall the notions of total workload of jobs... *)
+  Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).
+
+  (** ...notions of workload of higher or equal priority jobs... *)
+  Let total_hep_workload t1 t2 :=
+    workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
+
+  (** ... workload of other higher or equal priority jobs... *)
+  Let total_ohep_workload t1 t2 :=
+    workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
+
+  (** ... and the workload of jobs of the same task as job j. *)
+  Let task_workload t1 t2 :=
+    workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
+
+  (** In this section we prove that the workload of any jobs is
+       no larger than the request bound function. *)
+  Section WorkloadIsBoundedByRBF.
+
+    (** Consider any time t and any interval of length delta. *)
+    Variable t : instant.
+    Variable delta : instant.
+
+    (** First, we show that workload of task tsk is bounded by the number of
+        arrivals of the task times the cost of the task. *)
+    Lemma task_workload_le_num_of_arrivals_times_cost:
+      task_workload t (t + delta)
+      <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta).
+    Proof.
+      rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.
+      rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.
+      rewrite /same_task -H_job_of_tsk muln1.
+      apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+      rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
+        by apply H_job_cost_le_task_cost.
+    Qed.
+
+    (** As a corollary, we prove that workload of task is no larger the than
+        task request bound function. *)
+    Corollary task_workload_le_task_rbf:
+      task_workload t (t + delta) <= task_rbf delta.
+    Proof.
+      apply leq_trans with
+          (task_cost tsk *  number_of_task_arrivals arr_seq tsk t (t + delta));
+        first by apply task_workload_le_num_of_arrivals_times_cost.
+      rewrite leq_mul2l; apply/orP; right.
+      rewrite -{2}[delta](addKn t).
+        by apply H_is_arrival_bound; last rewrite leq_addr.
+    Qed.
+
+    (** Next, we prove that total workload of other tasks with higher-or-equal
+        priority is no larger than the total request bound function. *)
+    Lemma total_workload_le_total_rbf:
+      total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
+    Proof.
+      set l := arrivals_between arr_seq t (t + delta).
+      set hep := higher_eq_priority.
+      apply leq_trans with
+          (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
+            (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
+      { intros.
+        rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
+        rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
+        have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk && (job_task x != tsk)).
+        rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
+        rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
+        apply leq_sum; move => j0 /andP [IN0 HP0].
+        rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
+          by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
+      }
+      apply leq_sum_seq; intros tsk0 INtsk0 HP0.
+      apply leq_trans with
+          (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
+      { rewrite -sum1_size big_distrr /= big_filter.
+        rewrite /workload_of_jobs.
+        rewrite  muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
+        apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+          by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0.
+      }
+      { rewrite leq_mul2l; apply/orP; right.
+        rewrite -{2}[delta](addKn t).
+          by apply H_is_arrival_bound; last rewrite leq_addr.
+      }
+    Qed.
+
+    (** Next, we prove that total workload of tasks with higher-or-equal
+        priority is no larger than the total request bound function. *)
+    Lemma total_workload_le_total_rbf':
+      total_hep_workload t (t + delta) <= total_hep_rbf delta.
+    Proof.
+      set l := arrivals_between arr_seq t (t + delta).
+      set hep := higher_eq_priority.
+      apply leq_trans with
+          (n := \sum_(tsk' <- ts | hep tsk' tsk)
+                 (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
+      { rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
+        have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk).
+        rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
+        rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
+        apply leq_sum; move => j0 /andP [IN0 HP0].
+        rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
+          by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
+      }
+      apply leq_sum_seq; intros tsk0 INtsk0 HP0.
+      apply leq_trans with
+          (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
+      { rewrite -sum1_size big_distrr /= big_filter.
+        rewrite -/l /workload_of_jobs.
+        rewrite muln1.
+        apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+        rewrite -EQ.
+        apply H_job_cost_le_task_cost.
+          by apply in_arrivals_implies_arrived in IN0.
+      }
+      { rewrite leq_mul2l; apply/orP; right.
+        rewrite -{2}[delta](addKn t).
+          by apply H_is_arrival_bound; last rewrite leq_addr.
+      }
+    Qed.
+
+    (** Next, we prove that total workload of tasks is no larger than the total
+        request bound function. *)
+    Lemma total_workload_le_total_rbf'':
+      total_workload t (t + delta) <= total_rbf delta.
+    Proof.
+      set l := arrivals_between arr_seq t (t + delta).
+      apply leq_trans with
+          (n := \sum_(tsk' <- ts)
+                 (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
+      { rewrite /total_workload.
+        have EXCHANGE := exchange_big_dep predT.
+        rewrite EXCHANGE /=; clear EXCHANGE; last by done.
+        rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
+        apply leq_sum; move => j0 /andP [IN0 HP0].
+        rewrite big_mkcond (big_rem (job_task j0)) /=.
+        rewrite eq_refl; apply leq_addr.
+          by apply in_arrivals_implies_arrived in IN0;
+            apply H_all_jobs_from_taskset.
+      }
+      apply leq_sum_seq; intros tsk0 INtsk0 HP0.
+      apply leq_trans with
+          (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
+      { rewrite -sum1_size big_distrr /= big_filter.
+        rewrite -/l /workload_of_jobs.
+        rewrite muln1.
+        apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+        rewrite -EQ.
+        apply H_job_cost_le_task_cost.
+          by apply in_arrivals_implies_arrived in IN0.
+      }
+      { rewrite leq_mul2l; apply/orP; right.
+        rewrite -{2}[delta](addKn t).
+          by apply H_is_arrival_bound; last rewrite leq_addr.
+      }
+    Qed.
+
+  End WorkloadIsBoundedByRBF.
+
+End ProofWorkloadBound.
+
+(** ** RBF Properties *)
+(** In this section, we prove simple properties and identities of RBFs. *)
+Section RequestBoundFunctions.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent:
+    consistent_arrival_times arr_seq.
+
+  (** Let tsk be any task. *)
+  Variable tsk : Task.
+
+  (** Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts
+     [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
+     that equals 0 for the empty interval delta = 0. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
+  Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
+
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+
+  (** We prove that [task_rbf 0] is equal to 0. *)
+  Lemma task_rbf_0_zero:
+    task_rbf 0 = 0.
+  Proof.
+    rewrite /task_rbf /task_request_bound_function.
+    apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
+      by move: H_valid_arrival_curve => [T1 T2].
+  Qed.
+
+  (** We prove that task_rbf is monotone. *)
+  Lemma task_rbf_monotone:
+    monotone task_rbf leq.
+  Proof.
+    rewrite /monotone; intros ? ? LE.
+    rewrite /task_rbf /task_request_bound_function leq_mul2l.
+    apply/orP; right.
+      by move: H_valid_arrival_curve => [_ T]; apply T.
+  Qed.
+
+  (** Consider any job j of tsk. This guarantees that there exists at least one
+      job of task tsk. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_of_tsk : job_task j = tsk.
+
+  (** Then we prove that task_rbf 1 is greater than or equal to task cost. *)
+  Lemma task_rbf_1_ge_task_cost:
+    task_rbf 1 >= task_cost tsk.
+  Proof.
+    have ALT: forall n, n = 0 \/ n > 0
+      by clear; intros n; destruct n; [left | right].
+    specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
+    rewrite leqNgt; apply/negP; intros CONTR.
+    move: H_is_arrival_curve => ARRB.
+    specialize (ARRB (job_arrival j) (job_arrival j + 1)).
+    feed ARRB; first by rewrite leq_addr.
+    rewrite addKn in ARRB.
+    move: CONTR; rewrite /task_rbf /task_request_bound_function; move => CONTR.
+    move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move => /andP [_ CONTR].
+    move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move => /eqP CONTR.
+    move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move => /negP T; apply: T.
+    rewrite /number_of_task_arrivals -has_predT.
+    rewrite /task_arrivals_between.
+    apply/hasP; exists j; last by done.
+    rewrite /arrivals_between addn1 big_nat_recl; last by done.
+    rewrite big_geq ?cats0; last by done.
+    rewrite mem_filter.
+    apply/andP; split.
+    - by apply/eqP.
+    - move: H_j_arrives => [t ARR].
+      move: (ARR) => CONS.
+      apply H_arrival_times_are_consistent in CONS.
+      by rewrite CONS.
+  Qed.
+
+End RequestBoundFunctions.
diff --git a/restructuring/analysis/facts/readiness/basic.v b/restructuring/analysis/facts/readiness/basic.v
index c10e406bb..29eb01ede 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/restructuring/analysis/facts/readiness/basic.v
@@ -1,4 +1,4 @@
-Require Import rt.restructuring.analysis.basic_facts.completion.
+Require Import rt.restructuring.analysis.facts.behavior.completion.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/facts/transform/edf_opt.v
similarity index 99%
rename from restructuring/analysis/transform/facts/edf_opt.v
rename to restructuring/analysis/facts/transform/edf_opt.v
index 1be7c88f9..2536c0ca6 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/facts/transform/edf_opt.v
@@ -1,8 +1,8 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
 Require Export rt.restructuring.model.schedule.edf.
-Require Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.concepts.schedulability.
 Require Export rt.restructuring.analysis.transform.edf_trans.
-Require Export rt.restructuring.analysis.transform.facts.swaps.
+Require Export rt.restructuring.analysis.facts.transform.swaps.
 Require Export rt.restructuring.analysis.facts.readiness.basic.
 
 (** This file contains the main argument of the EDF optimality proof,
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/facts/transform/replace_at.v
similarity index 98%
rename from restructuring/analysis/transform/facts/replace_at.v
rename to restructuring/analysis/facts/transform/replace_at.v
index 5e22b2dfe..20a2fe23b 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/facts/transform/replace_at.v
@@ -1,4 +1,5 @@
 Require Export rt.restructuring.analysis.transform.swap.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
 
 (** In this file, we make a few simple observations about schedules with
     replacements. *)
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/facts/transform/swaps.v
similarity index 99%
rename from restructuring/analysis/transform/facts/swaps.v
rename to restructuring/analysis/facts/transform/swaps.v
index d59d6035c..7529e887a 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/facts/transform/swaps.v
@@ -1,4 +1,5 @@
-Require Export rt.restructuring.analysis.transform.facts.replace_at.
+Require Export rt.restructuring.analysis.facts.transform.replace_at.
+Require Export rt.restructuring.analysis.facts.behavior.deadlines.
 
 (** 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/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index 288b202d8..90e5ee75d 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
 
 (** This file provides an operation that transforms a finite prefix of
     a given schedule by applying a point-wise transformation to each
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 96dc092d2..443aa3987 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.behavior.all.
 
 (** This file defines simple allocation substitutions and a swapping operation
     as used for instance in the classic EDF optimality proof. *)
diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/results/edf/optimality.v
similarity index 98%
rename from restructuring/analysis/edf/optimality.v
rename to restructuring/results/edf/optimality.v
index 121c124f0..619b70358 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/results/edf/optimality.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.transform.facts.edf_opt.
+Require Export rt.restructuring.analysis.facts.transform.edf_opt.
 
 (** This file contains the theorem that states the famous EDF
     optimality result: if there is any way to meet all deadlines
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/results/edf/rta/bounded_nps.v
similarity index 99%
rename from restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
rename to restructuring/results/edf/rta/bounded_nps.v
index 6c59465f2..2b49af5b4 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/results/edf/rta/bounded_nps.v
@@ -1,6 +1,6 @@
-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 Export rt.restructuring.analysis.facts.priority_inversion.
+Require Export rt.restructuring.results.edf.rta.bounded_pi.
+Require Export rt.restructuring.analysis.facts.rbf.
 Require Import rt.restructuring.model.priority.edf.
 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/results/edf/rta/bounded_pi.v
similarity index 98%
rename from restructuring/analysis/edf/rta/response_time_bound.v
rename to restructuring/results/edf/rta/bounded_pi.v
index fda9c51b8..50b5a53ff 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/results/edf/rta/bounded_pi.v
@@ -1,10 +1,11 @@
 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 Export rt.restructuring.analysis.facts.priority_inversion.
+Require Export rt.restructuring.analysis.facts.carry_in.
+Require Export rt.restructuring.analysis.concepts.schedulability.
 Require Import rt.restructuring.model.priority.edf.
 Require Import rt.restructuring.model.task.absolute_deadline.
-Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
@@ -195,13 +196,13 @@ Section AbstractRTAforEDFwithArrivalCurves.
   (** We say that job j incurs interference at time t iff it cannot execute due to 
      a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *)
   Let interference (j : Job) (t : instant) :=
-    ideal_processor.interference sched EDF j t.
+    ideal_jlfp_rta.interference sched EDF j t.
 
   (** Instantiation of Interfering Workload *)
   (** The interfering workload, in turn, is defined as the sum of the priority inversion 
      function and interfering workload of jobs with higher or equal priority. *)
   Let interfering_workload (j : Job) (t : instant) :=
-    ideal_processor.interfering_workload arr_seq sched EDF j t.
+    ideal_jlfp_rta.interfering_workload arr_seq sched EDF j t.
 
   (** Finally, we define the interference bound function as the sum of the priority 
      interference bound and the higher-or-equal-priority workload. *)
@@ -242,7 +243,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
         }
       }
       { apply/negP;
-          rewrite /interference /ideal_processor.interference /is_priority_inversion
+          rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
                   /is_interference_from_another_hep_job 
                   HYP negb_or; apply/andP; split.
         - by rewrite Bool.negb_involutive /edf.EDF.
@@ -608,7 +609,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
       (** Next, consider any A from the search space (in abstract sense). *)
       Variable A : duration.
       Hypothesis H_A_is_in_abstract_search_space:
-        reduction_of_search_space.is_in_search_space tsk L total_interference_bound A.
+        search_space.is_in_search_space tsk L total_interference_bound A.
 
       (** We prove that A is also in the concrete search space. *)
       Lemma A_is_in_concrete_search_space:
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/results/edf/rta/floating_nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
rename to restructuring/results/edf/rta/floating_nonpreemptive.v
index 693cb2e7e..9ef9185f9 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/results/edf/rta/floating_nonpreemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Export rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
 Require Import rt.restructuring.model.priority.edf.
 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/results/edf/rta/fully_nonpreemptive.v
similarity index 96%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
rename to restructuring/results/edf/rta/fully_nonpreemptive.v
index e72bc1c60..551691c93 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/results/edf/rta/fully_nonpreemptive.v
@@ -1,6 +1,6 @@
-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.
+Require Export rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Import rt.restructuring.model.priority.edf.
 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/results/edf/rta/fully_preemptive.v
similarity index 96%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
rename to restructuring/results/edf/rta/fully_preemptive.v
index 07c5ebf84..e0c91fd41 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/results/edf/rta/fully_preemptive.v
@@ -1,6 +1,6 @@
-Require Import rt.restructuring.analysis.edf.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.
+Require Import rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Import rt.restructuring.model.priority.edf.
 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/results/edf/rta/limited_preemptive.v
similarity index 98%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
rename to restructuring/results/edf/rta/limited_preemptive.v
index 1b646474b..637feff56 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/results/edf/rta/limited_preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+Require Export rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
 Require Import rt.restructuring.model.priority.edf.
 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/results/fixed_priority/rta/bounded_nps.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
rename to restructuring/results/fixed_priority/rta/bounded_nps.v
index 6f39f334d..8ee2c9588 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/results/fixed_priority/rta/bounded_nps.v
@@ -1,7 +1,7 @@
-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 Export rt.restructuring.analysis.concepts.schedulability.
+Require Export rt.restructuring.analysis.concepts.request_bound_function.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_pi.
+Require Export rt.restructuring.analysis.facts.priority_inversion.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
@@ -139,7 +139,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Proof.
       intros j t ARR TSK.
       rewrite /max_length_of_priority_inversion /blocking_bound /FP_to_JLFP
-              /priority_inversion_is_bounded.max_length_of_priority_inversion.
+              /priority_inversion.max_length_of_priority_inversion.
       apply leq_trans with
           (\max_(j_lp <- arrivals_between arr_seq 0 t
                 | ~~ higher_eq_priority (job_task j_lp) tsk)
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/results/fixed_priority/rta/bounded_pi.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/response_time_bound.v
rename to restructuring/results/fixed_priority/rta/bounded_pi.v
index 3d2122480..b09566528 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/results/fixed_priority/rta/bounded_pi.v
@@ -1,6 +1,6 @@
 Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+Require Export rt.restructuring.analysis.facts.busy_interval.
+Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
@@ -164,14 +164,14 @@ Section AbstractRTAforFPwithArrivalCurves.
   (** We say that job j incurs interference at time t iff it cannot execute due to 
      a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *)
   Let interference (j : Job) (t : instant) :=
-    ideal_processor.interference sched hep_job j t.
+    ideal_jlfp_rta.interference sched hep_job j t.
 
   (** Instantiation of Interfering Workload *)
   (** The interfering workload, in turn, is defined as the sum of the
       priority inversion function and interfering workload of jobs
       with higher or equal priority. *)
   Let interfering_workload (j : Job) (t : instant) :=
-    ideal_processor.interfering_workload
+    ideal_jlfp_rta.interfering_workload
       arr_seq sched (@FP_to_JLFP Job Task H1 higher_eq_priority) j t.
   
   (** Finally, we define the interference bound function as the sum of the priority 
@@ -205,7 +205,7 @@ Section AbstractRTAforFPwithArrivalCurves.
             by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
                               eauto 2 using eqprop_to_eqbool.
       - move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
-        rewrite /interference /ideal_processor.interference /is_priority_inversion
+        rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
                   /is_interference_from_another_hep_job HYP2 negb_or.
          apply/andP; split.
          + rewrite Bool.negb_involutive; eauto 2.
@@ -317,7 +317,7 @@ Section AbstractRTAforFPwithArrivalCurves.
       (** Next, consider any A from the search space (in the abstract sence). *)
       Variable A : duration.
       Hypothesis H_A_is_in_abstract_search_space :
-        reduction_of_search_space.is_in_search_space tsk L total_interference_bound A. 
+        search_space.is_in_search_space tsk L total_interference_bound A. 
       
       (** We prove that A is also in the concrete search space. *)
       Lemma A_is_in_concrete_search_space:
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
rename to restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
index 6b9a836ac..fdd53ef23 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
similarity index 95%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
rename to restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
index 853e69903..67e67c4cd 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,6 +1,6 @@
-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.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/results/fixed_priority/rta/fully_preemptive.v
similarity index 95%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
rename to restructuring/results/fixed_priority/rta/fully_preemptive.v
index b67faa581..31d333f37 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_preemptive.v
@@ -1,6 +1,6 @@
-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.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/results/fixed_priority/rta/limited_preemptive.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
rename to restructuring/results/fixed_priority/rta/limited_preemptive.v
index 7ce643664..867d8f6f3 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/results/fixed_priority/rta/limited_preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-- 
GitLab