Concrete arrival sequence

Added definitions and facts about the concrete arrival sequence, used in Poet to generate assumption-less certificates

model/task/arrival/curves.v

@@ -64,11 +64,10 @@ Section ArrivalCurves.
     Definition valid_arrival_curve (num_arrivals : duration -> nat) :=
       num_arrivals 0 = 0 /\
       monotone leq num_arrivals.
-                                           
-    (** Similarly, we say that [max_arrivals] is an upper arrival
-        bound for task [tsk] iff, for any interval <<[t1, t2)>>,
-        [max_arrivals (t2 - t1)] bounds the number of jobs of [tsk]
-        that arrive in that interval. *)
+
+    (** We say that [max_arrivals] is an upper arrival bound for task [tsk]
+        iff, for any interval <<[t1, t2)>>, [max_arrivals (t2 - t1)] bounds the
+        number of jobs of [tsk] that arrive in that interval. *)
     Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration -> nat) :=
       forall (t1 t2 : instant),
         t1 <= t2 ->