Concrete arrival sequence

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

implementation/definitions/maximal_arrival_sequence.v

@@ -33,11 +33,7 @@ Section MaximalArrivalSequence.
     (** Let [tsk] be any task. *)
     Variable tsk : Task.
     
-    (** First, we define a function that, given a sequence [xs], keeps
-        only the last [n] elements. *)
-    Definition suffix (xs : seq nat) (n : nat) := drop (size xs - n) xs.
-    
-    (** Next, we introduce a function that computes the sum of the suffix of length [n]. *) 
+    (** First, we introduce a function that computes the sum of the suffix of length [n]. *) 
     Definition suffix_sum xs n :=
       \sum_(size xs - n <= t < size xs) nth 0 xs t.