diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index a92e599ebd253c63b1267a91b52a297e1865e7e5..1c048c5cad778edd593f8217e6be8f302044d4f0 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -139,7 +139,8 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Let bound_on_total_hep_workload_changes_at :=
     bound_on_total_hep_workload_changes_at ts tsk.
   Let response_time_bounded_by := task_response_time_bound arr_seq sched.
-  
+  Let is_in_search_space := is_in_search_space ts tsk.
+                         
   (** We also define a bound for the priority inversion caused by jobs with lower priority. *)
   Definition blocking_bound :=
     \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
@@ -257,16 +258,13 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Hypothesis H_L_positive : L > 0.
     Hypothesis H_fixed_point : L = total_rbf L.
     
-    (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-    Let is_in_search_space A :=
-      (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
-    
-    (** Consider any value R, and assume that for any given arrival offset  A in the search space,
-         there is a solution of the response-time bound recurrence which is bounded by R. *)
+    (** Consider any value [R], and assume that for any given arrival
+        offset [A] in the search space, there is a solution of the
+        response-time bound recurrence which is bounded by [R]. *)
     Variable R : duration.
     Hypothesis H_R_is_maximum:
       forall (A : duration),
-        is_in_search_space A -> 
+        is_in_search_space L A -> 
         exists (F : duration),
           A + F = blocking_bound
                   + (task_rbf (A + ε) - (task_cost tsk - task_run_to_completion_threshold tsk))
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index db70e08a234b147c6e5c8d03f164a21e47652e07..b79368c00a5f663b94549adc99e758deba275a05 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -171,7 +171,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
   
   (** 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) :=
+  Definition is_in_search_space (A : duration) :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
   
   (** Let R be a value that upper-bounds the solution of each response-time recurrence, 
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index c6cb739630af13a6e27e98ab52a23eb37d818d1a..b0b3bd0d3bd2b3259cd4f37cd532fb871aefb328 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -123,13 +123,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts tsk.  
-
-  Let is_in_search_space (A : duration) :=
-    (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+  Let is_in_search_space := is_in_search_space ts tsk L.
   
   (** Consider any value R, and assume that for any given arrival offset A in the search space,
       there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -164,4 +158,4 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
     }
   Qed.
 
-End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
\ No newline at end of file
+End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 85de469f6c113a5b6fa2a753a691fc537286c2a3..4d5521e510d99c6d30def69d8fb6eeb389c0f4b3 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -114,13 +114,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   (** ** Response-Time Bound *)
     
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts tsk.
-
-  Let is_in_search_space A :=
-    (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+  Let is_in_search_space := is_in_search_space ts tsk L.
   
   (** Consider any value R, and assume that for any given arrival offset A in the search space,
       there is a solution of the response-time bound recurrence which is bounded by R. *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index faaac1592c0657644a2ff18055121d302af0ddd1..4e706669e3735ae1358f02dc30663bdc5bfa24ba 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -105,14 +105,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
 
   (** ** Response-Time Bound *)
   
-  (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-      
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts tsk.
-
-  Let is_in_search_space A :=
-    (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+  (** To reduce the time complexity of the analysis, recall the notion of search space. *)      
+  Let is_in_search_space := is_in_search_space ts tsk L.
   
   (** Consider any value R, and assume that for any given arrival offset A in the search space,
       there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -124,8 +118,10 @@ 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 non-preemptive segments
-      to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
+  (** 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. *)
 
   Let response_time_bounded_by := task_response_time_bound arr_seq sched.
 
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index f0a67d2d0000b5e1d0b84e04f8619cf3beacac90..dca7b119fdc374d65903f264a827812b01900393 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -123,13 +123,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-  
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts tsk.
-  
-  Let is_in_search_space A :=
-    (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A). 
+  Let is_in_search_space := is_in_search_space ts tsk L.
   
   (** Consider any value R, and assume that for any given arrival offset A in the search space,
      there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -180,4 +174,4 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     }
   Qed.
       
-End RTAforFixedPreemptionPointsModelwithArrivalCurves.
\ No newline at end of file
+End RTAforFixedPreemptionPointsModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 325b493d5ced18e733f7e071909b91ef037af23f..88fb239df8cf165a9daab320cbc4c14ac83657a0 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -218,7 +218,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
 
     (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-    Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+    Let is_in_search_space := is_in_search_space tsk L.
     
     (** Next, consider any value R, and assume that for any given arrival offset A from the search 
        space there is a solution of the response-time bound recurrence that is bounded by R. *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 5f9f41962e8e2c359be64c7cb79962cc4291d6f4..fa895bdf33b4d5a1d8284d9d8f5cf913576cc3c0 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -144,7 +144,7 @@ Section AbstractRTAforFPwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space.
      Intuitively, this corresponds to all "interesting" arrival offsets that the job under
      analysis might have with regard to the beginning of its busy-window. *)
-  Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  Definition is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
 
   (** Let R be a value that upper-bounds the solution of each response-time recurrence, 
      i.e., for any relative arrival time A in the search space, there exists a corresponding 
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index ca36e3af9d53261433fcd9f7a762f78d704b1dbe..ae0faec39162e4e9fbf95d7fad32111be70f629a 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -126,7 +126,7 @@ Section RTAforFloatingModelwithArrivalCurves.
   (** ** Response-Time Bound *)
 
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  Let is_in_search_space := is_in_search_space tsk L.
   
   (** Next, consider any value R, and assume that for any given
       arrival A from search space there is a solution of the
@@ -159,4 +159,4 @@ Section RTAforFloatingModelwithArrivalCurves.
       by exists F; rewrite addn0; split.
   Qed.
 
-End RTAforFloatingModelwithArrivalCurves.
\ No newline at end of file
+End RTAforFloatingModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index a3b95d652b7cfd3e827472d4efa5231595666933..dad64281f9fbf159e9c46829d5e416dd27b1dc84 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -118,7 +118,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  Let is_in_search_space := is_in_search_space tsk L.
 
   (** Next, consider any value R, and assume that for any given arrival A from search space
       there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -156,4 +156,4 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     all: eauto 2 with basic_facts. 
   Qed.
 
-End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
\ No newline at end of file
+End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 8144eb552e3467dd1de288c926c395ef200e3e0f..ba0fed172ed11aaca1055825c376400bcf4f9846 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -111,7 +111,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  Let is_in_search_space := is_in_search_space tsk L.
   
   (** Next, consider any value R, and assume that for any given
        arrival A from search space there is a solution of the
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 37576d9c5211d6578251b316d7b41e203b029cef..e417801257d77a3e0ba55977f05dd2fcea2a2809 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -126,8 +126,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
-
+  Let is_in_search_space := is_in_search_space tsk L.
+  
   (** Next, consider any value R, and assume that for any given arrival A from search space
       there is a solution of the response-time bound recurrence which is bounded by R. *)    
   Variable R: nat.