diff --git a/implementation/definitions/scheduler.v b/implementation/definitions/scheduler.v
index 051c2ecc4c2bbaa918db466cc6475761838758b8..10b33292dbca53a060c0d5483fbb1fd7333ab0b0 100644
--- a/implementation/definitions/scheduler.v
+++ b/implementation/definitions/scheduler.v
@@ -22,9 +22,6 @@ Section UniprocessorSchedule.
 
     Variable sched_prefix : schedule (ideal.processor_state Job).
 
-    Definition jobs_backlogged_at (t : instant): seq Job :=
-      [seq j <- arrivals_up_to arr_seq t | backlogged sched_prefix j t].
-
     Definition prev_job_nonpreemptive (t : instant) : bool:=
       match t with
       | 0 => false
@@ -40,7 +37,7 @@ Section UniprocessorSchedule.
       if prev_job_nonpreemptive t then
         sched_prefix t.-1
       else
-        supremum (hep_job_at t) (jobs_backlogged_at t).
+        supremum (hep_job_at t) (jobs_backlogged_at arr_seq sched_prefix t).
 
   End JobAllocation.
 
diff --git a/model/schedule/work_conserving.v b/model/schedule/work_conserving.v
index db3ec06addfeafeba1dd59f6afe91f87cdbada0a..41f23a3a5408baca553dbf8274b7984f1901e5a0 100644
--- a/model/schedule/work_conserving.v
+++ b/model/schedule/work_conserving.v
@@ -40,5 +40,11 @@ Section WorkConserving.
       backlogged sched j t ->
       exists j_other, scheduled_at sched j_other t.
 
+  (** Related to this, we define the set of all jobs that are backlogged at a
+      given time [t], i.e., the set of jobs that could be scheduled, and which
+      a work-conserving scheduler must hence consider. *)
+  Definition jobs_backlogged_at (t : instant): seq Job :=
+    [seq j <- arrivals_up_to arr_seq t | backlogged sched j t].
+
 End WorkConserving.