Added edf_wc.v

analysis/definitions/schedule_prefix.v

@@ -17,4 +17,17 @@ Section PrefixDefinition.
       t < horizon ->
       sched t = sched' t.
 
+  (** In other words, two schedules with a shared prefix are completely
+      interchangeable w.r.t. whether a job is scheduled (in the prefix). *)
+  Fact identical_prefix_scheduled_at:
+    forall sched sched' h,
+      identical_prefix sched sched' h ->
+      forall j t,
+        t < h ->
+        scheduled_at sched j t = scheduled_at sched' j t.
+  Proof.
+    move=> sched sched' h IDENT j t LT_h.
+    now rewrite /scheduled_at (IDENT t LT_h).
+  Qed.
+
 End PrefixDefinition.