diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 137ac75a484ab76219d353987ea65275b404dc96..8e1a8db9e97be924ceb21becf47f0c2e20d88697 100644
--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -13,12 +13,16 @@ Section BusyIntervalJLFP.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.    
 
-  (** Consider any arrival sequence with consistent arrivals. *)
+  (** Consider any kind of processor state model. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.  
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).
+  (** ... and a schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
   
   (** Assume a given JLFP policy. *)
   Context `{JLFP_policy Job}. 
@@ -89,4 +93,4 @@ Section BusyIntervalJLFP.
 
   End DecidableQuietTime.
 
-End BusyIntervalJLFP.
\ No newline at end of file
+End BusyIntervalJLFP.