diff --git a/restructuring/results/edf/rta/bounded_nps.v b/restructuring/results/edf/rta/bounded_nps.v
index 2b49af5b437f2db3551f83deb7a347d2bc0e4577..b7247ad45ac67309976d2a6f31a9b2ad2b61db27 100644
--- a/restructuring/results/edf/rta/bounded_nps.v
+++ b/restructuring/results/edf/rta/bounded_nps.v
@@ -4,18 +4,18 @@ 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.
 
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
-(** * RTA for EDF-schedulers with Bounded Non-Preemprive Segments *)
+(** * RTA for EDF-schedulers with Bounded Non-Preemptive Segments *)
 
 (** In this section we instantiate the Abstract RTA for EDF-schedulers
     with Bounded Priority Inversion to EDF-schedulers for ideal
     uni-processor model of real-time tasks with arbitrary
-    arrival models _and_ bounded non-preemprive segments. *)
+    arrival models _and_ bounded non-preemptive segments. *)
 
 (** Recall that Abstract RTA for EDF-schedulers with Bounded Priority
     Inversion does not specify the cause of priority inversion. In
@@ -51,7 +51,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
   
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+  (** Next, consider any ideal uni-processor 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.
@@ -60,12 +60,12 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
-  (** In addition, we assume the existence of a function maping jobs
+  (** In addition, we assume the existence of a function mapping jobs
       to theirs preemption points ... *)
   Context `{JobPreemptable Job}.
 
   (** ... and assume that it defines a valid preemption
-     model with bounded nonpreemptive segments. *)
+     model with bounded non-preemptive segments. *)
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
     valid_model_with_bounded_nonpreemptive_segments
       arr_seq sched.
@@ -77,8 +77,8 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-  (** ... and the schedule respects the policy defined by thejob_preemptable 
-     function (i.e., jobs have bounded nonpreemptive segments). *)
+  (** ... and the schedule respects the policy defined by the [job_preemptable]
+     function (i.e., jobs have bounded non-preemptive segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
 
   (** Consider an arbitrary task set ts, ... *)
@@ -92,14 +92,14 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** 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
+     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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -108,18 +108,18 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     valid_preemption_model arr_seq sched.
 
   (** ...and a valid task run-to-completion threshold function. That is, 
-     [task_run_to_completion_threshold tsk] is (1) no bigger than tsk's 
-     cost, (2) for any job of task tsk job_run_to_completion_threshold 
+     [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s 
+     cost, (2) for any job of task [tsk] job_run_to_completion_threshold 
      is bounded by task_run_to_completion_threshold. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
 
-  (** We introduce as an abbreviation "rbf" for the task request bound function,
+  (** We introduce as an abbreviation [rbf] for the task request bound function,
      which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
   Let rbf := task_request_bound_function.
   
-  (** Next, we introduce task_rbf as an abbreviation for the task
-     request bound function of task tsk. *)
+  (** Next, we introduce [task_rbf] as an abbreviation for the task
+     request bound function of task [tsk]. *)
   Let task_rbf := rbf tsk.
   
   (** Using the sum of individual request bound functions, we define the request bound 
@@ -146,13 +146,13 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
      (task_max_nonpreemptive_segment tsk_o - ε).
   
   (** ** Priority inversion is bounded *)
-  (** In this section, we prove that a priority inversion for task tsk is bounded by 
-      the maximum length of nonpreemtive segments among the tasks with lower priority. *)
+  (** In this section, we prove that a priority inversion for task [tsk] is bounded by 
+      the maximum length of non-preemptive segments among the tasks with lower priority. *)
   Section PriorityInversionIsBounded.
 
     (** First, we prove that the maximum length of a priority
         inversion of job j is bounded by the maximum length of a
-        nonpreemptive section of a task with lower-priority task
+        non-preemptive section of a task with lower-priority task
         (i.e., the blocking term). *)
     Lemma priority_inversion_is_bounded_by_blocking:
       forall j t,
@@ -249,7 +249,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   
   (** ** Response-Time Bound *)
   (** In this section, we prove that the maximum among the solutions of the response-time 
-      bound recurrence is a response-time bound for tsk. *)
+      bound recurrence is a response-time bound for [tsk]. *)
   Section ResponseTimeBound.
 
     (** Let L be any positive fixed point of the busy interval recurrence. *)
diff --git a/restructuring/results/edf/rta/bounded_pi.v b/restructuring/results/edf/rta/bounded_pi.v
index 50b5a53ff680ad94164d1132a86473dad8189750..c3c946a6899defb0f6a2532f209e67f71da9aefc 100644
--- a/restructuring/results/edf/rta/bounded_pi.v
+++ b/restructuring/results/edf/rta/bounded_pi.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.task.absolute_deadline.
 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -94,14 +94,14 @@ Section AbstractRTAforEDFwithArrivalCurves.
   (** 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 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 
+  (** 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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -110,18 +110,18 @@ Section AbstractRTAforEDFwithArrivalCurves.
     valid_preemption_model arr_seq sched.
 
   (** ...and a valid task run-to-completion threshold function. That is, 
-     [task_run_to_completion_threshold tsk] is (1) no bigger than tsk's 
-     cost, (2) for any job of task tsk job_run_to_completion_threshold 
+     [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s 
+     cost, (2) for any job of task [tsk] job_run_to_completion_threshold 
      is bounded by task_run_to_completion_threshold. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
 
-  (** We introduce "rbf" as an abbreviation of the task request bound function,
+  (** We introduce [rbf] as an abbreviation of the task request bound function,
      which is defined as [task_cost(T) × max_arrivals(T,Δ)] for some task T. *)
   Let rbf  := task_request_bound_function.
   
-  (** Next, we introduce task_rbf as an abbreviation 
-     of the task request bound function of task tsk. *)
+  (** Next, we introduce [task_rbf] as an abbreviation 
+     of the task request bound function of task [tsk]. *)
   Let task_rbf := rbf tsk.
 
   (** Using the sum of individual request bound functions, we define the request bound 
@@ -133,8 +133,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Let number_of_task_arrivals := number_of_task_arrivals arr_seq.
 
   (** Assume that there exists a constant priority_inversion_bound that bounds 
-     the length of any priority inversion experienced by any job of tsk. 
-     Since we analyze only task tsk, we ignore the lengths of priority 
+     the length of any priority inversion experienced by any job of [tsk]. 
+     Since we analyze only task [tsk], we ignore the lengths of priority 
      inversions incurred by any other tasks. *)
   Variable priority_inversion_bound : duration.
   Hypothesis H_priority_inversion_is_bounded:
@@ -159,19 +159,19 @@ Section AbstractRTAforEDFwithArrivalCurves.
   (** In case of search space for EDF we ask whether [task_rbf A ≠ task_rbf (A + ε)]... *)
   Definition task_rbf_changes_at (A : duration) := task_rbf A != task_rbf (A + ε).
 
-  (** ...or there exists a task tsko from ts such that [tsko ≠ tsk] and 
+  (** ...or there exists a task [tsko] from ts such that [tsko ≠ tsk] and 
      [rbf(tsko, A + D tsk - D tsko) ≠ rbf(tsko, A + ε + D tsk - D tsko)].
      Note that we use a slightly uncommon notation [has (λ tsko ⇒ P tskₒ) ts] 
-     which can be interpreted as follows: task-set ts contains a task tsko such 
-     that a predicate P holds for tsko. *)
+     which can be interpreted as follows: task-set ts contains a task [tsko] such 
+     that a predicate [P] holds for [tsko]. *)
   Definition bound_on_total_hep_workload_changes_at A :=
     has (fun tsko =>
            (tsk != tsko)
              && (rbf tsko (A + D tsk - D tsko)
                      != rbf tsko ((A + ε) + D tsk - D tsko))) ts.
   
-  (** The final search space for EDF is a set of offsets that are less than L 
-     and where task_rbf or bound_on_total_hep_workload changes. *)
+  (** The final search space for EDF is a set of offsets that are less than [L] 
+     and where [task_rbf] or [bound_on_total_hep_workload] changes. *)
   Let is_in_search_space (A : duration) :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
   
@@ -214,7 +214,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Section FillingOutHypothesesOfAbstractRTATheorem.
 
     (** First, we prove that in the instantiation of interference and interfering workload, 
-       we really take into account everything that can interfere with tsk's jobs, and thus, 
+       we really take into account everything that can interfere with [tsk]'s jobs, and thus, 
        the scheduler satisfies the abstract notion of work conserving schedule. *)
     Lemma instantiated_i_and_w_are_coherent_with_schedule:
       work_conserving_ab tsk interference interfering_workload.
@@ -300,7 +300,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
           constructing a sequence of inequalities. *) 
       Section Inequalities.
 
-        (* Consider an arbitrary job j of tsk. *)
+        (* Consider an arbitrary 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.
@@ -408,7 +408,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
 
         (** Next we focus on one task [tsk_o ≠ tsk] and consider two cases. *)
         
-        (** Case 1: Δ ≤ A + ε + D tsk - D tsk_o. *)
+        (** Case 1: [Δ ≤ A + ε + D tsk - D tsk_o]. *)
         Section Case1.
 
           (** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
@@ -445,7 +445,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
 
         End Case1.
 
-        (** Case 2: A + ε + D tsk - D tsk_o ≤ Δ. *)
+        (** Case 2: [A + ε + D tsk - D tsk_o ≤ Δ]. *)
         Section Case2.
 
           (** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
@@ -561,8 +561,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
         task t, and the length of the interval to the maximum amount
         of interference.
 
-        However, in this module we analyze only one task -- tsk,
-        therefore it is “hardcoded” inside the interference bound
+        However, in this module we analyze only one task -- [tsk],
+        therefore it is “hard-coded” inside the interference bound
         function IBF. Therefore, in order for the IBF signature to
         match the required signature in module abstract_seq_RTA, we
         wrap the IBF function in a function that accepts, but simply
@@ -594,13 +594,13 @@ Section AbstractRTAforEDFwithArrivalCurves.
     (** Finally, we show that there exists a solution for the response-time recurrence. *)
     Section SolutionOfResponseTimeReccurenceExists.
 
-      (** Consider any job j of tsk. *)
+      (** Consider any job j of [tsk]. *)
       Variable j : Job.
       Hypothesis H_j_arrives : arrives_in arr_seq j.
       Hypothesis H_job_of_tsk : job_of_task tsk j.
       Hypothesis H_job_cost_positive : job_cost_positive j.
 
-      (** Given any job j of task tsk that arrives exactly A units after the beginning of 
+      (** Given any job j of task [tsk] that arrives exactly A units after the beginning of 
          the busy interval, the bound of the total interference incurred by j within an 
          interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF(A, Δ)]. *)
       Let total_interference_bound tsk (A Δ : duration) :=
@@ -675,7 +675,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
 
   (** ** Final Theorem *)
   (** Based on the properties established above, we apply the abstract analysis 
-     framework to infer that R is a response-time bound for tsk. *)
+     framework to infer that R is a response-time bound for [tsk]. *)
   Theorem uniprocessor_response_time_bound_edf:
     response_time_bounded_by tsk R.
   Proof.
diff --git a/restructuring/results/edf/rta/floating_nonpreemptive.v b/restructuring/results/edf/rta/floating_nonpreemptive.v
index 9ef9185f94efb4d192e5beec4c09d7ea5d998949..6bf11b5be61ef719567fc99024c483481d2ce70a 100644
--- a/restructuring/results/edf/rta/floating_nonpreemptive.v
+++ b/restructuring/results/edf/rta/floating_nonpreemptive.v
@@ -3,7 +3,7 @@ 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.
 
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -39,10 +39,10 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
-  (** Assume we have the model with floating nonpreemptive regions.
-      I.e., for each task only the length of the maximal nonpreemptive
+  (** Assume we have the model with floating non-preemptive regions.
+      I.e., for each task only the length of the maximal non-preemptive
       segment is known _and_ each job level is divided into a number
-      of nonpreemptive segments by inserting preemption points. *)
+      of non-preemptive segments by inserting preemption points. *)
   Context `{JobPreemptionPoints Job}
           `{TaskMaxNonpreemptiveSegment Task}.
   Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions:
@@ -59,18 +59,18 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** 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
+      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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
-  (** Next, consider any ideal uniprocessor schedule with limited
+  (** Next, consider any ideal uni-processor schedule with limited
       preemptions of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_jobs_come_from_arrival_sequence:
@@ -90,7 +90,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
   (** ... and the schedule respects the policy defined by the
-      job_preemptable function (i.e., jobs have bounded nonpreemptive
+      job_preemptable function (i.e., jobs have bounded non-preemptive
       segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
 
@@ -101,12 +101,12 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Let bound_on_total_hep_workload_changes_at :=
     bound_on_total_hep_workload_changes_at ts tsk.
   
-  (** We introduce the abbreviation "rbf" for the task request bound function,
+  (** We introduce the abbreviation [rbf] for the task request bound function,
        which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
   Let rbf := task_request_bound_function.
 
-  (** Next, we introduce task_rbf as an abbreviation
-      for the task request bound function of task tsk. *)
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
   Let task_rbf := rbf tsk.
 
   (** Using the sum of individual request bound functions, we define the request bound 
diff --git a/restructuring/results/edf/rta/fully_nonpreemptive.v b/restructuring/results/edf/rta/fully_nonpreemptive.v
index 551691c93f5a7287dc43ef4d8c98fa6efca5d10d..30bab00ec59598455cfee6a56650014d8df269e7 100644
--- a/restructuring/results/edf/rta/fully_nonpreemptive.v
+++ b/restructuring/results/edf/rta/fully_nonpreemptive.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreem
 Require Import rt.restructuring.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -50,14 +50,14 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** 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
+     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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -90,12 +90,12 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   Let bound_on_total_hep_workload_changes_at :=
     bound_on_total_hep_workload_changes_at ts tsk.
 
-  (** We introduce the abbreviation "rbf" for the task request bound function,
+  (** We introduce the abbreviation [rbf] for the task request bound function,
       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
   Let rbf := task_request_bound_function.
 
-  (** Next, we introduce task_rbf as an abbreviation
-      for the task request bound function of task tsk. *)
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
   Let task_rbf := rbf tsk.
 
   (** Using the sum of individual request bound functions, we define the request bound 
diff --git a/restructuring/results/edf/rta/fully_preemptive.v b/restructuring/results/edf/rta/fully_preemptive.v
index e0c91fd412a7621da72dcd7d27689eb2e18ce04e..e7cc3df8bb4689c0cab3b73283f9832e1a3c593d 100644
--- a/restructuring/results/edf/rta/fully_preemptive.v
+++ b/restructuring/results/edf/rta/fully_preemptive.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preempti
 Require Import rt.restructuring.model.priority.edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -50,14 +50,14 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** 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
+     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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -78,7 +78,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
   (** ... and the schedule respects the policy defined by the
-      job_preemptable function (i.e., jobs have bounded nonpreemptive
+      [job_preemptable] function (i.e., jobs have bounded non-preemptive
       segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
       
@@ -89,12 +89,12 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Let bound_on_total_hep_workload_changes_at :=
     bound_on_total_hep_workload_changes_at ts tsk.
 
-  (** We introduce the abbreviation "rbf" for the task request bound function,
+  (** We introduce the abbreviation [rbf] for the task request bound function,
       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
   Let rbf := task_request_bound_function.
 
-  (** Next, we introduce task_rbf as an abbreviation
-      for the task request bound function of task tsk. *)
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
   Let task_rbf := rbf tsk.
 
   (** Using the sum of individual request bound functions, we define the request bound 
@@ -126,7 +126,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
         A + F = task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
         F <= R.
 
-  (** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
+  (** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
       to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
   Theorem uniprocessor_response_time_bound_fully_preemptive_edf:
     response_time_bounded_by tsk R.
diff --git a/restructuring/results/edf/rta/limited_preemptive.v b/restructuring/results/edf/rta/limited_preemptive.v
index 637feff567571cfcd4834d0f08a524852edc0ac9..3892ec572b9c128bc36f81c3822bcbfd8ca6301b 100644
--- a/restructuring/results/edf/rta/limited_preemptive.v
+++ b/restructuring/results/edf/rta/limited_preemptive.v
@@ -3,7 +3,7 @@ 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.
 
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -13,7 +13,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
-(** * RTA for EDF-schedulers with Fixed Premption Points *)
+(** * RTA for EDF-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points. *)
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   
@@ -50,27 +50,27 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
   
   (** Next, we assume we have the model with fixed preemption points.
-     I.e., each task is divided into a number of nonpreemptive segments 
-     by inserting staticaly predefined preemption points. *)
+     I.e., each task is divided into a number of non-preemptive segments 
+     by inserting statically predefined preemption points. *)
   Context `{JobPreemptionPoints Job}.
   Context `{TaskPreemptionPoints Task}.
   Hypothesis H_valid_model_with_fixed_preemption_points:
     valid_fixed_preemption_points_model arr_seq ts.
 
   (** 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
+     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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
-  (** Next, consider any ideal uniprocessor schedule with limited
-      preemptionsof this arrival sequence ...  *)
+  (** Next, consider any ideal uni-processor schedule with limited
+      preemptions 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.
@@ -89,7 +89,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
   (** ... and the schedule respects the policy defined by the
-      job_preemptable function (i.e., jobs have bounded nonpreemptive
+      [job_preemptable] function (i.e., jobs have bounded non-preemptive
       segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
   
@@ -99,12 +99,12 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Let bound_on_total_hep_workload_changes_at :=
     bound_on_total_hep_workload_changes_at ts tsk.
   
-  (** We introduce the abbreviation "rbf" for the task request bound function,
+  (** We introduce the abbreviation [rbf] for the task request bound function,
      which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
   Let rbf := task_request_bound_function.
 
-  (** Next, we introduce task_rbf as an abbreviation
-     for the task request bound function of task tsk. *)
+  (** Next, we introduce [task_rbf] as an abbreviation
+     for the task request bound function of task [tsk]. *)
   Let task_rbf := rbf tsk.
 
   (** Using the sum of individual request bound functions, we define the request bound 
@@ -143,7 +143,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
                 + bound_on_total_hep_workload A (A + F) /\
         F + (task_last_nonpr_segment tsk - ε) <= R.
   
-  (** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
+  (** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
       to establish a response-time bound for the more concrete model of fixed preemption points.  *)
   Theorem uniprocessor_response_time_bound_edf_with_fixed_preemption_points:
     response_time_bounded_by tsk R.  
diff --git a/restructuring/results/fixed_priority/rta/bounded_nps.v b/restructuring/results/fixed_priority/rta/bounded_nps.v
index 8ee2c95889e242a26cf117c1be1c00b08383d7bc..0371282ea75983309bd097ac3e0e17e58086c70a 100644
--- a/restructuring/results/fixed_priority/rta/bounded_nps.v
+++ b/restructuring/results/fixed_priority/rta/bounded_nps.v
@@ -4,18 +4,18 @@ 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
-(** * RTA for FP-schedulers with Bounded Non-Preemprive Segments *)
+(** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
 
 (** In this section we instantiate the Abstract RTA for FP-schedulers
     with Bounded Priority Inversion to FP-schedulers for ideal
     uni-processor model of real-time tasks with arbitrary
-    arrival models _and_ bounded non-preemprive segments. *)
+    arrival models _and_ bounded non-preemptive segments. *)
 
 (** Recall that Abstract RTA for FP-schedulers with Bounded Priority
     Inversion does not specify the cause of priority inversion. In
@@ -41,7 +41,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+  (** Next, consider any ideal uni-processor 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.
@@ -50,12 +50,12 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
   
-  (** In addition, we assume the existence of a function maping jobs
+  (** In addition, we assume the existence of a function mapping jobs
       to theirs preemption points ... *)
   Context `{JobPreemptable Job}.
 
   (** ... and assume that it defines a valid preemption
-      model with bounded nonpreemptive segments. *)
+      model with bounded non-preemptive segments. *)
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
@@ -73,8 +73,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
-  (** ... and the schedule respects the policy defined by thejob_preemptable 
-     function (i.e., jobs have bounded nonpreemptive segments). *)
+  (** ... and the schedule respects the policy defined by the [job_preemptable]
+     function (i.e., jobs have bounded non-preemptive segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
   
   (** Consider an arbitrary task set ts, ... *)
@@ -88,14 +88,14 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
   
   (** 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
+     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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
   
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -104,8 +104,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     valid_preemption_model arr_seq sched.
 
   (** ...and a valid task run-to-completion threshold function. That is, 
-     [task_run_to_completion_threshold tsk] is (1) no bigger than tsk's 
-     cost, (2) for any job of task tsk job_run_to_completion_threshold 
+     [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s 
+     cost, (2) for any job of task [tsk] job_run_to_completion_threshold 
      is bounded by task_run_to_completion_threshold. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
@@ -124,12 +124,12 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
      (task_max_nonpreemptive_segment tsk_other - ε).
   
   (** ** Priority inversion is bounded *)
-  (** In this section, we prove that a priority inversion for task tsk is bounded by 
-      the maximum length of nonpreemtive segments among the tasks with lower priority. *)
+  (** In this section, we prove that a priority inversion for task [tsk] is bounded by 
+      the maximum length of non-preemptive segments among the tasks with lower priority. *)
   Section PriorityInversionIsBounded.
 
     (** First, we prove that the maximum length of a priority inversion of a job j is 
-       bounded by the maximum length of a nonpreemptive section of a task with 
+       bounded by the maximum length of a non-preemptive section of a task with 
        lower-priority task (i.e., the blocking term). *)
     Lemma priority_inversion_is_bounded_by_blocking:
       forall j t, 
@@ -209,7 +209,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
   (** ** Response-Time Bound *)
   (** In this section, we prove that the maximum among the solutions of the response-time 
-      bound recurrence is a response-time bound for tsk. *)
+      bound recurrence is a response-time bound for [tsk]. *)
   Section ResponseTimeBound.
 
     (** Let L be any positive fixed point of the busy interval recurrence. *)
diff --git a/restructuring/results/fixed_priority/rta/bounded_pi.v b/restructuring/results/fixed_priority/rta/bounded_pi.v
index b095665288bf4d0ac5158760c6c9c0452968155b..28b5752b0cc257d0762b4243d602e67bf6866c9d 100644
--- a/restructuring/results/fixed_priority/rta/bounded_pi.v
+++ b/restructuring/results/fixed_priority/rta/bounded_pi.v
@@ -3,7 +3,7 @@ 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -77,14 +77,14 @@ Section AbstractRTAforFPwithArrivalCurves.
   (** 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 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 
+  (** 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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
     
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -93,8 +93,8 @@ Section AbstractRTAforFPwithArrivalCurves.
     valid_preemption_model arr_seq sched.
 
   (** ...and a valid task run-to-completion threshold function. That is, 
-     [task_run_to_completion_threshold tsk] is (1) no bigger than tsk's 
-     cost, (2) for any job of task tsk job_run_to_completion_threshold 
+     [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s 
+     cost, (2) for any job of task [tsk] job_run_to_completion_threshold 
      is bounded by task_run_to_completion_threshold. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
@@ -115,22 +115,22 @@ Section AbstractRTAforFPwithArrivalCurves.
   Let job_backlogged_at := backlogged sched.
   Let response_time_bounded_by := task_response_time_bound arr_seq sched.
 
-  (** We introduce task_rbf as an abbreviation of the task request bound function,
+  (** We introduce [task_rbf] as an abbreviation of the task request bound function,
      which is defined as [task_cost(tsk) × max_arrivals(tsk,Δ)]. *)
   Let task_rbf := task_request_bound_function tsk.
 
   (** Using the sum of individual request bound functions, we define the request bound 
-     function of all tasks with higher-or-equal priority (with respect to tsk). *)
+     function of all tasks with higher-or-equal priority (with respect to [tsk]). *)
   Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
  
   (** Similarly, we define the request bound function of all tasks other 
-     than tsk with higher-or-equal priority (with respect to tsk). *)
+     than [tsk] with higher-or-equal priority (with respect to [tsk]). *)
   Let total_ohep_rbf :=
     total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
   
-  (** Assume that there eixsts a constant priority_inversion_bound that bounds 
-     the length of any priority inversion experienced by any job of tsk. 
-     Sinse we analyze only task tsk, we ignore the lengths of priority 
+  (** Assume that there exists a constant priority_inversion_bound that bounds 
+     the length of any priority inversion experienced by any job of [tsk]. 
+     Since we analyze only task [tsk], we ignore the lengths of priority 
      inversions incurred by any other tasks. *)
   Variable priority_inversion_bound : duration.
   Hypothesis H_priority_inversion_is_bounded:
@@ -183,7 +183,7 @@ Section AbstractRTAforFPwithArrivalCurves.
   Section FillingOutHypothesesOfAbstractRTATheorem.
 
     (** First, we prove that in the instantiation of interference and interfering workload, 
-       we really take into account everything that can interfere with tsk's jobs, and thus, 
+       we really take into account everything that can interfere with [tsk]'s jobs, and thus, 
        the scheduler satisfies the abstract notion of work conserving schedule. *) 
     Lemma instantiated_i_and_w_are_consistent_with_schedule:
       work_conserving_ab tsk interference interfering_workload.
@@ -256,7 +256,7 @@ Section AbstractRTAforFPwithArrivalCurves.
        and the length of the interval to the maximum amount of interference (for more details see 
        files limited.abstract_RTA.definitions and limited.abstract_RTA.abstract_seq_rta).
 
-       However, in this module we analyze only one task -- tsk, therefore it is “hardcoded” 
+       However, in this module we analyze only one task -- [tsk], therefore it is “hard-coded” 
        inside the interference bound function IBF. Moreover, in case of a model with fixed 
        priorities, interference that some job j incurs from higher-or-equal priority jobs does not
        depend on the relative arrival time of job j. Therefore, in order for the IBF signature to
@@ -300,21 +300,21 @@ Section AbstractRTAforFPwithArrivalCurves.
     Qed.
 
     (** Finally, we show that there exists a solution for the response-time recurrence. *)
-    Section SolutionOfResponseTimeReccurenceExists.
+    Section SolutionOfResponseTimeRecurrenceExists.
 
-      (** Consider any job j of tsk. *)
+      (** 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.
       Hypothesis H_job_cost_positive: job_cost_positive j.
 
-      (** Given any job j of task tsk that arrives exactly A units after the beginning of 
+      (** Given any job j of task [tsk] that arrives exactly A units after the beginning of 
          the busy interval, the bound of the total interference incurred by j within an 
          interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF Δ]. *)
       Let total_interference_bound tsk A Δ :=
         task_rbf (A + ε) - task_cost tsk + IBF Δ.
 
-      (** Next, consider any A from the search space (in the abstract sence). *)
+      (** Next, consider any A from the search space (in the abstract sense). *)
       Variable A : duration.
       Hypothesis H_A_is_in_abstract_search_space :
         search_space.is_in_search_space tsk L total_interference_bound A. 
@@ -353,13 +353,13 @@ Section AbstractRTAforFPwithArrivalCurves.
           by rewrite addnA [_ + priority_inversion_bound]addnC -!addnA.
       Qed.
 
-    End SolutionOfResponseTimeReccurenceExists.
+    End SolutionOfResponseTimeRecurrenceExists.
 
   End FillingOutHypothesesOfAbstractRTATheorem.
 
   (** ** Final Theorem *)
   (** Based on the properties established above, we apply the abstract analysis 
-     framework to infer that R is a response-time bound for tsk. *) 
+     framework to infer that [R] is a response-time bound for [tsk]. *) 
   Theorem uniprocessor_response_time_bound_fp:
     response_time_bounded_by tsk R.
   Proof.
diff --git a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
index fdd53ef23225271f26b7a7460a9cae0b641f257a..a7121e83089de8242538c540943dab690c75434c 100644
--- a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -2,7 +2,7 @@ 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -32,10 +32,10 @@ Section RTAforFloatingModelwithArrivalCurves.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
-  (** Assume we have the model with floating nonpreemptive regions. 
-      I.e., for each task only the length of the maximal nonpreemptive 
+  (** Assume we have the model with floating non-preemptive regions. 
+      I.e., for each task only the length of the maximal non-preemptive 
       segment is known _and_ each job level is divided into a number of
-      nonpreemptive segments by inserting preemption points. *)
+      non-preemptive segments by inserting preemption points. *)
   Context `{JobPreemptionPoints Job}
           `{TaskMaxNonpreemptiveSegment Task}.
   Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions:
@@ -51,18 +51,18 @@ Section RTAforFloatingModelwithArrivalCurves.
   Hypothesis H_job_cost_le_task_cost:
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
-  (** 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. *)
+  (** 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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
-  (** Next, consider any ideal uniprocessor schedule with limited preemptions of this arrival sequence ... *)
+  (** Next, consider any ideal uni-processor schedule with limited preemptions 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.
@@ -86,8 +86,8 @@ Section RTAforFloatingModelwithArrivalCurves.
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
-  (** ... and the schedule respects the policy defined by thejob_preemptable 
-     function (i.e., jobs have bounded nonpreemptive segments). *)
+  (** ... and the schedule respects the policy defined by the [job_preemptable] 
+     function (i.e., jobs have bounded non-preemptive segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
   
   (** Let's define some local names for clarity. *)
diff --git a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
index 67e67c4cd072dc7731b847f3e517548054d12871..8940d2cf42c2c7898b125ae5ef9aa9d99ac4f738 100644
--- a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -3,7 +3,7 @@ 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -42,14 +42,14 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** 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. *)
+      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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
diff --git a/restructuring/results/fixed_priority/rta/fully_preemptive.v b/restructuring/results/fixed_priority/rta/fully_preemptive.v
index 31d333f37bf211d2aa59ad076f9a31e8da2290ec..3f63abc7711a0341f6e3002dc0c367cdf29bf6fc 100644
--- a/restructuring/results/fixed_priority/rta/fully_preemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_preemptive.v
@@ -3,7 +3,7 @@ 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -42,14 +42,14 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** 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. *)
+      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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
@@ -75,8 +75,8 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
-  (** ... and the schedule respects the policy defined by thejob_preemptable 
-     function (i.e., jobs have bounded nonpreemptive segments). *)
+  (** ... and the schedule respects the policy defined by the [job_preemptable] 
+     function (i.e., jobs have bounded non-preemptive segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.  
 
   (** Let's define some local names for clarity. *)
@@ -104,7 +104,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
         A + F = task_rbf (A + ε) + total_ohep_rbf (A + F) /\
         F <= R.
 
-  (** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
+  (** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
        to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
   Theorem uniprocessor_response_time_bound_fully_preemptive_fp:
     response_time_bounded_by tsk R.
diff --git a/restructuring/results/fixed_priority/rta/limited_preemptive.v b/restructuring/results/fixed_priority/rta/limited_preemptive.v
index 867d8f6f3deb0604055c7c0cc6e0ddf624965474..b82100934df392b23b604cc92621423b8a6ee8d1 100644
--- a/restructuring/results/fixed_priority/rta/limited_preemptive.v
+++ b/restructuring/results/fixed_priority/rta/limited_preemptive.v
@@ -2,7 +2,7 @@ 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. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -13,7 +13,7 @@ Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
 
-(** * RTA for FP-schedulers with Fixed Premption Points *)
+(** * RTA for FP-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with fixed preemption points. *)
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
 
@@ -43,25 +43,25 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
 
   (** First, we assume we have the model with fixed preemption points.
-      I.e., each task is divided into a number of nonpreemptive segments 
-      by inserting staticaly predefined preemption points. *)
+      I.e., each task is divided into a number of non-preemptive segments 
+      by inserting statically predefined preemption points. *)
   Context `{JobPreemptionPoints Job}
           `{TaskPreemptionPoints Task}.
   Hypothesis H_valid_model_with_fixed_preemption_points:
     valid_fixed_preemption_points_model arr_seq ts.
 
-  (** 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. *)
+  (** 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_taskset_arrival_curve ts max_arrivals.
   Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
 
-  (** Let tsk be any task in ts that is to be analyzed. *)
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
-  (** Next, consider any ideal uniprocessor schedule  with limited preemptionsof this arrival sequence ... *)
+  (** Next, consider any ideal uni-processor schedule  with limited preemptions 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.
@@ -85,8 +85,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
-  (** ... and the schedule respects the policy defined by thejob_preemptable 
-     function (i.e., jobs have bounded nonpreemptive segments). *)
+  (** ... and the schedule respects the policy defined by the [job_preemptable]
+     function (i.e., jobs have bounded non-preemptive segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.  
 
   (** Let's define some local names for clarity. *)
@@ -121,7 +121,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
                 + total_ohep_rbf (A + F) /\
         F + (task_last_nonpr_segment tsk - ε) <= R.
         
-  (** Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
+  (** Now, we can reuse the results for the abstract model with bounded non-preemptive segments
      to establish a response-time bound for the more concrete model of fixed preemption points. *)
   Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
     response_time_bounded_by tsk R.