diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index 6f93d73b4ad313911b7f85f0c52c933635e6a2e4..b61d05cbd1e5122d32e55ab00d84fb14935e9a88 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -137,7 +137,7 @@ Section ValidSchedule.
 
   (* ... and whether a job cannot be scheduled after it completes. *)
   Definition completed_jobs_dont_execute :=
-    forall j t, service sched j t <= job_cost j.
+    forall j t, scheduled_at sched j t -> service sched j t < job_cost j.
 
   (* We say that the schedule is valid iff
      - jobs come from some arrival sequence