# Library prosa.analysis.facts.job_index

In this section, we prove some properties related to job_index.

Consider any type of tasks ...

... and any jobs associated with the tasks.

Consider any arrival sequence with consistent and non-duplicate arrivals, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Variable j1 j2 : Job.

Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.

Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.

Hypothesis H_same_task: job_task j1 = job_task j2.

Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.

Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.

Hypothesis H_same_task: job_task j1 = job_task j2.

In the next section, we prove some basic properties about jobs with equal indices.

To show that jobs j1 and j2 are equal, we'll perform case
analysis on the relation between their arrival times.
Jobs with equal indices have to be equal regardless of their
arrival times because of the way job_index is defined (i.e.,
jobs are first ordered according to their arrival times and ties are
broken arbitrarily due to which no two unequal jobs have the same
job_index).
In case job j2 arrives after or at the same time as j1 arrives, we
show that the jobs are equal.

And finally we show that irrespective of the relation between the arrival
of job j1 and j2, j1 must be equal to j2.

We show that jobs of a task are different if and only if they
have different indices.

We show that job_index j can be written as a sum of size (task_arrivals_before_job_arrival j)
and index j (task_arrivals_at arr_seq (job_task j) (job_arrival j)).

Lemma index_as_sum_size_and_index:

job_index arr_seq j1 =

size (task_arrivals_before_job_arrival arr_seq j1)

+ index j1 (task_arrivals_at_job_arrival arr_seq j1).

job_index arr_seq j1 =

size (task_arrivals_before_job_arrival arr_seq j1)

+ index j1 (task_arrivals_at_job_arrival arr_seq j1).

Given jobs j1 and j2 in arrivals_between_P arr_seq P t1 t2, the fact that
j2 arrives strictly before j1 implies that j2 also belongs in the sequence
arrivals_between_P arr_seq P t1 (job_arrival j1).

Lemma arrival_lt_implies_job_in_arrivals_between_P:

∀ (P : Job → bool) (t1 t2 : instant),

(j1 \in arrivals_between_P arr_seq P t1 t2) →

(j2 \in arrivals_between_P arr_seq P t1 t2) →

job_arrival j2 < job_arrival j1 →

j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).

∀ (P : Job → bool) (t1 t2 : instant),

(j1 \in arrivals_between_P arr_seq P t1 t2) →

(j2 \in arrivals_between_P arr_seq P t1 t2) →

job_arrival j2 < job_arrival j1 →

j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).

We show that jobs in the sequence arrivals_between_P are ordered by their arrival times, i.e.,
if index of a job j2 is greater than or equal to index of any other job j1 in the sequence,
then job_arrival j2 must be greater than or equal to job_arrival j1.

Lemma index_lte_implies_arrival_lte_P:

∀ (P : Job → bool) (t1 t2 : instant),

(j1 \in arrivals_between_P arr_seq P t1 t2) →

(j2 \in arrivals_between_P arr_seq P t1 t2) →

index j1 (arrivals_between_P arr_seq P t1 t2) ≤ index j2 (arrivals_between_P arr_seq P t1 t2) →

job_arrival j1 ≤ job_arrival j2.

∀ (P : Job → bool) (t1 t2 : instant),

(j1 \in arrivals_between_P arr_seq P t1 t2) →

(j2 \in arrivals_between_P arr_seq P t1 t2) →

index j1 (arrivals_between_P arr_seq P t1 t2) ≤ index j2 (arrivals_between_P arr_seq P t1 t2) →

job_arrival j1 ≤ job_arrival j2.

We observe that index of job j1 is same in the
sequences task_arrivals_up_to_job_arrival j1 and task_arrivals_up_to_job_arrival j2
provided j2 arrives after j1.

Lemma job_index_same_in_task_arrivals:

job_arrival j1 ≤ job_arrival j2 →

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2).

job_arrival j1 ≤ job_arrival j2 →

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2).

We show that the job_index of a job j1 is strictly less than
the size of task_arrivals_up_to_job_arrival arr_seq j1.

Lemma index_job_lt_size_task_arrivals_up_to_job:

job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

Finally, we show that a lower job index implies an earlier arrival time.

Lemma index_lte_implies_arrival_lte:

job_index arr_seq j2 ≤ job_index arr_seq j1 →

job_arrival j2 ≤ job_arrival j1.

job_index arr_seq j2 ≤ job_index arr_seq j1 →

job_arrival j2 ≤ job_arrival j1.

We show that if job j1 arrives earlier than job j2
then job_index arr_seq j1 is strictly less than job_index arr_seq j2.

Lemma earlier_arrival_implies_lower_index:

job_arrival j1 < job_arrival j2 →

job_index arr_seq j1 < job_index arr_seq j2.

job_arrival j1 < job_arrival j2 →

job_index arr_seq j1 < job_index arr_seq j2.

We prove a weaker version of the lemma index_job_lt_size_task_arrivals_up_to_job,
given that the job_index of j is positive.

Lemma job_index_minus_one_lt_size_task_arrivals_up_to:

job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

Since task_arrivals_up_to_job_arrival arr_seq j has at least the job
j in it, its size has to be positive.

Lemma positive_job_index_implies_positive_size_of_task_arrivals:

size (task_arrivals_up_to_job_arrival arr_seq j1) > 0.

End JobIndexLemmas.

size (task_arrivals_up_to_job_arrival arr_seq j1) > 0.

End JobIndexLemmas.

In this section, we prove a few basic properties of
function prev_job.

Consider any type of tasks ...

... and any jobs associated with the tasks.

Consider any unique arrival sequence with consistent arrivals ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and an arbitrary job with a positive job_index.

Variable j : Job.

Hypothesis H_arrives_in_arr_seq: arrives_in arr_seq j.

Hypothesis H_positive_job_index: job_index arr_seq j > 0.

Hypothesis H_arrives_in_arr_seq: arrives_in arr_seq j.

Hypothesis H_positive_job_index: job_index arr_seq j > 0.

We observe that the fact that job j is in the arrival sequence
implies that job prev_job j is in the arrival sequence.

Lemma prev_job_index:

index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.

index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.

Lemma prev_job_in_task_arrivals_up_to_j:

prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j.

prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j.

We observe that for any job j the arrival time of prev_job j is
strictly less than the arrival time of j in context of periodic tasks.

Lemma prev_job_index_j:

job_index arr_seq j > 0 →

job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1.

job_index arr_seq j > 0 →

job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1.

Lemma no_jobs_between_consecutive_jobs:

job_index arr_seq j > 0 →

task_arrivals_between arr_seq (job_task j)

(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::].

job_index arr_seq j > 0 →

task_arrivals_between arr_seq (job_task j)

(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::].