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]
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 "[ 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 "[ 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 "[ 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]
(** In this file we provide basic properties related to tasks on arrival sequences. *) Section TaskArrivals. (** Consider any type of job associated with any type of tasks. *) Context {Job : JobType}. Context {Task : TaskType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any job arrival sequence with consistent arrivals. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq. (** We show that the number of arrivals of task can be split into disjoint intervals. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq

forall (tsk : Task) (t t1 t2 : nat), t1 <= t <= t2 -> number_of_task_arrivals arr_seq tsk t1 t2 = number_of_task_arrivals arr_seq tsk t1 t + number_of_task_arrivals arr_seq tsk t t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq

forall (tsk : Task) (t t1 t2 : nat), t1 <= t <= t2 -> number_of_task_arrivals arr_seq tsk t1 t2 = number_of_task_arrivals arr_seq tsk t1 t + number_of_task_arrivals arr_seq tsk t t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t, t1, t2: nat
GE: t1 <= t
LE: t <= t2

number_of_task_arrivals arr_seq tsk t1 t2 = number_of_task_arrivals arr_seq tsk t1 t + number_of_task_arrivals arr_seq tsk t t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t, t1, t2: nat
GE: t1 <= t
LE: t <= t2

size [seq j <- \cat_(t1<=t<t2)arrivals_at arr_seq t | job_of_task tsk j] = size [seq j <- \cat_(t1<=t<t)arrivals_at arr_seq t | job_of_task tsk j] + size [seq j <- \cat_(t<=t<t2)arrivals_at arr_seq t | job_of_task tsk j]
now rewrite (@big_cat_nat _ _ _ t) //= filter_cat size_cat. Qed. (** To simplify subsequent proofs, we further lift [arrivals_between_cat] to the filtered version [task_arrivals_between]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq

forall (tsk : Task) (t1 t t2 : nat), t1 <= t -> t <= t2 -> task_arrivals_between arr_seq tsk t1 t2 = task_arrivals_between arr_seq tsk t1 t ++ task_arrivals_between arr_seq tsk t t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq

forall (tsk : Task) (t1 t t2 : nat), t1 <= t -> t <= t2 -> task_arrivals_between arr_seq tsk t1 t2 = task_arrivals_between arr_seq tsk t1 t ++ task_arrivals_between arr_seq tsk t t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t, t2: nat
LEQ_t1: t1 <= t
LEQ_t2: t <= t2

task_arrivals_between arr_seq tsk t1 t2 = task_arrivals_between arr_seq tsk t1 t ++ task_arrivals_between arr_seq tsk t t2
now rewrite /task_arrivals_between -filter_cat -arrivals_between_cat. Qed. (** We show that [task_arrivals_up_to_job_arrival j1] is a prefix of [task_arrivals_up_to_job_arrival j2] if [j2] arrives at the same time or after [j1]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq

forall j1 j2 : Job, arrives_in arr_seq j1 -> arrives_in arr_seq j2 -> job_task j1 = job_task j2 -> job_arrival j1 <= job_arrival j2 -> prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq

forall j1 j2 : Job, arrives_in arr_seq j1 -> arrives_in arr_seq j2 -> job_task j1 = job_task j2 -> job_arrival j1 <= job_arrival j2 -> prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
TSK: job_task j1 = job_task j2
ARR_LT: job_arrival j1 <= job_arrival j2

prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
TSK: job_task j1 = job_task j2
ARR_LT: job_arrival j1 <= job_arrival j2

task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq (job_task j1) (job_arrival j1 + 1) (job_arrival j2 + 1) = task_arrivals_up_to_job_arrival arr_seq j2
now rewrite /task_arrivals_up_to_job_arrival !addn1 TSK -task_arrivals_between_cat. Qed. (** Let [tsk] be any task. *) Variable tsk : Task. (** Any job [j] from the arrival sequence is contained in [task_arrivals_up_to_job_arrival j]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j : Job, arrives_in arr_seq j -> j \in task_arrivals_up_to_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j : Job, arrives_in arr_seq j -> j \in task_arrivals_up_to_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

j \in task_arrivals_up_to_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

job_of_task (job_task j) j /\ j \in arrivals_between arr_seq 0 (job_arrival j).+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

j \in arrivals_between arr_seq 0 (job_arrival j).+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
ARR, EQ: j \in arrivals_at arr_seq t

j \in arrivals_between arr_seq 0 (job_arrival j).+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
ARR: j \in arrivals_at arr_seq t
EQ: job_arrival j = t

j \in arrivals_between arr_seq 0 (job_arrival j).+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
ARR: j \in arrivals_at arr_seq t
EQ: job_arrival j = t

0 <= t < t.+1
now lia. Qed. (** Also, any job [j] from the arrival sequence is contained in [task_arrivals_at_job_arrival j]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j : Job, arrives_in arr_seq j -> j \in task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j : Job, arrives_in arr_seq j -> j \in task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

j \in task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

job_of_task (job_task j) j /\ j \in arrivals_at arr_seq (job_arrival j)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

j \in arrivals_at arr_seq (job_arrival j)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

j \in arr_seq (job_arrival j)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
ARR: j \in arrivals_at arr_seq t

j \in arr_seq (job_arrival j)
now rewrite (H_consistent_arrivals j t ARR). Qed. (** We show that for any time [t_m] less than or equal to [t], task arrivals up to [t_m] forms a prefix of task arrivals up to [t]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t_m t : nat, t_m <= t -> task_arrivals_up_to arr_seq tsk t = task_arrivals_up_to arr_seq tsk t_m ++ task_arrivals_between arr_seq tsk t_m.+1 t.+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t_m t : nat, t_m <= t -> task_arrivals_up_to arr_seq tsk t = task_arrivals_up_to arr_seq tsk t_m ++ task_arrivals_between arr_seq tsk t_m.+1 t.+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: nat
INEQ: t1 <= t2

task_arrivals_up_to arr_seq tsk t2 = task_arrivals_up_to arr_seq tsk t1 ++ task_arrivals_between arr_seq tsk t1.+1 t2.+1
now rewrite -filter_cat -arrivals_between_cat. Qed. (** We observe that for any job [j], task arrivals up to [job_arrival j] is a concatenation of task arrivals before [job_arrival j] and task arrivals at [job_arrival j]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j : Job, arrives_in arr_seq j -> task_arrivals_up_to_job_arrival arr_seq j = task_arrivals_before_job_arrival arr_seq j ++ task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j : Job, arrives_in arr_seq j -> task_arrivals_up_to_job_arrival arr_seq j = task_arrivals_before_job_arrival arr_seq j ++ task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

task_arrivals_up_to_job_arrival arr_seq j = task_arrivals_before_job_arrival arr_seq j ++ task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

[seq j0 <- arrivals_between arr_seq 0 (job_arrival j).+1 | job_of_task (job_task j) j0] = task_arrivals_before_job_arrival arr_seq j ++ task_arrivals_at_job_arrival arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j

[seq j0 <- arrivals_between arr_seq 0 (job_arrival j) ++ arrivals_between arr_seq (job_arrival j) (job_arrival j).+1 | job_of_task (job_task j) j0] = [seq j0 <- arrivals_between arr_seq 0 (job_arrival j) ++ arrivals_at arr_seq (job_arrival j) | job_of_task (job_task j) j0]
now rewrite /arrivals_between big_nat1. Qed. (** We show that any job [j] in the arrival sequence is also contained in task arrivals between time instants [t1] and [t2], if [job_arrival j] lies in the interval <<[t1,t2)>>. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t1 t2 : nat), arrives_in arr_seq j -> job_task j = tsk -> t1 <= job_arrival j < t2 -> j \in task_arrivals_between arr_seq tsk t1 t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t1 t2 : nat), arrives_in arr_seq j -> job_task j = tsk -> t1 <= job_arrival j < t2 -> j \in task_arrivals_between arr_seq tsk t1 t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t1, t2: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
INEQ: t1 <= job_arrival j < t2

j \in task_arrivals_between arr_seq tsk t1 t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t1, t2: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
INEQ: t1 <= job_arrival j < t2

job_of_task tsk j /\ j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t1, t2: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
INEQ: t1 <= job_arrival j < t2

j \in arrivals_between arr_seq t1 t2
now apply arrived_between_implies_in_arrivals. Qed. (** Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] is also contained in [arrivals_between arr_seq t1 t2]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> j \in arrivals_between arr_seq t1 t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant
j: Job

j \in task_arrivals_between arr_seq tsk t1 t2 -> j \in arrivals_between arr_seq t1 t2
by rewrite mem_filter; move => /andP [/eqP TSK JB_IN]. Qed. (** Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] arrives in the arrival sequence [arr_seq]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> arrives_in arr_seq j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> arrives_in arr_seq j
move=> t1 t2 j IN; apply/in_arrivals_implies_arrived/task_arrivals_between_subset; exact IN. Qed. (** Any job [j] in [task_arrivals_before arr_seq tsk t] has an arrival time earlier than [t]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t : instant), j \in task_arrivals_before arr_seq tsk t -> job_arrival j < t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t : instant), j \in task_arrivals_before arr_seq tsk t -> job_arrival j < t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
IN: j \in task_arrivals_before arr_seq tsk t

job_arrival j < t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
IN: j \in [seq j <- arrivals_between arr_seq 0 t | job_of_task tsk j]

job_arrival j < t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
IN: j \in arrivals_between arr_seq 0 t

job_arrival j < t
by apply in_arrivals_implies_arrived_between in IN => //. Qed. (** Any job [j] in [task_arrivals_before arr_seq tsk t] is a job of task [tsk]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t : instant), j \in task_arrivals_before arr_seq tsk t -> job_task j == tsk
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t : instant), j \in task_arrivals_before arr_seq tsk t -> job_task j == tsk
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
IN: j \in task_arrivals_before arr_seq tsk t

job_task j == tsk
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: instant
IN: j \in [seq j <- arrivals_between arr_seq 0 t | job_of_task tsk j]

job_task j == tsk
by move: IN; rewrite mem_filter => /andP [TSK _]. Qed. (** We repeat the observation for [task_arrivals_between]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> job_task j = tsk
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> job_task j = tsk
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant
j: Job

j \in task_arrivals_between arr_seq tsk t1 t2 -> job_task j = tsk
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant
j: Job
JT: job_of_task tsk j

job_task j = tsk
by move: JT; rewrite /job_of_task => /eqP. Qed. (** If a job arrives between to points in time, then the corresponding interval is nonempty... *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> t1 < t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (t1 t2 : instant) (j : Job), j \in task_arrivals_between arr_seq tsk t1 t2 -> t1 < t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant
j: Job
IN: j \in task_arrivals_between arr_seq tsk t1 t2

t1 < t2
by apply /(arrivals_between_nonempty arr_seq _ _ j)/task_arrivals_between_subset. Qed. (** ... which we can also express in terms of [number_of_task_arrivals] being nonzero. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, 0 < number_of_task_arrivals arr_seq tsk t1 t2 -> t1 < t2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, 0 < number_of_task_arrivals arr_seq tsk t1 t2 -> t1 < t2
by move=> t1 t2; rewrite -has_predT => /hasP [j IN] _; eapply task_arrivals_nonempty; eauto. Qed. (** An arrival sequence with non-duplicate arrivals implies that the task arrivals also contain non-duplicate arrivals. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t : instant, arrival_sequence_uniq arr_seq -> uniq (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t : instant, arrival_sequence_uniq arr_seq -> uniq (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t: instant
UNQ_SEQ: arrival_sequence_uniq arr_seq

uniq (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t: instant
UNQ_SEQ: arrival_sequence_uniq arr_seq

uniq (arrivals_between arr_seq 0 t.+1)
now apply arrivals_uniq. Qed. (** The same observation applies to [task_arrivals_between]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, arrival_sequence_uniq arr_seq -> uniq (task_arrivals_between arr_seq tsk t1 t2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, arrival_sequence_uniq arr_seq -> uniq (task_arrivals_between arr_seq tsk t1 t2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant
UNIQ: arrival_sequence_uniq arr_seq

uniq (task_arrivals_between arr_seq tsk t1 t2)
by apply/filter_uniq/arrivals_uniq. Qed. (** A job cannot arrive before it's arrival time. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t : nat), arrives_in arr_seq j -> t < job_arrival j -> j \notin task_arrivals_up_to arr_seq (job_task j) t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (j : Job) (t : nat), arrives_in arr_seq j -> t < job_arrival j -> j \notin task_arrivals_up_to arr_seq (job_task j) t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j

j \notin task_arrivals_up_to arr_seq (job_task j) t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
IN: j \in arrivals_between arr_seq 0 t.+1

False
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
t': nat
IN: j \in arrivals_at arr_seq t'
NEQt': 0 <= t' < t.+1

False
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
t': nat
IN: j \in arrivals_at arr_seq t'
NEQt': 0 <= job_arrival j < t.+1

False
now lia. Qed. (** We show that for any two jobs [j1] and [j2], task arrivals up to arrival of job [j1] form a strict prefix of task arrivals up to arrival of job [j2]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j1 j2 : Job, job_task j1 = tsk -> job_task j2 = tsk -> 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)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall j1 j2 : Job, job_task j1 = tsk -> job_task j2 = tsk -> 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)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: 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)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2

task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 <> [::] /\ task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2

task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 <> [::]
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2

task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 <> [::]
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
JIN: ~ j2 \in [::]
NIL: task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = [::]

False
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
NIL: task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = [::]

j2 \in task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2

task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2

task_arrivals_up_to_job_arrival arr_seq j1 ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to_job_arrival arr_seq j2
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2

task_arrivals_up_to arr_seq tsk (job_arrival j1) ++ task_arrivals_between arr_seq tsk (job_arrival j1).+1 (job_arrival j2).+1 = task_arrivals_up_to arr_seq tsk (job_arrival j2)
now rewrite -task_arrivals_cat; try by lia. Qed. (** For any job [j2] with [job_index] equal to [n], the nth job in the sequence [task_arrivals_up_to arr_seq tsk t] is [j2], given that [t] is not less than [job_arrival j2]. *) (** Note that [j_def] is used as a default job for the access function and has nothing to do with the lemma. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (n : nat) (j_def j : Job) (t : nat), arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j <= t -> nth j_def (task_arrivals_up_to arr_seq tsk t) n = j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall (n : nat) (j_def j : Job) (t : nat), arrives_in arr_seq j -> job_task j = tsk -> job_index arr_seq j = n -> job_arrival j <= t -> nth j_def (task_arrivals_up_to arr_seq tsk t) n = j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

nth j_def (task_arrivals_up_to arr_seq tsk t) n = j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

nth j_def (task_arrivals_up_to arr_seq tsk t) (job_index arr_seq j) = j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)
nth j_def (task_arrivals_up_to arr_seq tsk t) (job_index arr_seq j) = j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

exists xs : seq Job, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
CAT: exists xs : seq Job, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t
index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

exists xs : seq Job, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

exists xs : seq Job, task_arrivals_up_to arr_seq tsk (job_arrival j) ++ xs = task_arrivals_up_to arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t

task_arrivals_up_to arr_seq tsk (job_arrival j) ++ task_arrivals_between arr_seq tsk (job_arrival j).+1 t.+1 = task_arrivals_up_to arr_seq tsk t
now rewrite -task_arrivals_cat.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
CAT: exists xs : seq Job, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t

index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t

index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)
now rewrite -ARR_CAT index_cat ifT; last by apply arrives_in_task_arrivals_up_to.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)

nth j_def (task_arrivals_up_to arr_seq tsk t) (job_index arr_seq j) = j
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)

j \in task_arrivals_up_to arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)

job_of_task tsk j /\ j \in arrivals_between arr_seq 0 t.+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t)

j \in arrivals_between arr_seq 0 t.+1
now apply job_in_arrivals_between => //. Qed. (** We show that task arrivals in the interval <<[t1, t2)>> is the same as concatenation of task arrivals at each instant in <<[t1, t2)>>. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1<=t<t2)task_arrivals_at arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1<=t<t2)task_arrivals_at arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant

task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1<=t<t2)task_arrivals_at arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant

[seq j <- \cat_(t1<=t<t2)arrivals_at arr_seq t | job_of_task tsk j] = \cat_(t1<=t<t2) [seq j <- arrivals_at arr_seq t | job_of_task tsk j]
now apply bigcat_nat_filter_eq_filter_bigcat_nat. Qed. (** The number of jobs of a task [tsk] in the interval <<[t1, t2)>> is the same as sum of the number of jobs of the task [tsk] at each instant in <<[t1, t2)>>. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, size (task_arrivals_between arr_seq tsk t1 t2) = \sum_(t1 <= t < t2) size (task_arrivals_at arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, size (task_arrivals_between arr_seq tsk t1 t2) = \sum_(t1 <= t < t2) size (task_arrivals_at arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant

size (task_arrivals_between arr_seq tsk t1 t2) = \sum_(t1 <= t < t2) size (task_arrivals_at arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant

size [seq j <- \cat_(t1<=t<t2)arrivals_at arr_seq t | job_of_task tsk j] = \sum_(t1 <= t < t2) size [seq j <- arrivals_at arr_seq t | job_of_task tsk j]
now rewrite size_big_nat bigcat_nat_filter_eq_filter_bigcat_nat. Qed. (** We note that, trivially, the list of task arrivals [task_arrivals_between] is sorted by arrival times because the underlying [arrivals_between] is sorted, as established by the lemma [arrivals_between_sorted]. *)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task

forall t1 t2 : instant, sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant

sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
tsk: Task
t1, t2: instant

sorted by_arrival_times (arrivals_between arr_seq t1 t2)
exact: arrivals_between_sorted. Qed. End TaskArrivals.