# Library prosa.implementation.facts.job_constructor

In this file, we prove facts about the job-constructor function when used in
pair with the concrete arrival sequence.

Assume that an arrival curve based on a concrete prefix is given.

#[local] Existing Instance ConcreteMaxArrivals.

Consider a task set ts with non-duplicate tasks.

... and that each generated job is unique.

Next, for convenience, we define arr_seq as the concrete arrival
sequence used with the job constructor.

We start by proving that the arrival time of a job is consistent with its
positioning inside the arrival sequence.

Next, we show that the list of arrivals at any time t is unique ...

... and generalize the above result to arbitrary time intervals.

Finally, we observe that generate_jobs_at tsk n t indeed generates jobs
of task tsk that arrive at t