# Library prosa.implementation.facts.job_constructor

Require Export prosa.implementation.definitions.job_constructor.
In this file, we prove facts about the job-constructor function when used in pair with the concrete arrival sequence.
Section JobConstructor.
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.
Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.
First, we show that generate_jobs_at tsk n t generates n jobs ...
Lemma job_generation_valid_number :
∀ tsk n t,
tsk \in ts → size (generate_jobs_at tsk n t) = n.
... and that each generated job is unique.
Lemma generate_jobs_at_unique :
∀ tsk n t,
uniq (generate_jobs_at tsk n t).
Next, for convenience, we define arr_seq as the concrete arrival sequence used with the job constructor.
Let arr_seq := concrete_arrival_sequence generate_jobs_at ts.
We start by proving that the arrival time of a job is consistent with its positioning inside the arrival sequence.
Lemma job_arrival_consistent :
∀ j t,
j \in arr_seq t → job_arrival j = t.
Next, we show that the list of arrivals at any time t is unique ...
Lemma arrivals_at_unique :
∀ t,
uniq (arr_seq t).
... and generalize the above result to arbitrary time intervals.
Lemma arrivals_between_unique :
∀ t1 t2,
uniq (arrivals_between arr_seq t1 t2).
Finally, we observe that generate_jobs_at tsk n t indeed generates jobs of task tsk that arrive at t
Corollary job_generation_valid_jobs :
∀ tsk n t j,
j \in generate_jobs_at tsk n t →
job_task j = tsk
∧ job_arrival j = t
∧ job_cost j ≤ task_cost tsk.
End JobConstructor.