# Library prosa.analysis.definitions.completion_sequence

This module contains basic definitions and properties of job
completion sequences.
We begin by defining a job completion sequence.

# Notion of a Completion Sequence

Consider any kind of jobs with a cost
and any kind of processor state.

Consider any job arrival sequence.

Consider any schedule.

Definition completion_sequence : arrival_sequence Job :=

fun t ⇒ [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].

End CompletionSequence.

fun t ⇒ [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].

End CompletionSequence.