Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
(** In this section, we prove some properties related to [job_index]. *) Section JobIndexLemmas. (** Consider any type of tasks ... *) Context {Task : TaskType}. (** ... and any jobs associated with the tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq. Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq. (** ... and any two jobs [j1] and [j2] from this arrival sequence that stem from the same task. *) 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. (** In the next section, we prove some basic properties about jobs with equal indices. *) Section EqualJobIndex. (** Assume that the jobs [j1] and [j2] have the same [job_index] in the arrival sequence. *) Hypothesis H_equal_index: job_index arr_seq j1 = job_index arr_seq j2. (** 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. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2

job_arrival j1 <= job_arrival j2 -> j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2

job_arrival j1 <= job_arrival j2 -> j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
ARR_LT: job_arrival j1 <= job_arrival j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
ARR_LT: job_arrival j1 <= job_arrival j2
IND: job_index arr_seq j1 = job_index arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
ARR_LT: prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2)
IND: job_index arr_seq j1 = job_index arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

index j1 (task_arrivals_up_to_job_arrival arr_seq j2) = index j2 (task_arrivals_up_to_job_arrival arr_seq j2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

index j1 (task_arrivals_up_to_job_arrival arr_seq j2) = index j2 (task_arrivals_up_to_job_arrival arr_seq j2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

j1 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

j1 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

j1 \in task_arrivals_up_to_job_arrival arr_seq j1 \/ j1 \in xs
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

j2 \in task_arrivals_up_to_job_arrival arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs = task_arrivals_up_to_job_arrival arr_seq j2

j2 \in task_arrivals_up_to_job_arrival arr_seq j2
now apply arrives_in_task_arrivals_up_to. Qed. (** And similarly if [j1] arrives after [j2], we show that the jobs are equal. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2

job_arrival j2 < job_arrival j1 -> j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2

job_arrival j2 < job_arrival j1 -> j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
LT: job_arrival j2 < job_arrival j1

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
LT: job_arrival j2 < job_arrival j1
IND: job_index arr_seq j1 = job_index arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
LT: prefix_of (task_arrivals_up_to_job_arrival arr_seq j2) (task_arrivals_up_to_job_arrival arr_seq j1)
IND: job_index arr_seq j1 = job_index arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j2 (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j2 (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

j1 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

j1 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

j2 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

j2 \in task_arrivals_up_to_job_arrival arr_seq j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index, IND: job_index arr_seq j1 = job_index arr_seq j2
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j2 ++ xs = task_arrivals_up_to_job_arrival arr_seq j1

j2 \in task_arrivals_up_to_job_arrival arr_seq j2 \/ j2 \in xs
now left; apply arrives_in_task_arrivals_up_to => //. Qed. (** And finally we show that irrespective of the relation between the arrival of job [j1] and [j2], [j1] must be equal to [j2]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
LT: job_arrival j1 < job_arrival j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
GT: job_arrival j2 < job_arrival j1
j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
EQ: job_arrival j1 = job_arrival j2
j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
LT: job_arrival j1 < job_arrival j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
GT: job_arrival j2 < job_arrival j1
j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
EQ: job_arrival j1 = job_arrival j2
j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
GT: job_arrival j2 < job_arrival j1

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
EQ: job_arrival j1 = job_arrival j2
j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
GT: job_arrival j2 < job_arrival j1

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
EQ: job_arrival j1 = job_arrival j2
j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
EQ: job_arrival j1 = job_arrival j2

j1 = j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
H_equal_index: job_index arr_seq j1 = job_index arr_seq j2
EQ: job_arrival j1 = job_arrival j2

j1 = j2
now apply case_arrival_lte_implies_equal_job; lia. Qed. End EqualJobIndex. (** We show that jobs of a task are different if and only if they have different indices. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

j1 <> j2 <-> job_index arr_seq j1 <> job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

j1 <> j2 <-> job_index arr_seq j1 <> job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

j1 <> j2 -> job_index arr_seq j1 <> job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

j1 <> j2 -> job_index arr_seq j1 <> job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
NEQJ: j1 <> j2
EQ: job_index arr_seq j1 = job_index arr_seq j2

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
NEQ: job_index arr_seq j1 <> job_index arr_seq j2
EQ: j1 = j2

False
now move: EQ NEQ => ->. Qed. (** 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))]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 = size (task_arrivals_before_job_arrival arr_seq j1) + index j1 (task_arrivals_at_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 = size (task_arrivals_before_job_arrival arr_seq j1) + index j1 (task_arrivals_at_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

index j1 (task_arrivals_before_job_arrival arr_seq j1 ++ task_arrivals_at_job_arrival arr_seq j1) = size (task_arrivals_before_job_arrival arr_seq j1) + index j1 (task_arrivals_at arr_seq (job_task j1) (job_arrival j1))
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

(j1 \in task_arrivals_before_job_arrival arr_seq j1) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
T: (j1 \in task_arrivals_before_job_arrival arr_seq j1) = true

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
SM_TSK: job_task j1 = job_task j1
JB_IN_ARR: j1 \in arrivals_between arr_seq 0 (job_arrival j1)

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
SM_TSK: job_task j1 = job_task j1
ind: nat
JB_IN: j1 \in arrivals_at arr_seq ind
IND_INTR: 0 <= ind < job_arrival j1

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
SM_TSK: job_task j1 = job_task j1
ind: nat
JB_IN: j1 \in arrivals_at arr_seq ind
IND_INTR: 0 <= ind < ind

False
now lia. Qed. (** 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)]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

forall (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)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

forall (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)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
J1_IN: j1 \in arrivals_between_P arr_seq P t1 t2
J2_IN: j2 \in arrivals_between_P arr_seq P t1 t2
ARR_LT: job_arrival j2 < job_arrival j1

j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
J1_IN: j1 \in arrivals_between_P arr_seq P t1 t2
ARR_LT: job_arrival j2 < job_arrival j1
PJ2: P j2
J2ARR: j2 \in arrivals_between arr_seq t1 t2

j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
J1_IN: j1 \in arrivals_between_P arr_seq P t1 t2
ARR_LT: job_arrival j2 < job_arrival j1
PJ2: P j2
J2ARR: j2 \in arrivals_between arr_seq t1 t2

j2 \in arrivals_between arr_seq t1 (job_arrival j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
J1_IN: j1 \in arrivals_between_P arr_seq P t1 t2
ARR_LT: job_arrival j2 < job_arrival j1
PJ2: P j2
i: nat
J2_IN: j2 \in arrivals_at arr_seq i
INEQ: t1 <= i < t2

j2 \in arrivals_between arr_seq t1 (job_arrival j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
J1_IN: j1 \in arrivals_between_P arr_seq P t1 t2
ARR_LT: job_arrival j2 < job_arrival j1
PJ2: P j2
i: nat
J2_IN: j2 \in arrivals_at arr_seq i
INEQ: t1 <= i < t2

t1 <= i < job_arrival j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
J1_IN: j1 \in arrivals_between_P arr_seq P t1 t2
PJ2: P j2
i: nat
J2_IN: job_arrival j2 = i
INEQ: t1 <= i < t2
ARR_LT: i < job_arrival j1

t1 <= i < job_arrival j1
now lia. Qed. (** 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]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

forall (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
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

forall (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
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LE: 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
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

index j2 (arrivals_between_P arr_seq P t1 t2) < index j1 (arrivals_between_P arr_seq P t1 t2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1) ++ arrivals_between_P arr_seq P (job_arrival j1) t2) < index j1 (arrivals_between_P arr_seq P t1 (job_arrival j1) ++ arrivals_between_P arr_seq P (job_arrival j1) t2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) < (if j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1) then index j1 (arrivals_between_P arr_seq P t1 (job_arrival j1)) else size (arrivals_between_P arr_seq P t1 (job_arrival j1)) + index j1 (arrivals_between_P arr_seq P (job_arrival j1) t2))
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) < size (arrivals_between_P arr_seq P t1 (job_arrival j1)) + index j1 (arrivals_between_P arr_seq P (job_arrival j1) t2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) < size (arrivals_between_P arr_seq P t1 (job_arrival j1)) + index j1 (arrivals_between_P arr_seq P (job_arrival j1) t2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) < size (arrivals_between_P arr_seq P t1 (job_arrival j1))
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1

(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
P: Job -> bool
t1, t2: instant
IN1: j1 \in arrivals_between_P arr_seq P t1 t2
IN2: j2 \in arrivals_between_P arr_seq P t1 t2
LT: job_arrival j2 < job_arrival j1
T: (j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = true

False
by apply job_arrival_between_P in T; try lia. Qed. (** 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]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task 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)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task 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)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
LT: 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)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
SUB: job_task j1 = job_task j1 -> job_task j2 = job_task j1 -> arrives_in arr_seq j1 -> arrives_in arr_seq j2 -> job_arrival j1 < job_arrival j2 -> strict_prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2)

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
xs2: seq Job
NEMPT2: xs2 <> [::]
CAT2: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs2 = task_arrivals_up_to_job_arrival arr_seq j2

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
xs2: seq Job
NEMPT2: xs2 <> [::]
CAT2: task_arrivals_up_to_job_arrival arr_seq j1 ++ xs2 = task_arrivals_up_to_job_arrival arr_seq j2

j1 \in task_arrivals_up_to_job_arrival arr_seq j1
by apply arrives_in_task_arrivals_up_to => //. Qed. (** 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]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

j1 \in task_arrivals_up_to_job_arrival arr_seq j1
exact: arrives_in_task_arrivals_up_to. Qed. (** Finally, we show that a lower job index implies an earlier arrival time. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j2 <= job_index arr_seq j1 -> job_arrival j2 <= job_arrival j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j2 <= job_index arr_seq j1 -> job_arrival j2 <= job_arrival j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
IND_LT: job_index arr_seq j2 <= job_index arr_seq j1

job_arrival j2 <= job_arrival j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
IND_LT: index j2 (task_arrivals_up_to_job_arrival arr_seq j2) <= index j1 (task_arrivals_up_to_job_arrival arr_seq j1)

job_arrival j2 <= job_arrival j1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

index j1 (task_arrivals_up_to_job_arrival arr_seq j1) < index j2 (task_arrivals_up_to_job_arrival arr_seq j2)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

index j1 (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j2)) < index j2 (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j2))
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

index j1 (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j1) ++ task_arrivals_between arr_seq (job_task j2) (job_arrival j1).+1 (job_arrival j2).+1) < index j2 (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j1) ++ task_arrivals_between arr_seq (job_task j2) (job_arrival j1).+1 (job_arrival j2).+1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

index j1 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) < (if j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1) then index j2 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) else size (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) + index j2 (task_arrivals_between arr_seq (job_task j1) (job_arrival j1).+1 (job_arrival j2).+1))
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

index j1 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) < size (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) + index j2 (task_arrivals_between arr_seq (job_task j1) (job_arrival j1).+1 (job_arrival j2).+1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2
(j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

index j1 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) < size (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) + index j2 (task_arrivals_between arr_seq (job_task j1) (job_arrival j1).+1 (job_arrival j2).+1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2
(j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

(j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2

(j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_GT: job_arrival j1 < job_arrival j2
T: (j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = true

False
now apply job_arrival_between_P in T; try lia. Qed. (** 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]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_arrival j1 < job_arrival j2 -> job_index arr_seq j1 < job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_arrival j1 < job_arrival j2 -> job_index arr_seq j1 < job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
ARR_LT: job_arrival j1 < job_arrival j2

job_index arr_seq j1 < job_index arr_seq j2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
IND_LT: job_index arr_seq j2 <= job_index arr_seq j1

job_arrival j2 <= job_arrival j1
now apply index_lte_implies_arrival_lte. Qed. (** 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. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1)
now apply index_job_lt_size_task_arrivals_up_to_job. Qed. (** Since [task_arrivals_up_to_job_arrival arr_seq j] has at least the job [j] in it, its size has to be positive. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

0 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2

0 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
Z: size (task_arrivals_up_to_job_arrival arr_seq j1) = 0

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
Z: task_arrivals_up_to_job_arrival arr_seq j1 = [::]

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j1, j2: Job
H_j1_from_arrival_sequence: arrives_in arr_seq j1
H_j2_from_arrival_sequence: arrives_in arr_seq j2
H_same_task: job_task j1 = job_task j2
Z: task_arrivals_up_to_job_arrival arr_seq j1 = [::]
J_IN: j1 \in task_arrivals_up_to_job_arrival arr_seq j1

False
now rewrite Z in J_IN. Qed. End JobIndexLemmas. (** In this section, we prove a few basic properties of function [prev_job]. *) Section PreviousJob. (** Consider any type of tasks ... *) Context {Task : TaskType}. (** ... and any jobs associated with the tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any unique arrival sequence with consistent arrivals ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq. Hypothesis H_uniq_arr_seq : arrival_sequence_uniq 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. (** We observe that the fact that job [j] is in the arrival sequence implies that job [prev_job j] is in the arrival sequence. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
EQ: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) = j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
IN: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) \in task_arrivals_up_to_job_arrival arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
EQ: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) = j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
IN: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) \in task_arrivals_up_to_job_arrival arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
IN: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) \in task_arrivals_up_to_job_arrival arr_seq j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
IN: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) \in task_arrivals_up_to_job_arrival arr_seq j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
IN: nth j (task_arrivals_up_to_job_arrival arr_seq j) (job_index arr_seq j - 1) \in task_arrivals_up_to_job_arrival arr_seq j

prev_job arr_seq j \in arrivals_between arr_seq 0 (job_arrival j).+1
now move: IN; rewrite mem_filter => /andP [_ IN]. Qed. (** We show that the index of [prev_job j] in task arrivals up to [j] is one less than [job_index arr_seq j]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

job_index arr_seq j - 1 < size (task_arrivals_up_to_job_arrival arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

job_index arr_seq j < size (task_arrivals_up_to_job_arrival arr_seq j)
now apply index_job_lt_size_task_arrivals_up_to_job. Qed. (** Observe that job [j] and [prev_job j] stem from the same task. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
SIZEL: job_index arr_seq j - 1 < size (task_arrivals_up_to_job_arrival arr_seq j)

job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
SIZEL: job_of_task (job_task j) (prev_job arr_seq j) && (prev_job arr_seq j \in arrivals_between arr_seq 0 (job_arrival j).+1)

job_task (prev_job arr_seq j) = job_task j
now move : SIZEL => /andP [/eqP TSK PREV_IN]. Qed. (** We show that [prev_job arr_seq j] belongs in [task_arrivals_up_to_job_arrival arr_seq j]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

uniq (task_arrivals_up_to_job_arrival arr_seq j)
now apply uniq_task_arrivals. Qed. (** 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. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
PREV_JOB_IN: prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j

job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
TSK: job_of_task (job_task j) (prev_job arr_seq j)
PREV_IN: prev_job arr_seq j \in arrivals_between arr_seq 0 (job_arrival j).+1

job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
TSK: job_of_task (job_task j) (prev_job arr_seq j)
i: nat
PREV_IN: prev_job arr_seq j \in arrivals_at arr_seq i
INEQ: 0 <= i < (job_arrival j).+1

job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j
TSK: job_of_task (job_task j) (prev_job arr_seq j)
i: nat
PREV_IN: job_arrival (prev_job arr_seq j) = i
INEQ: 0 <= job_arrival (prev_job arr_seq j) < (job_arrival j).+1

job_arrival (prev_job arr_seq j) <= job_arrival j
now lia. Qed. (** We show that for any job [j] the job index of [prev_job j] is one less than the job index of [j]. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

0 < job_index arr_seq j -> job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

0 < job_index arr_seq j -> job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

job_index arr_seq (prev_job arr_seq j) = index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j
job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j
job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

job_task (prev_job arr_seq j) = job_task j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

job_arrival (prev_job arr_seq j) <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, NZ_IND: 0 < job_index arr_seq j

job_arrival (prev_job arr_seq j) <= job_arrival j
now apply prev_job_arr_lte. Qed. (** We also show that for any job [j] there are no task arrivals between [prev_job j] and [j].*)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

0 < job_index arr_seq j -> task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

0 < job_index arr_seq j -> task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j

task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
EQ: job_arrival (prev_job arr_seq j) = job_arrival j

task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
EQ: job_arrival (prev_job arr_seq j) = job_arrival j

task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
EQ: job_arrival (prev_job arr_seq j) = job_arrival j

task_arrivals_between arr_seq (job_task j) (job_arrival j).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
EQ: job_arrival (prev_job arr_seq j) = job_arrival j
j': Job
IN: j' \in arrivals_between arr_seq (job_arrival j).+1 (job_arrival j)
TASK: job_task j' = job_task j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
EQ: job_arrival (prev_job arr_seq j) = job_arrival j
j': Job
TASK: job_task j' = job_task j
i: nat
J'_IN: j' \in arrivals_at arr_seq i
ARR_INEQ: job_arrival j < i < job_arrival j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j

task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j

task_arrivals_between arr_seq (job_task j) (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
IN: j3 \in arrivals_between arr_seq (job_arrival (prev_job arr_seq j)).+1 (job_arrival j)
TASK: job_task j3 = job_task j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: j3 \in arrivals_at arr_seq i
ARR_INEQ: job_arrival (prev_job arr_seq j) < i < job_arrival j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: j3 \in arrivals_at arr_seq i
ARR_INEQ: job_arrival (prev_job arr_seq j) < i < job_arrival j
J3_ARR: arrives_in arr_seq j3

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
ARR_INEQ: job_arrival (prev_job arr_seq j) < job_arrival j3 < job_arrival j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_arrival (prev_job arr_seq j) < job_arrival j3
J3_L_J: job_arrival j3 < job_arrival j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_index arr_seq (prev_job arr_seq j) < job_index arr_seq j3
J3_L_J: job_arrival j3 < job_arrival j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_arrival (prev_job arr_seq j) < job_arrival j3
J3_L_J: job_arrival j3 < job_arrival j
arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_index arr_seq (prev_job arr_seq j) < job_index arr_seq j3
J3_L_J: job_arrival j3 < job_arrival j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_arrival (prev_job arr_seq j) < job_arrival j3
J3_L_J: job_arrival j3 < job_arrival j
arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_index arr_seq (prev_job arr_seq j) < job_index arr_seq j3
J3_L_J: job_index arr_seq j3 < job_index arr_seq j

False
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_arrival (prev_job arr_seq j) < job_arrival j3
J3_L_J: job_arrival j3 < job_arrival j
arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_arrival (prev_job arr_seq j) < job_arrival j3
J3_L_J: job_arrival j3 < job_arrival j

arrives_in arr_seq (prev_job arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index, POS_IND: 0 < job_index arr_seq j
LT: job_arrival (prev_job arr_seq j) < job_arrival j
j3: Job
TASK: job_task j3 = job_task j
i: nat
J3_IN: job_arrival j3 = i
J3_ARR: arrives_in arr_seq j3
PJ_L_J3: job_arrival (prev_job arr_seq j) < job_arrival j3
J3_L_J: job_arrival j3 < job_arrival j

arrives_in arr_seq (prev_job arr_seq j)
now apply prev_job_arr. Qed. (** We show that there always exists a job of lesser [job_index] than a job with a positive [job_index] that arrives in the arrival sequence. *)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

forall k : nat, k < job_index arr_seq j -> exists j' : Job, j <> j' /\ job_task j' = job_task j /\ arrives_in arr_seq j' /\ job_index arr_seq j' = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
H_positive_job_index: 0 < job_index arr_seq j

forall k : nat, k < job_index arr_seq j -> exists j' : Job, j <> j' /\ job_task j' = job_task j /\ arrives_in arr_seq j' /\ job_index arr_seq j' = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j

forall k : nat, k < job_index arr_seq j -> exists j' : Job, j <> j' /\ job_task j' = job_task j /\ arrives_in arr_seq j' /\ job_index arr_seq j' = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j

exists j' : Job, j <> j' /\ job_task j' = job_task j /\ arrives_in arr_seq j' /\ job_index arr_seq j' = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j

j <> nth j (task_arrivals_up_to_job_arrival arr_seq j) k /\ job_task (nth j (task_arrivals_up_to_job_arrival arr_seq j) k) = job_task j /\ arrives_in arr_seq (nth j (task_arrivals_up_to_job_arrival arr_seq j) k) /\ job_index arr_seq (nth j (task_arrivals_up_to_job_arrival arr_seq j) k) = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
JK_IN: jk \in task_arrivals_up_to_job_arrival arr_seq j

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
JK_IN: jk \in arrivals_between arr_seq 0 (job_arrival j).+1

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk

index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk

index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk

uniq (task_arrivals_up_to_job_arrival arr_seq j)
now apply uniq_task_arrivals => //.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

j <> jk /\ job_task jk = job_task j /\ arrives_in arr_seq jk /\ job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

j <> jk
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

j <> jk
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_index arr_seq j <> job_index arr_seq jk
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

index j (task_arrivals_up_to_job_arrival arr_seq j) <> index jk (task_arrivals_up_to_job_arrival arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
job_arrival jk <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

index j (task_arrivals_up_to_job_arrival arr_seq j) <> index jk (task_arrivals_up_to_job_arrival arr_seq j)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
job_arrival jk <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_index arr_seq j <> k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
job_arrival jk <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_arrival jk <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_arrival jk <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: job_arrival jk = i
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
I_INEQ: 0 <= job_arrival jk < (job_arrival j).+1

job_arrival jk <= job_arrival j
now lia.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_index arr_seq jk = k
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: jk \in arrivals_at arr_seq i
I_INEQ: 0 <= i < (job_arrival j).+1
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

job_arrival jk <= job_arrival j
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
j: Job
H_arrives_in_arr_seq: arrives_in arr_seq j
k: nat
K_LT: k < job_index arr_seq j
jk:= nth j (task_arrivals_up_to_job_arrival arr_seq j) k: Job
K_LT_SIZE: k < size (task_arrivals_up_to_job_arrival arr_seq j)
TSK: job_task jk = job_task j
i: nat
JK_IN: job_arrival jk = i
JK_ARR: arrives_in arr_seq jk
INDJK: index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
I_INEQ: 0 <= job_arrival jk < (job_arrival j).+1

job_arrival jk <= job_arrival j
now lia. } Qed. End PreviousJob.