Added edf_wc.v

analysis/facts/transform/edf_wc.v

@@ -73,7 +73,7 @@ Section NonIdleSwapWorkConservationLemmas.
   (** ...and [j] is backlogged in [swap_sched] at instant [t] *)
   Hypothesis H_backlogged_j_t : backlogged swap_sched j t.
 
-  (** We first show that if [t] equals [t1] then swap_sched maintains work conservation.
+  (** We first show that if [t] equals [t1] then [swap_sched] maintains work conservation.
       That is, there exists some job that's scheduled in [swap_sched] at instant [t] *)
   Lemma non_idle_swap_maintains_work_conservation_t1 :
     work_conserving arr_seq sched ->
@@ -82,7 +82,7 @@ Section NonIdleSwapWorkConservationLemmas.
     move=> _ EQ; rewrite EQ; by exists j2; rewrite swap_job_scheduled_t1.
   Qed.
 
-  (** Similarly, if [t] equals [t2] then then swap_sched maintains work conservation. *)
+  (** Similarly, if [t] equals [t2] then then [swap_sched] maintains work conservation. *)
   Lemma non_idle_swap_maintains_work_conservation_t2 :
     work_conserving arr_seq sched ->
     t = t2 -> exists j_other, scheduled_at swap_sched j_other t.
@@ -90,7 +90,7 @@ Section NonIdleSwapWorkConservationLemmas.
     move=> _ EQ; rewrite EQ; by exists j1; rewrite swap_job_scheduled_t2.
   Qed.
 
-  (** If [t] is less than or equal to [t1] then then then swap_sched maintains work conservation. *)
+  (** If [t] is less than or equal to [t1] then then then [swap_sched] maintains work conservation. *)
   Lemma non_idle_swap_maintains_work_conservation_LEQ_t1 :
     work_conserving arr_seq sched ->
     t <= t1 -> exists j_other, scheduled_at swap_sched j_other t.
@@ -109,7 +109,7 @@ Section NonIdleSwapWorkConservationLemmas.
     exists j_other; by rewrite  (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
   Qed.
 
-  (** Similarly, if [t] is greater than [t2] then then then swap_sched maintains work conservation. *)
+  (** Similarly, if [t] is greater than [t2] then then then [swap_sched] maintains work conservation. *)
   Lemma non_idle_swap_maintains_work_conservation_GT_t2 :
     work_conserving arr_seq sched ->
     t2 < t -> exists j_other, scheduled_at swap_sched j_other t.